Metamath Proof Explorer

Theorem on3ind

Description: Triple induction over ordinals. (Contributed by Scott Fenton, 4-Sep-2024)

Ref Expression
Hypotheses on3ind.1 
|- ( a = d -> ( ph <-> ps ) )
on3ind.2 
|- ( b = e -> ( ps <-> ch ) )
on3ind.3 
|- ( c = f -> ( ch <-> th ) )
on3ind.4 
|- ( a = d -> ( ta <-> th ) )
on3ind.5 
|- ( b = e -> ( et <-> ta ) )
on3ind.6 
|- ( b = e -> ( ze <-> th ) )
on3ind.7 
|- ( c = f -> ( si <-> ta ) )
on3ind.8 
|- ( a = X -> ( ph <-> rh ) )
on3ind.9 
|- ( b = Y -> ( rh <-> mu ) )
on3ind.10 
|- ( c = Z -> ( mu <-> la ) )
on3ind.i 
|- ( ( a e. On /\ b e. On /\ c e. On ) -> ( ( ( A. d e. a A. e e. b A. f e. c th /\ A. d e. a A. e e. b ch /\ A. d e. a A. f e. c ze ) /\ ( A. d e. a ps /\ A. e e. b A. f e. c ta /\ A. e e. b si ) /\ A. f e. c et ) -> ph ) )
Assertion on3ind 
|- ( ( X e. On /\ Y e. On /\ Z e. On ) -> la )

Proof

Step Hyp Ref Expression
1 on3ind.1 
 |-  ( a = d -> ( ph <-> ps ) )
2 on3ind.2 
 |-  ( b = e -> ( ps <-> ch ) )
3 on3ind.3 
 |-  ( c = f -> ( ch <-> th ) )
4 on3ind.4 
 |-  ( a = d -> ( ta <-> th ) )
5 on3ind.5 
 |-  ( b = e -> ( et <-> ta ) )
6 on3ind.6 
 |-  ( b = e -> ( ze <-> th ) )
7 on3ind.7 
 |-  ( c = f -> ( si <-> ta ) )
8 on3ind.8 
 |-  ( a = X -> ( ph <-> rh ) )
9 on3ind.9 
 |-  ( b = Y -> ( rh <-> mu ) )
10 on3ind.10 
 |-  ( c = Z -> ( mu <-> la ) )
11 on3ind.i 
 |-  ( ( a e. On /\ b e. On /\ c e. On ) -> ( ( ( A. d e. a A. e e. b A. f e. c th /\ A. d e. a A. e e. b ch /\ A. d e. a A. f e. c ze ) /\ ( A. d e. a ps /\ A. e e. b A. f e. c ta /\ A. e e. b si ) /\ A. f e. c et ) -> ph ) )
