Metamath Proof Explorer

Theorem nosep2o

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

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

Proof

Step Hyp Ref Expression
1 simp2 
 |-  ( ( A e. No /\ B e. No /\ A =/= B ) -> B e. No )
2 simp1 
 |-  ( ( A e. No /\ B e. No /\ A =/= B ) -> A e. No )
3 simp3 
 |-  ( ( A e. No /\ B e. No /\ A =/= B ) -> A =/= B )
4 3 necomd 
 |-  ( ( A e. No /\ B e. No /\ A =/= B ) -> B =/= A )
5 nosepne 
 |-  ( ( B e. No /\ A e. No /\ B =/= A ) -> ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) =/= ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) )
6 1 2 4 5 syl3anc 
 |-  ( ( A e. No /\ B e. No /\ A =/= B ) -> ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) =/= ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) )
7 6 adantr 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) -> ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) =/= ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) )
8 simpr 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) -> ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o )
9 7 8 neeqtrd 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) -> ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) =/= 2o )
10 9 neneqd 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) -> -. ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o )
11 simpl2 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) -> B e. No )
12 nofv 
 |-  ( B e. No -> ( ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = (/) \/ ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 1o \/ ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) )
13 11 12 syl 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) -> ( ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = (/) \/ ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 1o \/ ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) )
14 3orel3 
 |-  ( -. ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o -> ( ( ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = (/) \/ ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 1o \/ ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) -> ( ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = (/) \/ ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 1o ) ) )
15 10 13 14 sylc 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) -> ( ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = (/) \/ ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 1o ) )
16 15 orcomd 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) -> ( ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 1o \/ ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = (/) ) )
17 16 8 jca 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) -> ( ( ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 1o \/ ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = (/) ) /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) )
18 andir 
 |-  ( ( ( ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 1o \/ ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = (/) ) /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) <-> ( ( ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 1o /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) \/ ( ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = (/) /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) ) )
19 17 18 sylib 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) -> ( ( ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 1o /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) \/ ( ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = (/) /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) ) )
20 3mix2 
 |-  ( ( ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 1o /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) -> ( ( ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 1o /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = (/) ) \/ ( ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 1o /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) \/ ( ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = (/) /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) ) )
21 3mix3 
 |-  ( ( ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = (/) /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) -> ( ( ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 1o /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = (/) ) \/ ( ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 1o /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) \/ ( ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = (/) /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) ) )
22 20 21 jaoi 
 |-  ( ( ( ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 1o /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) \/ ( ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = (/) /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) ) -> ( ( ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 1o /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = (/) ) \/ ( ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 1o /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) \/ ( ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = (/) /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) ) )
23 19 22 syl 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) -> ( ( ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 1o /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = (/) ) \/ ( ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 1o /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) \/ ( ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = (/) /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) ) )
24 fvex 
 |-  ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) e. _V
25 fvex 
 |-  ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) e. _V
26 24 25 brtp 
 |-  ( ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) <-> ( ( ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 1o /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = (/) ) \/ ( ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 1o /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) \/ ( ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = (/) /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) ) )
27 23 26 sylibr 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) -> ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) )
28 simpl1 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) -> A e. No )
29 sltval2 
 |-  ( ( B e. No /\ A e. No ) -> ( B  ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) ) )
30 11 28 29 syl2anc 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) -> ( B  ( B ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) ) )
31 27 30 mpbird 
 |-  ( ( ( A e. No /\ B e. No /\ A =/= B ) /\ ( A ` |^| { x e. On | ( B ` x ) =/= ( A ` x ) } ) = 2o ) -> B