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 Fr A
	xpord2ind.2	|- R Po A
	xpord2ind.3	|- R Se A
	xpord2ind.4	|- S Fr B
	xpord2ind.5	|- S Po B
	xpord2ind.6	|- S Se B
	xpord2ind.7	|- ( a = c -> ( ph <-> ps ) )
	xpord2ind.8	|- ( b = d -> ( ps <-> ch ) )
	xpord2ind.9	|- ( a = c -> ( th <-> ch ) )
	xpord2ind.11	|- ( a = X -> ( ph <-> ta ) )
	xpord2ind.12	|- ( b = Y -> ( ta <-> et ) )
	xpord2ind.i	|- ( ( a e. A /\ b e. B ) -> ( ( A. c e. Pred ( R , A , a ) A. d e. Pred ( S , B , b ) ch /\ A. c e. Pred ( R , A , a ) ps /\ A. d e. Pred ( S , B , b ) th ) -> ph ) )
Assertion	xpord2ind	|- ( ( X e. A /\ Y e. B ) -> et )

Proof

Step	Hyp	Ref	Expression
1		xpord2ind.1	|- R Fr A
2		xpord2ind.2	|- R Po A
3		xpord2ind.3	|- R Se A
4		xpord2ind.4	|- S Fr B
5		xpord2ind.5	|- S Po B
6		xpord2ind.6	|- S Se B
7		xpord2ind.7	|- ( a = c -> ( ph <-> ps ) )
8		xpord2ind.8	|- ( b = d -> ( ps <-> ch ) )
9		xpord2ind.9	|- ( a = c -> ( th <-> ch ) )
10		xpord2ind.11	|- ( a = X -> ( ph <-> ta ) )
11		xpord2ind.12	|- ( b = Y -> ( ta <-> et ) )
12		xpord2ind.i	|- ( ( a e. A /\ b e. B ) -> ( ( A. c e. Pred ( R , A , a ) A. d e. Pred ( S , B , b ) ch /\ A. c e. Pred ( R , A , a ) ps /\ A. d e. Pred ( S , B , b ) th ) -> ph ) )
13		eqid	|- { <. x , y >. | ( x e. ( A X. B ) /\ y e. ( A X. B ) /\ ( ( ( 1st ` x ) R ( 1st ` y ) \/ ( 1st ` x ) = ( 1st ` y ) ) /\ ( ( 2nd ` x ) S ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) /\ x =/= y ) ) } = { <. x , y >. | ( x e. ( A X. B ) /\ y e. ( A X. B ) /\ ( ( ( 1st ` x ) R ( 1st ` y ) \/ ( 1st ` x ) = ( 1st ` y ) ) /\ ( ( 2nd ` x ) S ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) /\ x =/= y ) ) }
14	13 1 2 3 4 5 6 7 8 9 10 11 12	xpord2indlem	|- ( ( X e. A /\ Y e. B ) -> et )