Theorem xpord2ind

Description: Induction over the Cartesian product ordering. Note that the substitutions cover all possible cases of membership in the predecessor class. (Contributed by Scott Fenton, 22-Aug-2024)

	Ref	Expression
Hypotheses	xpord2ind.1	$$⊢R\mathrm{Fr}A$$
	xpord2ind.2	$$⊢R\mathrm{Po}A$$
	xpord2ind.3	$$⊢R\mathrm{Se}A$$
	xpord2ind.4	$$⊢S\mathrm{Fr}B$$
	xpord2ind.5	$$⊢S\mathrm{Po}B$$
	xpord2ind.6	$$⊢S\mathrm{Se}B$$
	xpord2ind.7	$$⊢a=c\to \left(\phi \leftrightarrow \psi \right)$$
	xpord2ind.8	$$⊢b=d\to \left(\psi \leftrightarrow \chi \right)$$
	xpord2ind.9	$$⊢a=c\to \left(\theta \leftrightarrow \chi \right)$$
	xpord2ind.11	$$⊢a=X\to \left(\phi \leftrightarrow \tau \right)$$
	xpord2ind.12	$$⊢b=Y\to \left(\tau \leftrightarrow \eta \right)$$
	xpord2ind.i	$$⊢\left(a\in A\wedge b\in B\right)\to \left(\left(\forall c\in Pred\left(R,A,a\right)\forall d\in Pred\left(S,B,b\right)\chi \wedge \forall c\in Pred\left(R,A,a\right)\psi \wedge \forall d\in Pred\left(S,B,b\right)\theta \right)\to \phi \right)$$
Assertion	xpord2ind	$$⊢\left(X\in A\wedge Y\in B\right)\to \eta$$

Proof

Step	Hyp	Ref	Expression
1		xpord2ind.1	$$⊢R\mathrm{Fr}A$$
2		xpord2ind.2	$$⊢R\mathrm{Po}A$$
3		xpord2ind.3	$$⊢R\mathrm{Se}A$$
4		xpord2ind.4	$$⊢S\mathrm{Fr}B$$
5		xpord2ind.5	$$⊢S\mathrm{Po}B$$
6		xpord2ind.6	$$⊢S\mathrm{Se}B$$
7		xpord2ind.7	$$⊢a=c\to \left(\phi \leftrightarrow \psi \right)$$
8		xpord2ind.8	$$⊢b=d\to \left(\psi \leftrightarrow \chi \right)$$
9		xpord2ind.9	$$⊢a=c\to \left(\theta \leftrightarrow \chi \right)$$
10		xpord2ind.11	$$⊢a=X\to \left(\phi \leftrightarrow \tau \right)$$
11		xpord2ind.12	$$⊢b=Y\to \left(\tau \leftrightarrow \eta \right)$$
12		xpord2ind.i	$$⊢\left(a\in A\wedge b\in B\right)\to \left(\left(\forall c\in Pred\left(R,A,a\right)\forall d\in Pred\left(S,B,b\right)\chi \wedge \forall c\in Pred\left(R,A,a\right)\psi \wedge \forall d\in Pred\left(S,B,b\right)\theta \right)\to \phi \right)$$
13		eqid	$$⊢\left\{⟨x,y⟩|\left(x\in \left(A\times B\right)\wedge y\in \left(A\times B\right)\wedge \left(\left(1^{st}\left(x\right)R{1}^{st}\left(y\right)\vee 1^{st}\left(x\right)=1^{st}\left(y\right)\right)\wedge \left(2^{nd}\left(x\right)S{2}^{nd}\left(y\right)\vee 2^{nd}\left(x\right)=2^{nd}\left(y\right)\right)\wedge x\ne y\right)\right)\right\}=\left\{⟨x,y⟩|\left(x\in \left(A\times B\right)\wedge y\in \left(A\times B\right)\wedge \left(\left(1^{st}\left(x\right)R{1}^{st}\left(y\right)\vee 1^{st}\left(x\right)=1^{st}\left(y\right)\right)\wedge \left(2^{nd}\left(x\right)S{2}^{nd}\left(y\right)\vee 2^{nd}\left(x\right)=2^{nd}\left(y\right)\right)\wedge x\ne y\right)\right)\right\}$$
14	13 1 2 3 4 5 6 7 8 9 10 11 12	xpord2indlem	$$⊢\left(X\in A\wedge Y\in B\right)\to \eta$$