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