Metamath Proof Explorer

Theorem no3inds

Description: Triple induction over surreal numbers. (Contributed by Scott Fenton, 9-Oct-2024)

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

Proof

Step Hyp Ref Expression
1 no3inds.1 
 |-  ( a = d -> ( ph <-> ps ) )
2 no3inds.2 
 |-  ( b = e -> ( ps <-> ch ) )
3 no3inds.3 
 |-  ( c = f -> ( ch <-> th ) )
4 no3inds.4 
 |-  ( a = d -> ( ta <-> th ) )
5 no3inds.5 
 |-  ( b = e -> ( et <-> ta ) )
6 no3inds.6 
 |-  ( b = e -> ( ze <-> th ) )
7 no3inds.7 
 |-  ( c = f -> ( si <-> ta ) )
8 no3inds.8 
 |-  ( a = X -> ( ph <-> rh ) )
9 no3inds.9 
 |-  ( b = Y -> ( rh <-> mu ) )
10 no3inds.10 
 |-  ( c = Z -> ( mu <-> la ) )
11 no3inds.i 
 |-  ( ( a e. No /\ b e. No /\ c e. No ) -> ( ( ( A. d e. ( ( _L ` a ) u. ( _R ` a ) ) A. e e. ( ( _L ` b ) u. ( _R ` b ) ) A. f e. ( ( _L ` c ) u. ( _R ` c ) ) th /\ A. d e. ( ( _L ` a ) u. ( _R ` a ) ) A. e e. ( ( _L ` b ) u. ( _R ` b ) ) ch /\ A. d e. ( ( _L ` a ) u. ( _R ` a ) ) A. f e. ( ( _L ` c ) u. ( _R ` c ) ) ze ) /\ ( A. d e. ( ( _L ` a ) u. ( _R ` a ) ) ps /\ A. e e. ( ( _L ` b ) u. ( _R ` b ) ) A. f e. ( ( _L ` c ) u. ( _R ` c ) ) ta /\ A. e e. ( ( _L ` b ) u. ( _R ` b ) ) si ) /\ A. f e. ( ( _L ` c ) u. ( _R ` c ) ) et ) -> ph ) )
12 eqid 
 |-  { <. z , w >. | ( z e. ( ( No X. No ) X. No ) /\ w e. ( ( No X. No ) X. No ) /\ ( ( ( ( 1st ` ( 1st ` z ) ) { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } ( 1st ` ( 1st ` w ) ) \/ ( 1st ` ( 1st ` z ) ) = ( 1st ` ( 1st ` w ) ) ) /\ ( ( 2nd ` ( 1st ` z ) ) { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } ( 2nd ` ( 1st ` w ) ) \/ ( 2nd ` ( 1st ` z ) ) = ( 2nd ` ( 1st ` w ) ) ) /\ ( ( 2nd ` z ) { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } ( 2nd ` w ) \/ ( 2nd ` z ) = ( 2nd ` w ) ) ) /\ z =/= w ) ) } = { <. z , w >. | ( z e. ( ( No X. No ) X. No ) /\ w e. ( ( No X. No ) X. No ) /\ ( ( ( ( 1st ` ( 1st ` z ) ) { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } ( 1st ` ( 1st ` w ) ) \/ ( 1st ` ( 1st ` z ) ) = ( 1st ` ( 1st ` w ) ) ) /\ ( ( 2nd ` ( 1st ` z ) ) { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } ( 2nd ` ( 1st ` w ) ) \/ ( 2nd ` ( 1st ` z ) ) = ( 2nd ` ( 1st ` w ) ) ) /\ ( ( 2nd ` z ) { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } ( 2nd ` w ) \/ ( 2nd ` z ) = ( 2nd ` w ) ) ) /\ z =/= w ) ) }
13 eqid 
 |-  { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } = { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) }
14 13 lrrecfr 
 |-  { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } Fr No
15 13 lrrecpo 
 |-  { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } Po No
16 13 lrrecse 
 |-  { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } Se No
