Theorem xpord3indd

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

	Ref	Expression
Hypotheses	xpord3indd.x	$$⊢\kappa \to X\in A$$
	xpord3indd.y	$$⊢\kappa \to Y\in B$$
	xpord3indd.z	$$⊢\kappa \to Z\in C$$
	xpord3indd.1	$$⊢\kappa \to R\mathrm{Fr}A$$
	xpord3indd.2	$$⊢\kappa \to R\mathrm{Po}A$$
	xpord3indd.3	$$⊢\kappa \to R\mathrm{Se}A$$
	xpord3indd.4	$$⊢\kappa \to S\mathrm{Fr}B$$
	xpord3indd.5	$$⊢\kappa \to S\mathrm{Po}B$$
	xpord3indd.6	$$⊢\kappa \to S\mathrm{Se}B$$
	xpord3indd.7	$$⊢\kappa \to T\mathrm{Fr}C$$
	xpord3indd.8	$$⊢\kappa \to T\mathrm{Po}C$$
	xpord3indd.9	$$⊢\kappa \to T\mathrm{Se}C$$
	xpord3indd.10	$$⊢a=d\to \left(\phi \leftrightarrow \psi \right)$$
	xpord3indd.11	$$⊢b=e\to \left(\psi \leftrightarrow \chi \right)$$
	xpord3indd.12	$$⊢c=f\to \left(\chi \leftrightarrow \theta \right)$$
	xpord3indd.13	$$⊢a=d\to \left(\tau \leftrightarrow \theta \right)$$
	xpord3indd.14	$$⊢b=e\to \left(\eta \leftrightarrow \tau \right)$$
	xpord3indd.15	$$⊢b=e\to \left(\zeta \leftrightarrow \theta \right)$$
	xpord3indd.16	$$⊢c=f\to \left(\sigma \leftrightarrow \tau \right)$$
	xpord3indd.17	$$⊢a=X\to \left(\phi \leftrightarrow \rho \right)$$
	xpord3indd.18	$$⊢b=Y\to \left(\rho \leftrightarrow \mu \right)$$
	xpord3indd.19	$$⊢c=Z\to \left(\mu \leftrightarrow \lambda \right)$$
	xpord3indd.i	$$⊢\left(\kappa \wedge \left(a\in A\wedge b\in B\wedge c\in C\right)\right)\to \left(\left(\left(\forall d\in Pred\left(R,A,a\right)\forall e\in Pred\left(S,B,b\right)\forall f\in Pred\left(T,C,c\right)\theta \wedge \forall d\in Pred\left(R,A,a\right)\forall e\in Pred\left(S,B,b\right)\chi \wedge \forall d\in Pred\left(R,A,a\right)\forall f\in Pred\left(T,C,c\right)\zeta \right)\wedge \left(\forall d\in Pred\left(R,A,a\right)\psi \wedge \forall e\in Pred\left(S,B,b\right)\forall f\in Pred\left(T,C,c\right)\tau \wedge \forall e\in Pred\left(S,B,b\right)\sigma \right)\wedge \forall f\in Pred\left(T,C,c\right)\eta \right)\to \phi \right)$$
Assertion	xpord3indd	$$⊢\kappa \to \lambda$$

Proof

