Metamath Proof Explorer

Theorem no2indslem

Description: Double induction on surreals with explicit notation for the relationships. (Contributed by Scott Fenton, 22-Aug-2024)

Ref Expression
Hypotheses no2indslem.a 
|- R = { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) }
no2indslem.1 
|- ( x = z -> ( ph <-> ps ) )
no2indslem.2 
|- ( y = w -> ( ps <-> ch ) )
no2indslem.3 
|- ( x = z -> ( th <-> ch ) )
no2indslem.4 
|- ( x = A -> ( ph <-> ta ) )
no2indslem.5 
|- ( y = B -> ( ta <-> et ) )
no2indslem.i 
|- ( ( x e. No /\ y e. No ) -> ( ( A. z e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. w e. ( ( _Left ` y ) u. ( _Right ` y ) ) ch /\ A. z e. ( ( _Left ` x ) u. ( _Right ` x ) ) ps /\ A. w e. ( ( _Left ` y ) u. ( _Right ` y ) ) th ) -> ph ) )
Assertion no2indslem 
|- ( ( A e. No /\ B e. No ) -> et )

Proof

Step Hyp Ref Expression
1 no2indslem.a 
 |-  R = { <. a , b >. | a e. ( ( _Left ` b ) u. ( _Right ` b ) ) }
2 no2indslem.1 
 |-  ( x = z -> ( ph <-> ps ) )
3 no2indslem.2 
 |-  ( y = w -> ( ps <-> ch ) )
4 no2indslem.3 
 |-  ( x = z -> ( th <-> ch ) )
5 no2indslem.4 
 |-  ( x = A -> ( ph <-> ta ) )
6 no2indslem.5 
 |-  ( y = B -> ( ta <-> et ) )
7 no2indslem.i 
 |-  ( ( x e. No /\ y e. No ) -> ( ( A. z e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. w e. ( ( _Left ` y ) u. ( _Right ` y ) ) ch /\ A. z e. ( ( _Left ` x ) u. ( _Right ` x ) ) ps /\ A. w e. ( ( _Left ` y ) u. ( _Right ` y ) ) th ) -> ph ) )
8 1 lrrecfr 
 |-  R Fr No
9 1 lrrecpo 
 |-  R Po No
10 1 lrrecse 
 |-  R Se No
11 1 lrrecpred 
 |-  ( x e. No -> Pred ( R , No , x ) = ( ( _Left ` x ) u. ( _Right ` x ) ) )
12 11 adantr 
 |-  ( ( x e. No /\ y e. No ) -> Pred ( R , No , x ) = ( ( _Left ` x ) u. ( _Right ` x ) ) )
13 1 lrrecpred 
 |-  ( y e. No -> Pred ( R , No , y ) = ( ( _Left ` y ) u. ( _Right ` y ) ) )
14 13 adantl 
 |-  ( ( x e. No /\ y e. No ) -> Pred ( R , No , y ) = ( ( _Left ` y ) u. ( _Right ` y ) ) )
15 14 raleqdv 
 |-  ( ( x e. No /\ y e. No ) -> ( A. w e. Pred ( R , No , y ) ch <-> A. w e. ( ( _Left ` y ) u. ( _Right ` y ) ) ch ) )
16 12 15 raleqbidv 
 |-  ( ( x e. No /\ y e. No ) -> ( A. z e. Pred ( R , No , x ) A. w e. Pred ( R , No , y ) ch <-> A. z e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. w e. ( ( _Left ` y ) u. ( _Right ` y ) ) ch ) )
17 12 raleqdv 
 |-  ( ( x e. No /\ y e. No ) -> ( A. z e. Pred ( R , No , x ) ps <-> A. z e. ( ( _Left ` x ) u. ( _Right ` x ) ) ps ) )
18 14 raleqdv 
 |-  ( ( x e. No /\ y e. No ) -> ( A. w e. Pred ( R , No , y ) th <-> A. w e. ( ( _Left ` y ) u. ( _Right ` y ) ) th ) )
19 16 17 18 3anbi123d 
 |-  ( ( x e. No /\ y e. No ) -> ( ( A. z e. Pred ( R , No , x ) A. w e. Pred ( R , No , y ) ch /\ A. z e. Pred ( R , No , x ) ps /\ A. w e. Pred ( R , No , y ) th ) <-> ( A. z e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. w e. ( ( _Left ` y ) u. ( _Right ` y ) ) ch /\ A. z e. ( ( _Left ` x ) u. ( _Right ` x ) ) ps /\ A. w e. ( ( _Left ` y ) u. ( _Right ` y ) ) th ) ) )
20 19 7 sylbid 
 |-  ( ( x e. No /\ y e. No ) -> ( ( A. z e. Pred ( R , No , x ) A. w e. Pred ( R , No , y ) ch /\ A. z e. Pred ( R , No , x ) ps /\ A. w e. Pred ( R , No , y ) th ) -> ph ) )
21 8 9 10 8 9 10 2 3 4 5 6 20 xpord2ind 
 |-  ( ( A e. No /\ B e. No ) -> et )