Metamath Proof Explorer

Theorem noextendgt

Description: Extending a surreal with a positive sign results in a bigger surreal. (Contributed by Scott Fenton, 22-Nov-2021)

Ref Expression
Assertion noextendgt 
|- ( A e. No -> A . } ) )

Proof

Step Hyp Ref Expression
1 nodmord 
 |-  ( A e. No -> Ord dom A )
2 ordirr 
 |-  ( Ord dom A -> -. dom A e. dom A )
3 1 2 syl 
 |-  ( A e. No -> -. dom A e. dom A )
4 ndmfv 
 |-  ( -. dom A e. dom A -> ( A ` dom A ) = (/) )
5 3 4 syl 
 |-  ( A e. No -> ( A ` dom A ) = (/) )
6 nofun 
 |-  ( A e. No -> Fun A )
7 funfn 
 |-  ( Fun A <-> A Fn dom A )
8 6 7 sylib 
 |-  ( A e. No -> A Fn dom A )
9 nodmon 
 |-  ( A e. No -> dom A e. On )
10 2on 
 |-  2o e. On
11 fnsng 
 |-  ( ( dom A e. On /\ 2o e. On ) -> { <. dom A , 2o >. } Fn { dom A } )
12 9 10 11 sylancl 
 |-  ( A e. No -> { <. dom A , 2o >. } Fn { dom A } )
13 disjsn 
 |-  ( ( dom A i^i { dom A } ) = (/) <-> -. dom A e. dom A )
14 3 13 sylibr 
 |-  ( A e. No -> ( dom A i^i { dom A } ) = (/) )
15 snidg 
 |-  ( dom A e. On -> dom A e. { dom A } )
16 9 15 syl 
 |-  ( A e. No -> dom A e. { dom A } )
17 fvun2 
 |-  ( ( A Fn dom A /\ { <. dom A , 2o >. } Fn { dom A } /\ ( ( dom A i^i { dom A } ) = (/) /\ dom A e. { dom A } ) ) -> ( ( A u. { <. dom A , 2o >. } ) ` dom A ) = ( { <. dom A , 2o >. } ` dom A ) )
18 8 12 14 16 17 syl112anc 
 |-  ( A e. No -> ( ( A u. { <. dom A , 2o >. } ) ` dom A ) = ( { <. dom A , 2o >. } ` dom A ) )
19 fvsng 
 |-  ( ( dom A e. On /\ 2o e. On ) -> ( { <. dom A , 2o >. } ` dom A ) = 2o )
20 9 10 19 sylancl 
 |-  ( A e. No -> ( { <. dom A , 2o >. } ` dom A ) = 2o )
21 18 20 eqtrd 
 |-  ( A e. No -> ( ( A u. { <. dom A , 2o >. } ) ` dom A ) = 2o )
22 5 21 jca 
 |-  ( A e. No -> ( ( A ` dom A ) = (/) /\ ( ( A u. { <. dom A , 2o >. } ) ` dom A ) = 2o ) )
23 22 3mix3d 
 |-  ( A e. No -> ( ( ( A ` dom A ) = 1o /\ ( ( A u. { <. dom A , 2o >. } ) ` dom A ) = (/) ) \/ ( ( A ` dom A ) = 1o /\ ( ( A u. { <. dom A , 2o >. } ) ` dom A ) = 2o ) \/ ( ( A ` dom A ) = (/) /\ ( ( A u. { <. dom A , 2o >. } ) ` dom A ) = 2o ) ) )
24 fvex 
 |-  ( A ` dom A ) e. _V
25 fvex 
 |-  ( ( A u. { <. dom A , 2o >. } ) ` dom A ) e. _V
26 24 25 brtp 
 |-  ( ( A ` dom A ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( A u. { <. dom A , 2o >. } ) ` dom A ) <-> ( ( ( A ` dom A ) = 1o /\ ( ( A u. { <. dom A , 2o >. } ) ` dom A ) = (/) ) \/ ( ( A ` dom A ) = 1o /\ ( ( A u. { <. dom A , 2o >. } ) ` dom A ) = 2o ) \/ ( ( A ` dom A ) = (/) /\ ( ( A u. { <. dom A , 2o >. } ) ` dom A ) = 2o ) ) )
27 23 26 sylibr 
 |-  ( A e. No -> ( A ` dom A ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( A u. { <. dom A , 2o >. } ) ` dom A ) )
28 10 elexi 
 |-  2o e. _V
29 28 prid2 
 |-  2o e. { 1o , 2o }
30 29 noextenddif 
 |-  ( A e. No -> |^| { x e. On | ( A ` x ) =/= ( ( A u. { <. dom A , 2o >. } ) ` x ) } = dom A )
31 30 fveq2d 
 |-  ( A e. No -> ( A ` |^| { x e. On | ( A ` x ) =/= ( ( A u. { <. dom A , 2o >. } ) ` x ) } ) = ( A ` dom A ) )
32 30 fveq2d 
 |-  ( A e. No -> ( ( A u. { <. dom A , 2o >. } ) ` |^| { x e. On | ( A ` x ) =/= ( ( A u. { <. dom A , 2o >. } ) ` x ) } ) = ( ( A u. { <. dom A , 2o >. } ) ` dom A ) )
33 27 31 32 3brtr4d 
 |-  ( A e. No -> ( A ` |^| { x e. On | ( A ` x ) =/= ( ( A u. { <. dom A , 2o >. } ) ` x ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( A u. { <. dom A , 2o >. } ) ` |^| { x e. On | ( A ` x ) =/= ( ( A u. { <. dom A , 2o >. } ) ` x ) } ) )
34 29 noextend 
 |-  ( A e. No -> ( A u. { <. dom A , 2o >. } ) e. No )
35 sltval2 
 |-  ( ( A e. No /\ ( A u. { <. dom A , 2o >. } ) e. No ) -> ( A . } ) <-> ( A ` |^| { x e. On | ( A ` x ) =/= ( ( A u. { <. dom A , 2o >. } ) ` x ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( A u. { <. dom A , 2o >. } ) ` |^| { x e. On | ( A ` x ) =/= ( ( A u. { <. dom A , 2o >. } ) ` x ) } ) ) )
36 34 35 mpdan 
 |-  ( A e. No -> ( A . } ) <-> ( A ` |^| { x e. On | ( A ` x ) =/= ( ( A u. { <. dom A , 2o >. } ) ` x ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( ( A u. { <. dom A , 2o >. } ) ` |^| { x e. On | ( A ` x ) =/= ( ( A u. { <. dom A , 2o >. } ) ` x ) } ) ) )
37 33 36 mpbird 
 |-  ( A e. No -> A . } ) )