12 eqid 
 |-  { <. x , y >. | ( x e. ( ( On X. On ) X. On ) /\ y e. ( ( On X. On ) X. On ) /\ ( ( ( ( 1st ` ( 1st ` x ) ) _E ( 1st ` ( 1st ` y ) ) \/ ( 1st ` ( 1st ` x ) ) = ( 1st ` ( 1st ` y ) ) ) /\ ( ( 2nd ` ( 1st ` x ) ) _E ( 2nd ` ( 1st ` y ) ) \/ ( 2nd ` ( 1st ` x ) ) = ( 2nd ` ( 1st ` y ) ) ) /\ ( ( 2nd ` x ) _E ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) ) /\ x =/= y ) ) } = { <. x , y >. | ( x e. ( ( On X. On ) X. On ) /\ y e. ( ( On X. On ) X. On ) /\ ( ( ( ( 1st ` ( 1st ` x ) ) _E ( 1st ` ( 1st ` y ) ) \/ ( 1st ` ( 1st ` x ) ) = ( 1st ` ( 1st ` y ) ) ) /\ ( ( 2nd ` ( 1st ` x ) ) _E ( 2nd ` ( 1st ` y ) ) \/ ( 2nd ` ( 1st ` x ) ) = ( 2nd ` ( 1st ` y ) ) ) /\ ( ( 2nd ` x ) _E ( 2nd ` y ) \/ ( 2nd ` x ) = ( 2nd ` y ) ) ) /\ x =/= y ) ) }
13 onfr 
 |-  _E Fr On
14 epweon 
 |-  _E We On
15 weso 
 |-  ( _E We On -> _E Or On )
16 sopo 
 |-  ( _E Or On -> _E Po On )
17 14 15 16 mp2b 
 |-  _E Po On
18 epse 
 |-  _E Se On
19 predon 
 |-  ( a e. On -> Pred ( _E , On , a ) = a )
20 19 3ad2ant1 
 |-  ( ( a e. On /\ b e. On /\ c e. On ) -> Pred ( _E , On , a ) = a )
21 predon 
 |-  ( b e. On -> Pred ( _E , On , b ) = b )
22 21 3ad2ant2 
 |-  ( ( a e. On /\ b e. On /\ c e. On ) -> Pred ( _E , On , b ) = b )
23 predon 
 |-  ( c e. On -> Pred ( _E , On , c ) = c )
24 23 3ad2ant3 
 |-  ( ( a e. On /\ b e. On /\ c e. On ) -> Pred ( _E , On , c ) = c )
25 24 raleqdv 
 |-  ( ( a e. On /\ b e. On /\ c e. On ) -> ( A. f e. Pred ( _E , On , c ) th <-> A. f e. c th ) )
26 22 25 raleqbidv 
 |-  ( ( a e. On /\ b e. On /\ c e. On ) -> ( A. e e. Pred ( _E , On , b ) A. f e. Pred ( _E , On , c ) th <-> A. e e. b A. f e. c th ) )
27 20 26 raleqbidv 
 |-  ( ( a e. On /\ b e. On /\ c e. On ) -> ( A. d e. Pred ( _E , On , a ) A. e e. Pred ( _E , On , b ) A. f e. Pred ( _E , On , c ) th <-> A. d e. a A. e e. b A. f e. c th ) )
28 22 raleqdv 
 |-  ( ( a e. On /\ b e. On /\ c e. On ) -> ( A. e e. Pred ( _E , On , b ) ch <-> A. e e. b ch ) )
29 20 28 raleqbidv 
 |-  ( ( a e. On /\ b e. On /\ c e. On ) -> ( A. d e. Pred ( _E , On , a ) A. e e. Pred ( _E , On , b ) ch <-> A. d e. a A. e e. b ch ) )
30 24 raleqdv 
 |-  ( ( a e. On /\ b e. On /\ c e. On ) -> ( A. f e. Pred ( _E , On , c ) ze <-> A. f e. c ze ) )
31 20 30 raleqbidv 
 |-  ( ( a e. On /\ b e. On /\ c e. On ) -> ( A. d e. Pred ( _E , On , a ) A. f e. Pred ( _E , On , c ) ze <-> A. d e. a A. f e. c ze ) )
32 27 29 31 3anbi123d 
 |-  ( ( a e. On /\ b e. On /\ c e. On ) -> ( ( A. d e. Pred ( _E , On , a ) A. e e. Pred ( _E , On , b ) A. f e. Pred ( _E , On , c ) th /\ A. d e. Pred ( _E , On , a ) A. e e. Pred ( _E , On , b ) ch /\ A. d e. Pred ( _E , On , a ) A. f e. Pred ( _E , On , c ) ze ) <-> ( A. d e. a A. e e. b A. f e. c th /\ A. d e. a A. e e. b ch /\ A. d e. a A. f e. c ze ) ) )
33 20 raleqdv 
 |-  ( ( a e. On /\ b e. On /\ c e. On ) -> ( A. d e. Pred ( _E , On , a ) ps <-> A. d e. a ps ) )
34 24 raleqdv 
 |-  ( ( a e. On /\ b e. On /\ c e. On ) -> ( A. f e. Pred ( _E , On , c ) ta <-> A. f e. c ta ) )
35 22 34 raleqbidv 
 |-  ( ( a e. On /\ b e. On /\ c e. On ) -> ( A. e e. Pred ( _E , On , b ) A. f e. Pred ( _E , On , c ) ta <-> A. e e. b A. f e. c ta ) )
36 22 raleqdv 
 |-  ( ( a e. On /\ b e. On /\ c e. On ) -> ( A. e e. Pred ( _E , On , b ) si <-> A. e e. b si ) )
37 33 35 36 3anbi123d 
 |-  ( ( a e. On /\ b e. On /\ c e. On ) -> ( ( A. d e. Pred ( _E , On , a ) ps /\ A. e e. Pred ( _E , On , b ) A. f e. Pred ( _E , On , c ) ta /\ A. e e. Pred ( _E , On , b ) si ) <-> ( A. d e. a ps /\ A. e e. b A. f e. c ta /\ A. e e. b si ) ) )
38 24 raleqdv 
 |-  ( ( a e. On /\ b e. On /\ c e. On ) -> ( A. f e. Pred ( _E , On , c ) et <-> A. f e. c et ) )
39 32 37 38 3anbi123d 
 |-  ( ( a e. On /\ b e. On /\ c e. On ) -> ( ( ( A. d e. Pred ( _E , On , a ) A. e e. Pred ( _E , On , b ) A. f e. Pred ( _E , On , c ) th /\ A. d e. Pred ( _E , On , a ) A. e e. Pred ( _E , On , b ) ch /\ A. d e. Pred ( _E , On , a ) A. f e. Pred ( _E , On , c ) ze ) /\ ( A. d e. Pred ( _E , On , a ) ps /\ A. e e. Pred ( _E , On , b ) A. f e. Pred ( _E , On , c ) ta /\ A. e e. Pred ( _E , On , b ) si ) /\ A. f e. Pred ( _E , On , c ) et ) <-> ( ( A. d e. a A. e e. b A. f e. c th /\ A. d e. a A. e e. b ch /\ A. d e. a A. f e. c ze ) /\ ( A. d e. a ps /\ A. e e. b A. f e. c ta /\ A. e e. b si ) /\ A. f e. c et ) ) )
40 39 11 sylbid 
 |-  ( ( a e. On /\ b e. On /\ c e. On ) -> ( ( ( A. d e. Pred ( _E , On , a ) A. e e. Pred ( _E , On , b ) A. f e. Pred ( _E , On , c ) th /\ A. d e. Pred ( _E , On , a ) A. e e. Pred ( _E , On , b ) ch /\ A. d e. Pred ( _E , On , a ) A. f e. Pred ( _E , On , c ) ze ) /\ ( A. d e. Pred ( _E , On , a ) ps /\ A. e e. Pred ( _E , On , b ) A. f e. Pred ( _E , On , c ) ta /\ A. e e. Pred ( _E , On , b ) si ) /\ A. f e. Pred ( _E , On , c ) et ) -> ph ) )
41 12 13 17 18 13 17 18 13 17 18 1 2 3 4 5 6 7 8 9 10 40 xpord3ind 
 |-  ( ( X e. On /\ Y e. On /\ Z e. On ) -> la )