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	|- ( ka -> X e. A )
	xpord3indd.y	|- ( ka -> Y e. B )
	xpord3indd.z	|- ( ka -> Z e. C )
	xpord3indd.1	|- ( ka -> R Fr A )
	xpord3indd.2	|- ( ka -> R Po A )
	xpord3indd.3	|- ( ka -> R Se A )
	xpord3indd.4	|- ( ka -> S Fr B )
	xpord3indd.5	|- ( ka -> S Po B )
	xpord3indd.6	|- ( ka -> S Se B )
	xpord3indd.7	|- ( ka -> T Fr C )
	xpord3indd.8	|- ( ka -> T Po C )
	xpord3indd.9	|- ( ka -> T Se C )
	xpord3indd.10	|- ( a = d -> ( ph <-> ps ) )
	xpord3indd.11	|- ( b = e -> ( ps <-> ch ) )
	xpord3indd.12	|- ( c = f -> ( ch <-> th ) )
	xpord3indd.13	|- ( a = d -> ( ta <-> th ) )
	xpord3indd.14	|- ( b = e -> ( et <-> ta ) )
	xpord3indd.15	|- ( b = e -> ( ze <-> th ) )
	xpord3indd.16	|- ( c = f -> ( si <-> ta ) )
	xpord3indd.17	|- ( a = X -> ( ph <-> rh ) )
	xpord3indd.18	|- ( b = Y -> ( rh <-> mu ) )
	xpord3indd.19	|- ( c = Z -> ( mu <-> la ) )
	xpord3indd.i	|- ( ( ka /\ ( a e. A /\ b e. B /\ c e. C ) ) -> ( ( ( A. d e. Pred ( R , A , a ) A. e e. Pred ( S , B , b ) A. f e. Pred ( T , C , c ) th /\ A. d e. Pred ( R , A , a ) A. e e. Pred ( S , B , b ) ch /\ A. d e. Pred ( R , A , a ) A. f e. Pred ( T , C , c ) ze ) /\ ( A. d e. Pred ( R , A , a ) ps /\ A. e e. Pred ( S , B , b ) A. f e. Pred ( T , C , c ) ta /\ A. e e. Pred ( S , B , b ) si ) /\ A. f e. Pred ( T , C , c ) et ) -> ph ) )
Assertion	xpord3indd	|- ( ka -> la )

Proof

Step	Hyp	Ref	Expression
1		xpord3indd.x	|- ( ka -> X e. A )
2		xpord3indd.y	|- ( ka -> Y e. B )
3		xpord3indd.z	|- ( ka -> Z e. C )
4		xpord3indd.1	|- ( ka -> R Fr A )
5		xpord3indd.2	|- ( ka -> R Po A )
6		xpord3indd.3	|- ( ka -> R Se A )
7		xpord3indd.4	|- ( ka -> S Fr B )
8		xpord3indd.5	|- ( ka -> S Po B )
9		xpord3indd.6	|- ( ka -> S Se B )
10		xpord3indd.7	|- ( ka -> T Fr C )
11		xpord3indd.8	|- ( ka -> T Po C )
12		xpord3indd.9	|- ( ka -> T Se C )
13		xpord3indd.10	|- ( a = d -> ( ph <-> ps ) )
14		xpord3indd.11	|- ( b = e -> ( ps <-> ch ) )
15		xpord3indd.12	|- ( c = f -> ( ch <-> th ) )
16		xpord3indd.13	|- ( a = d -> ( ta <-> th ) )
17		xpord3indd.14	|- ( b = e -> ( et <-> ta ) )
18		xpord3indd.15	|- ( b = e -> ( ze <-> th ) )
19		xpord3indd.16	|- ( c = f -> ( si <-> ta ) )
20		xpord3indd.17	|- ( a = X -> ( ph <-> rh ) )
21		xpord3indd.18	|- ( b = Y -> ( rh <-> mu ) )
22		xpord3indd.19	|- ( c = Z -> ( mu <-> la ) )
23		xpord3indd.i	|- ( ( ka /\ ( a e. A /\ b e. B /\ c e. C ) ) -> ( ( ( A. d e. Pred ( R , A , a ) A. e e. Pred ( S , B , b ) A. f e. Pred ( T , C , c ) th /\ A. d e. Pred ( R , A , a ) A. e e. Pred ( S , B , b ) ch /\ A. d e. Pred ( R , A , a ) A. f e. Pred ( T , C , c ) ze ) /\ ( A. d e. Pred ( R , A , a ) ps /\ A. e e. Pred ( S , B , b ) A. f e. Pred ( T , C , c ) ta /\ A. e e. Pred ( S , B , b ) si ) /\ A. f e. Pred ( T , C , c ) et ) -> ph ) )
24		eqid	|- { <. x , y >. | ( x e. ( ( A X. B ) X. C ) /\ y e. ( ( A X. B ) X. C ) /\ ( ( ( ( 1st ` ( 1st ` x ) ) R ( 1st ` ( 1st ` y ) ) \/ ( 1st ` ( 1st ` x ) ) = ( 1st ` ( 1st ` y ) ) ) /\ ( ( 2nd ` ( 1st ` x ) ) S ( 2nd ` ( 1st ` y ) ) \/ ( 2nd ` ( 1st ` x ) ) = ( 2nd ` ( 1st ` y ) ) ) /\ ( ( 2nd ` x ) T ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) ) /\ x =/= y ) ) } = { <. x , y >. | ( x e. ( ( A X. B ) X. C ) /\ y e. ( ( A X. B ) X. C ) /\ ( ( ( ( 1st ` ( 1st ` x ) ) R ( 1st ` ( 1st ` y ) ) \/ ( 1st ` ( 1st ` x ) ) = ( 1st ` ( 1st ` y ) ) ) /\ ( ( 2nd ` ( 1st ` x ) ) S ( 2nd ` ( 1st ` y ) ) \/ ( 2nd ` ( 1st ` x ) ) = ( 2nd ` ( 1st ` y ) ) ) /\ ( ( 2nd ` x ) T ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) ) /\ x =/= y ) ) }
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	|- ( ka -> la )