Metamath Proof Explorer

Theorem nosep1o

Description: If the value of a surreal at a separator is 1o then the surreal is lesser. (Contributed by Scott Fenton, 7-Dec-2021)

Ref Expression
Assertion nosep1o 
|- ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o ) -> A

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o ) -> ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o )
2 nosepne 
 |-  ( ( A e. No /\ B e. No /\ A =/= B ) -> ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) =/= ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) )
3 2 adantr 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o ) -> ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) =/= ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) )
4 1 3 eqnetrrd 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o ) -> 1o =/= ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) )
5 4 necomd 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o ) -> ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) =/= 1o )
6 5 neneqd 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o ) -> -. ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o )
7 simpl2 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o ) -> B e. No )
8 nofv 
 |-  ( B e. No -> ( ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) \/ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o \/ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) )
9 7 8 syl 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o ) -> ( ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) \/ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o \/ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) )
10 3orel2 
 |-  ( -. ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o -> ( ( ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) \/ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o \/ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) -> ( ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) \/ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) ) )
11 6 9 10 sylc 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o ) -> ( ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) \/ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) )
12 eqid 
 |-  1o = 1o
13 11 12 jctil 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o ) -> ( 1o = 1o /\ ( ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) \/ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) ) )
14 andi 
 |-  ( ( 1o = 1o /\ ( ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) \/ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) ) <-> ( ( 1o = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) ) \/ ( 1o = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) ) )
15 13 14 sylib 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o ) -> ( ( 1o = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) ) \/ ( 1o = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) ) )
16 3mix1 
 |-  ( ( 1o = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) ) -> ( ( 1o = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) ) \/ ( 1o = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) \/ ( 1o = (/) /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) ) )
17 3mix2 
 |-  ( ( 1o = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) -> ( ( 1o = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) ) \/ ( 1o = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) \/ ( 1o = (/) /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) ) )
18 16 17 jaoi 
 |-  ( ( ( 1o = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) ) \/ ( 1o = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) ) -> ( ( 1o = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) ) \/ ( 1o = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) \/ ( 1o = (/) /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) ) )
19 15 18 syl 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o ) -> ( ( 1o = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) ) \/ ( 1o = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) \/ ( 1o = (/) /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) ) )
20 1oex 
 |-  1o e. _V
21 fvex 
 |-  ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) e. _V
22 20 21 brtp 
 |-  ( 1o { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) <-> ( ( 1o = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) ) \/ ( 1o = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) \/ ( 1o = (/) /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) ) )
23 19 22 sylibr 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o ) -> 1o { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) )
24 1 23 eqbrtrd 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o ) -> ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) )
25 simpl1 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o ) -> A e. No )
26 sltval2 
 |-  ( ( A e. No /\ B e. No ) -> ( A  ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) ) )
27 25 7 26 syl2anc 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o ) -> ( A  ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) ) )
28 24 27 mpbird 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o ) -> A