Does the Axiom of Substitution Have Limits?

Your statement that $P(X)$ is the proposition that the elements of $X$ are ordered from least to greatest tacitly relies on two assumptions: (1) that $X$ is a sequence of objects and (2) that there is an ordering relation on those objects. When you make those assumptions explicit (as you must if you want to model $P$ in set thoery), then the axiom of substitution holds. You might be interested in the notion of referential transparency.