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 onfr 
 |-  _E Fr On
13 epweon 
 |-  _E We On
14 weso 
 |-  ( _E We On -> _E Or On )
15 sopo 
 |-  ( _E Or On -> _E Po On )
16 13 14 15 mp2b 
 |-  _E Po On
17 epse 
 |-  _E Se On
18 predon 
 |-  ( a e. On -> Pred ( _E , On , a ) = a )
19 18 3ad2ant1 
 |-  ( ( a e. On /\ b e. On /\ c e. On ) -> Pred ( _E , On , a ) = a )
20 predon 
 |-  ( b e. On -> Pred ( _E , On , b ) = b )
21 20 3ad2ant2 
 |-  ( ( a e. On /\ b e. On /\ c e. On ) -> Pred ( _E , On , b ) = b )
22 predon 
 |-  ( c e. On -> Pred ( _E , On , c ) = c )
23 22 3ad2ant3 
 |-  ( ( a e. On /\ b e. On /\ c e. On ) -> Pred ( _E , On , c ) = c )
24 23 raleqdv 
 |-  ( ( a e. On /\ b e. On /\ c e. On ) -> ( A. f e. Pred ( _E , On , c ) th <-> A. f e. c th ) )
25 21 24 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 ) )
26 19 25 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 ) )
27 21 raleqdv 
 |-  ( ( a e. On /\ b e. On /\ c e. On ) -> ( A. e e. Pred ( _E , On , b ) ch <-> A. e e. b ch ) )
28 19 27 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 ) )
29 23 raleqdv 
 |-  ( ( a e. On /\ b e. On /\ c e. On ) -> ( A. f e. Pred ( _E , On , c ) ze <-> A. f e. c ze ) )
30 19 29 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 ) )
31 26 28 30 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 ) ) )
32 19 raleqdv 
 |-  ( ( a e. On /\ b e. On /\ c e. On ) -> ( A. d e. Pred ( _E , On , a ) ps <-> A. d e. a ps ) )
33 23 raleqdv 
 |-  ( ( a e. On /\ b e. On /\ c e. On ) -> ( A. f e. Pred ( _E , On , c ) ta <-> A. f e. c ta ) )
34 21 33 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 ) )
35 21 raleqdv 
 |-  ( ( a e. On /\ b e. On /\ c e. On ) -> ( A. e e. Pred ( _E , On , b ) si <-> A. e e. b si ) )
36 32 34 35 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 ) ) )
37 23 raleqdv 
 |-  ( ( a e. On /\ b e. On /\ c e. On ) -> ( A. f e. Pred ( _E , On , c ) et <-> A. f e. c et ) )
38 31 36 37 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 ) ) )
39 38 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 ) )
40 12 16 17 12 16 17 12 16 17 1 2 3 4 5 6 7 8 9 10 39 xpord3ind 
 |-  ( ( X e. On /\ Y e. On /\ Z e. On ) -> la )