Metamath Proof Explorer

Theorem sltval

Description: The value of the surreal less than relationship. (Contributed by Scott Fenton, 14-Jun-2011)

Ref Expression
Assertion sltval 
|- ( ( A e. No /\ B e. No ) -> ( A  E. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) ) )

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( f = A -> ( f e. No <-> A e. No ) )
2 1 anbi1d 
 |-  ( f = A -> ( ( f e. No /\ g e. No ) <-> ( A e. No /\ g e. No ) ) )
3 fveq1 
 |-  ( f = A -> ( f ` y ) = ( A ` y ) )
4 3 eqeq1d 
 |-  ( f = A -> ( ( f ` y ) = ( g ` y ) <-> ( A ` y ) = ( g ` y ) ) )
5 4 ralbidv 
 |-  ( f = A -> ( A. y e. x ( f ` y ) = ( g ` y ) <-> A. y e. x ( A ` y ) = ( g ` y ) ) )
6 fveq1 
 |-  ( f = A -> ( f ` x ) = ( A ` x ) )
7 6 breq1d 
 |-  ( f = A -> ( ( f ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( g ` x ) <-> ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( g ` x ) ) )
8 5 7 anbi12d 
 |-  ( f = A -> ( ( A. y e. x ( f ` y ) = ( g ` y ) /\ ( f ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( g ` x ) ) <-> ( A. y e. x ( A ` y ) = ( g ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( g ` x ) ) ) )
9 8 rexbidv 
 |-  ( f = A -> ( E. x e. On ( A. y e. x ( f ` y ) = ( g ` y ) /\ ( f ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( g ` x ) ) <-> E. x e. On ( A. y e. x ( A ` y ) = ( g ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( g ` x ) ) ) )
10 2 9 anbi12d 
 |-  ( f = A -> ( ( ( f e. No /\ g e. No ) /\ E. x e. On ( A. y e. x ( f ` y ) = ( g ` y ) /\ ( f ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( g ` x ) ) ) <-> ( ( A e. No /\ g e. No ) /\ E. x e. On ( A. y e. x ( A ` y ) = ( g ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( g ` x ) ) ) ) )
11 eleq1 
 |-  ( g = B -> ( g e. No <-> B e. No ) )
12 11 anbi2d 
 |-  ( g = B -> ( ( A e. No /\ g e. No ) <-> ( A e. No /\ B e. No ) ) )
13 fveq1 
 |-  ( g = B -> ( g ` y ) = ( B ` y ) )
14 13 eqeq2d 
 |-  ( g = B -> ( ( A ` y ) = ( g ` y ) <-> ( A ` y ) = ( B ` y ) ) )
15 14 ralbidv 
 |-  ( g = B -> ( A. y e. x ( A ` y ) = ( g ` y ) <-> A. y e. x ( A ` y ) = ( B ` y ) ) )
16 fveq1 
 |-  ( g = B -> ( g ` x ) = ( B ` x ) )
17 16 breq2d 
 |-  ( g = B -> ( ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( g ` x ) <-> ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) )
18 15 17 anbi12d 
 |-  ( g = B -> ( ( A. y e. x ( A ` y ) = ( g ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( g ` x ) ) <-> ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) ) )
19 18 rexbidv 
 |-  ( g = B -> ( E. x e. On ( A. y e. x ( A ` y ) = ( g ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( g ` x ) ) <-> E. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) ) )
20 12 19 anbi12d 
 |-  ( g = B -> ( ( ( A e. No /\ g e. No ) /\ E. x e. On ( A. y e. x ( A ` y ) = ( g ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( g ` x ) ) ) <-> ( ( A e. No /\ B e. No ) /\ E. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) ) ) )
21 df-slt 
 |-  . | ( ( f e. No /\ g e. No ) /\ E. x e. On ( A. y e. x ( f ` y ) = ( g ` y ) /\ ( f ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( g ` x ) ) ) }
22 10 20 21 brabg 
 |-  ( ( A e. No /\ B e. No ) -> ( A  ( ( A e. No /\ B e. No ) /\ E. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) ) ) )
23 22 bianabs 
 |-  ( ( A e. No /\ B e. No ) -> ( A  E. x e. On ( A. y e. x ( A ` y ) = ( B ` y ) /\ ( A ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` x ) ) ) )