17 13 lrrecpred 
 |-  ( a e. No -> Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , a ) = ( ( _L ` a ) u. ( _R ` a ) ) )
18 17 3ad2ant1 
 |-  ( ( a e. No /\ b e. No /\ c e. No ) -> Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , a ) = ( ( _L ` a ) u. ( _R ` a ) ) )
19 13 lrrecpred 
 |-  ( b e. No -> Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , b ) = ( ( _L ` b ) u. ( _R ` b ) ) )
20 19 3ad2ant2 
 |-  ( ( a e. No /\ b e. No /\ c e. No ) -> Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , b ) = ( ( _L ` b ) u. ( _R ` b ) ) )
21 13 lrrecpred 
 |-  ( c e. No -> Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , c ) = ( ( _L ` c ) u. ( _R ` c ) ) )
22 21 3ad2ant3 
 |-  ( ( a e. No /\ b e. No /\ c e. No ) -> Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , c ) = ( ( _L ` c ) u. ( _R ` c ) ) )
23 22 raleqdv 
 |-  ( ( a e. No /\ b e. No /\ c e. No ) -> ( A. f e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , c ) th <-> A. f e. ( ( _L ` c ) u. ( _R ` c ) ) th ) )
24 20 23 raleqbidv 
 |-  ( ( a e. No /\ b e. No /\ c e. No ) -> ( A. e e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , b ) A. f e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , c ) th <-> A. e e. ( ( _L ` b ) u. ( _R ` b ) ) A. f e. ( ( _L ` c ) u. ( _R ` c ) ) th ) )
25 18 24 raleqbidv 
 |-  ( ( a e. No /\ b e. No /\ c e. No ) -> ( A. d e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , a ) A. e e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , b ) A. f e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , c ) th <-> A. d e. ( ( _L ` a ) u. ( _R ` a ) ) A. e e. ( ( _L ` b ) u. ( _R ` b ) ) A. f e. ( ( _L ` c ) u. ( _R ` c ) ) th ) )
26 20 raleqdv 
 |-  ( ( a e. No /\ b e. No /\ c e. No ) -> ( A. e e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , b ) ch <-> A. e e. ( ( _L ` b ) u. ( _R ` b ) ) ch ) )
27 18 26 raleqbidv 
 |-  ( ( a e. No /\ b e. No /\ c e. No ) -> ( A. d e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , a ) A. e e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , b ) ch <-> A. d e. ( ( _L ` a ) u. ( _R ` a ) ) A. e e. ( ( _L ` b ) u. ( _R ` b ) ) ch ) )
28 22 raleqdv 
 |-  ( ( a e. No /\ b e. No /\ c e. No ) -> ( A. f e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , c ) ze <-> A. f e. ( ( _L ` c ) u. ( _R ` c ) ) ze ) )
29 18 28 raleqbidv 
 |-  ( ( a e. No /\ b e. No /\ c e. No ) -> ( A. d e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , a ) A. f e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , c ) ze <-> A. d e. ( ( _L ` a ) u. ( _R ` a ) ) A. f e. ( ( _L ` c ) u. ( _R ` c ) ) ze ) )
30 25 27 29 3anbi123d 
 |-  ( ( a e. No /\ b e. No /\ c e. No ) -> ( ( A. d e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , a ) A. e e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , b ) A. f e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , c ) th /\ A. d e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , a ) A. e e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , b ) ch /\ A. d e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , a ) A. f e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , c ) ze ) <-> ( A. d e. ( ( _L ` a ) u. ( _R ` a ) ) A. e e. ( ( _L ` b ) u. ( _R ` b ) ) A. f e. ( ( _L ` c ) u. ( _R ` c ) ) th /\ A. d e. ( ( _L ` a ) u. ( _R ` a ) ) A. e e. ( ( _L ` b ) u. ( _R ` b ) ) ch /\ A. d e. ( ( _L ` a ) u. ( _R ` a ) ) A. f e. ( ( _L ` c ) u. ( _R ` c ) ) ze ) ) )
31 18 raleqdv 
 |-  ( ( a e. No /\ b e. No /\ c e. No ) -> ( A. d e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , a ) ps <-> A. d e. ( ( _L ` a ) u. ( _R ` a ) ) ps ) )
