Theorem xpord3ind

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, 4-Sep-2024)

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

Proof

Step	Hyp	Ref	Expression
1		xpord3ind.1	|- R Fr A
2		xpord3ind.2	|- R Po A
3		xpord3ind.3	|- R Se A
4		xpord3ind.4	|- S Fr B
5		xpord3ind.5	|- S Po B
6		xpord3ind.6	|- S Se B
7		xpord3ind.7	|- T Fr C
8		xpord3ind.8	|- T Po C
9		xpord3ind.9	|- T Se C
10		xpord3ind.10	|- ( a = d -> ( ph <-> ps ) )
11		xpord3ind.11	|- ( b = e -> ( ps <-> ch ) )
12		xpord3ind.12	|- ( c = f -> ( ch <-> th ) )
13		xpord3ind.13	|- ( a = d -> ( ta <-> th ) )
14		xpord3ind.14	|- ( b = e -> ( et <-> ta ) )
15		xpord3ind.15	|- ( b = e -> ( ze <-> th ) )
16		xpord3ind.16	|- ( c = f -> ( si <-> ta ) )
17		xpord3ind.17	|- ( a = X -> ( ph <-> rh ) )
18		xpord3ind.18	|- ( b = Y -> ( rh <-> mu ) )
19		xpord3ind.19	|- ( c = Z -> ( mu <-> la ) )
20		xpord3ind.i	|- ( ( 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 ) )
21		simp1	|- ( ( X e. A /\ Y e. B /\ Z e. C ) -> X e. A )
22		simp2	|- ( ( X e. A /\ Y e. B /\ Z e. C ) -> Y e. B )
23		simp3	|- ( ( X e. A /\ Y e. B /\ Z e. C ) -> Z e. C )
24		ax-1	|- ( R Fr A -> ( ( X e. A /\ Y e. B /\ Z e. C ) -> R Fr A ) )
25	1 24	ax-mp	|- ( ( X e. A /\ Y e. B /\ Z e. C ) -> R Fr A )
26	2	a1i	|- ( ( X e. A /\ Y e. B /\ Z e. C ) -> R Po A )
27	3	a1i	|- ( ( X e. A /\ Y e. B /\ Z e. C ) -> R Se A )
28	4	a1i	|- ( ( X e. A /\ Y e. B /\ Z e. C ) -> S Fr B )
29	5	a1i	|- ( ( X e. A /\ Y e. B /\ Z e. C ) -> S Po B )
30	6	a1i	|- ( ( X e. A /\ Y e. B /\ Z e. C ) -> S Se B )
31	7	a1i	|- ( ( X e. A /\ Y e. B /\ Z e. C ) -> T Fr C )
32	8	a1i	|- ( ( X e. A /\ Y e. B /\ Z e. C ) -> T Po C )
33	9	a1i	|- ( ( X e. A /\ Y e. B /\ Z e. C ) -> T Se C )
34	20	adantl	|- ( ( ( X e. A /\ Y e. B /\ Z e. C ) /\ ( 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 ) )
35	21 22 23 25 26 27 28 29 30 31 32 33 10 11 12 13 14 15 16 17 18 19 34	xpord3indd	|- ( ( X e. A /\ Y e. B /\ Z e. C ) -> la )