Metamath Proof Explorer

Theorem noextendlt

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

Ref Expression
Assertion noextendlt 
|- ( A e. No -> ( A u. { <. dom A , 1o >. } )

Proof

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