32 22 raleqdv 
 |-  ( ( a e. No /\ b e. No /\ c e. No ) -> ( A. f e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , c ) ta <-> A. f e. ( ( _L ` c ) u. ( _R ` c ) ) ta ) )
33 20 32 raleqbidv 
 |-  ( ( a e. No /\ b e. No /\ c e. No ) -> ( A. e e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , b ) A. f e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , c ) ta <-> A. e e. ( ( _L ` b ) u. ( _R ` b ) ) A. f e. ( ( _L ` c ) u. ( _R ` c ) ) ta ) )
34 20 raleqdv 
 |-  ( ( a e. No /\ b e. No /\ c e. No ) -> ( A. e e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , b ) si <-> A. e e. ( ( _L ` b ) u. ( _R ` b ) ) si ) )
35 31 33 34 3anbi123d 
 |-  ( ( a e. No /\ b e. No /\ c e. No ) -> ( ( A. d e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , a ) ps /\ A. e e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , b ) A. f e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , c ) ta /\ A. e e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , b ) si ) <-> ( A. d e. ( ( _L ` a ) u. ( _R ` a ) ) ps /\ A. e e. ( ( _L ` b ) u. ( _R ` b ) ) A. f e. ( ( _L ` c ) u. ( _R ` c ) ) ta /\ A. e e. ( ( _L ` b ) u. ( _R ` b ) ) si ) ) )
36 22 raleqdv 
 |-  ( ( a e. No /\ b e. No /\ c e. No ) -> ( A. f e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , c ) et <-> A. f e. ( ( _L ` c ) u. ( _R ` c ) ) et ) )
37 30 35 36 3anbi123d 
 |-  ( ( a e. No /\ b e. No /\ c e. No ) -> ( ( ( A. d e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , a ) A. e e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , b ) A. f e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , c ) th /\ A. d e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , a ) A. e e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , b ) ch /\ A. d e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , a ) A. f e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , c ) ze ) /\ ( A. d e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , a ) ps /\ A. e e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , b ) A. f e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , c ) ta /\ A. e e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , b ) si ) /\ A. f e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , c ) et ) <-> ( ( A. d e. ( ( _L ` a ) u. ( _R ` a ) ) A. e e. ( ( _L ` b ) u. ( _R ` b ) ) A. f e. ( ( _L ` c ) u. ( _R ` c ) ) th /\ A. d e. ( ( _L ` a ) u. ( _R ` a ) ) A. e e. ( ( _L ` b ) u. ( _R ` b ) ) ch /\ A. d e. ( ( _L ` a ) u. ( _R ` a ) ) A. f e. ( ( _L ` c ) u. ( _R ` c ) ) ze ) /\ ( A. d e. ( ( _L ` a ) u. ( _R ` a ) ) ps /\ A. e e. ( ( _L ` b ) u. ( _R ` b ) ) A. f e. ( ( _L ` c ) u. ( _R ` c ) ) ta /\ A. e e. ( ( _L ` b ) u. ( _R ` b ) ) si ) /\ A. f e. ( ( _L ` c ) u. ( _R ` c ) ) et ) ) )
38 37 11 sylbid 
 |-  ( ( a e. No /\ b e. No /\ c e. No ) -> ( ( ( A. d e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , a ) A. e e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , b ) A. f e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , c ) th /\ A. d e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , a ) A. e e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , b ) ch /\ A. d e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , a ) A. f e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , c ) ze ) /\ ( A. d e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , a ) ps /\ A. e e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , b ) A. f e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , c ) ta /\ A. e e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , b ) si ) /\ A. f e. Pred ( { <. x , y >. | x e. ( ( _L ` y ) u. ( _R ` y ) ) } , No , c ) et ) -> ph ) )
39 12 14 15 16 14 15 16 14 15 16 1 2 3 4 5 6 7 8 9 10 38 xpord3ind 
 |-  ( ( X e. No /\ Y e. No /\ Z e. No ) -> la )