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. ( ( _L ` b ) u. ( _R ` b ) ) }
no2indslem.b 
|- S = { <. c , d >. | ( c e. ( No X. No ) /\ d e. ( No X. No ) /\ ( ( ( 1st ` c ) R ( 1st ` d ) \/ ( 1st ` c ) = ( 1st ` d ) ) /\ ( ( 2nd ` c ) R ( 2nd ` d ) \/ ( 2nd ` c ) = ( 2nd ` d ) ) /\ c =/= d ) ) }
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. ( ( _L ` x ) u. ( _R ` x ) ) A. w e. ( ( _L ` y ) u. ( _R ` y ) ) ch /\ A. z e. ( ( _L ` x ) u. ( _R ` x ) ) ps /\ A. w e. ( ( _L ` y ) u. ( _R ` 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. ( ( _L ` b ) u. ( _R ` b ) ) }
2 no2indslem.b 
 |-  S = { <. c , d >. | ( c e. ( No X. No ) /\ d e. ( No X. No ) /\ ( ( ( 1st ` c ) R ( 1st ` d ) \/ ( 1st ` c ) = ( 1st ` d ) ) /\ ( ( 2nd ` c ) R ( 2nd ` d ) \/ ( 2nd ` c ) = ( 2nd ` d ) ) /\ c =/= d ) ) }
3 no2indslem.1 
 |-  ( x = z -> ( ph <-> ps ) )
4 no2indslem.2 
 |-  ( y = w -> ( ps <-> ch ) )
5 no2indslem.3 
 |-  ( x = z -> ( th <-> ch ) )
6 no2indslem.4 
 |-  ( x = A -> ( ph <-> ta ) )
7 no2indslem.5 
 |-  ( y = B -> ( ta <-> et ) )
8 no2indslem.i 
 |-  ( ( x e. No /\ y e. No ) -> ( ( A. z e. ( ( _L ` x ) u. ( _R ` x ) ) A. w e. ( ( _L ` y ) u. ( _R ` y ) ) ch /\ A. z e. ( ( _L ` x ) u. ( _R ` x ) ) ps /\ A. w e. ( ( _L ` y ) u. ( _R ` y ) ) th ) -> ph ) )
9 1 lrrecfr 
 |-  R Fr No
10 1 lrrecpo 
 |-  R Po No
11 1 lrrecse 
 |-  R Se No
12 1 lrrecpred 
 |-  ( x e. No -> Pred ( R , No , x ) = ( ( _L ` x ) u. ( _R ` x ) ) )
13 12 adantr 
 |-  ( ( x e. No /\ y e. No ) -> Pred ( R , No , x ) = ( ( _L ` x ) u. ( _R ` x ) ) )
14 1 lrrecpred 
 |-  ( y e. No -> Pred ( R , No , y ) = ( ( _L ` y ) u. ( _R ` y ) ) )
15 14 adantl 
 |-  ( ( x e. No /\ y e. No ) -> Pred ( R , No , y ) = ( ( _L ` y ) u. ( _R ` y ) ) )
16 15 raleqdv 
 |-  ( ( x e. No /\ y e. No ) -> ( A. w e. Pred ( R , No , y ) ch <-> A. w e. ( ( _L ` y ) u. ( _R ` y ) ) ch ) )
17 13 16 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. ( ( _L ` x ) u. ( _R ` x ) ) A. w e. ( ( _L ` y ) u. ( _R ` y ) ) ch ) )
18 13 raleqdv 
 |-  ( ( x e. No /\ y e. No ) -> ( A. z e. Pred ( R , No , x ) ps <-> A. z e. ( ( _L ` x ) u. ( _R ` x ) ) ps ) )
19 15 raleqdv 
 |-  ( ( x e. No /\ y e. No ) -> ( A. w e. Pred ( R , No , y ) th <-> A. w e. ( ( _L ` y ) u. ( _R ` y ) ) th ) )
20 17 18 19 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. ( ( _L ` x ) u. ( _R ` x ) ) A. w e. ( ( _L ` y ) u. ( _R ` y ) ) ch /\ A. z e. ( ( _L ` x ) u. ( _R ` x ) ) ps /\ A. w e. ( ( _L ` y ) u. ( _R ` y ) ) th ) ) )
21 20 8 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 ) )
22 2 9 10 11 9 10 11 3 4 5 6 7 21 xpord2ind 
 |-  ( ( A e. No /\ B e. No ) -> et )