Step	Hyp	Ref	Expression
1		xpord3indd.x	$$⊢\kappa \to X\in A$$
2		xpord3indd.y	$$⊢\kappa \to Y\in B$$
3		xpord3indd.z	$$⊢\kappa \to Z\in C$$
4		xpord3indd.1	$$⊢\kappa \to R\mathrm{Fr}A$$
5		xpord3indd.2	$$⊢\kappa \to R\mathrm{Po}A$$
6		xpord3indd.3	$$⊢\kappa \to R\mathrm{Se}A$$
7		xpord3indd.4	$$⊢\kappa \to S\mathrm{Fr}B$$
8		xpord3indd.5	$$⊢\kappa \to S\mathrm{Po}B$$
9		xpord3indd.6	$$⊢\kappa \to S\mathrm{Se}B$$
10		xpord3indd.7	$$⊢\kappa \to T\mathrm{Fr}C$$
11		xpord3indd.8	$$⊢\kappa \to T\mathrm{Po}C$$
12		xpord3indd.9	$$⊢\kappa \to T\mathrm{Se}C$$
13		xpord3indd.10	$$⊢a=d\to \left(\phi \leftrightarrow \psi \right)$$
14		xpord3indd.11	$$⊢b=e\to \left(\psi \leftrightarrow \chi \right)$$
15		xpord3indd.12	$$⊢c=f\to \left(\chi \leftrightarrow \theta \right)$$
16		xpord3indd.13	$$⊢a=d\to \left(\tau \leftrightarrow \theta \right)$$
17		xpord3indd.14	$$⊢b=e\to \left(\eta \leftrightarrow \tau \right)$$
18		xpord3indd.15	$$⊢b=e\to \left(\zeta \leftrightarrow \theta \right)$$
19		xpord3indd.16	$$⊢c=f\to \left(\sigma \leftrightarrow \tau \right)$$
20		xpord3indd.17	$$⊢a=X\to \left(\phi \leftrightarrow \rho \right)$$
21		xpord3indd.18	$$⊢b=Y\to \left(\rho \leftrightarrow \mu \right)$$
22		xpord3indd.19	$$⊢c=Z\to \left(\mu \leftrightarrow \lambda \right)$$
23		xpord3indd.i	$$⊢\left(\kappa \wedge \left(a\in A\wedge b\in B\wedge c\in C\right)\right)\to \left(\left(\left(\forall d\in Pred\left(R,A,a\right)\forall e\in Pred\left(S,B,b\right)\forall f\in Pred\left(T,C,c\right)\theta \wedge \forall d\in Pred\left(R,A,a\right)\forall e\in Pred\left(S,B,b\right)\chi \wedge \forall d\in Pred\left(R,A,a\right)\forall f\in Pred\left(T,C,c\right)\zeta \right)\wedge \left(\forall d\in Pred\left(R,A,a\right)\psi \wedge \forall e\in Pred\left(S,B,b\right)\forall f\in Pred\left(T,C,c\right)\tau \wedge \forall e\in Pred\left(S,B,b\right)\sigma \right)\wedge \forall f\in Pred\left(T,C,c\right)\eta \right)\to \phi \right)$$
24		eqid	$$⊢\left\{⟨x,y⟩|\left(x\in \left(\left(A\times B\right)\times C\right)\wedge y\in \left(\left(A\times B\right)\times C\right)\wedge \left(\left(\left(1^{st}\left(1^{st}\left(x\right)\right)R{1}^{st}\left(1^{st}\left(y\right)\right)\vee 1^{st}\left(1^{st}\left(x\right)\right)=1^{st}\left(1^{st}\left(y\right)\right)\right)\wedge \left(2^{nd}\left(1^{st}\left(x\right)\right)S{2}^{nd}\left(1^{st}\left(y\right)\right)\vee 2^{nd}\left(1^{st}\left(x\right)\right)=2^{nd}\left(1^{st}\left(y\right)\right)\right)\wedge \left(2^{nd}\left(x\right)T{2}^{nd}\left(y\right)\vee 2^{nd}\left(x\right)=2^{nd}\left(y\right)\right)\right)\wedge x\ne y\right)\right)\right\}=\left\{⟨x,y⟩|\left(x\in \left(\left(A\times B\right)\times C\right)\wedge y\in \left(\left(A\times B\right)\times C\right)\wedge \left(\left(\left(1^{st}\left(1^{st}\left(x\right)\right)R{1}^{st}\left(1^{st}\left(y\right)\right)\vee 1^{st}\left(1^{st}\left(x\right)\right)=1^{st}\left(1^{st}\left(y\right)\right)\right)\wedge \left(2^{nd}\left(1^{st}\left(x\right)\right)S{2}^{nd}\left(1^{st}\left(y\right)\right)\vee 2^{nd}\left(1^{st}\left(x\right)\right)=2^{nd}\left(1^{st}\left(y\right)\right)\right)\wedge \left(2^{nd}\left(x\right)T{2}^{nd}\left(y\right)\vee 2^{nd}\left(x\right)=2^{nd}\left(y\right)\right)\right)\wedge x\ne y\right)\right)\right\}$$
25	24 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23	xpord3inddlem	$$⊢\kappa \to \lambda$$