Metamath Proof Explorer

Theorem noextend

Description: Extending a surreal by one sign value results in a new surreal. (Contributed by Scott Fenton, 22-Nov-2021)

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

Proof

Step Hyp Ref Expression
1 noextend.1 
 |-  X e. { 1o , 2o }
2 nofun 
 |-  ( A e. No -> Fun A )
3 dmexg 
 |-  ( A e. No -> dom A e. _V )
4 funsng 
 |-  ( ( dom A e. _V /\ X e. { 1o , 2o } ) -> Fun { <. dom A , X >. } )
5 3 1 4 sylancl 
 |-  ( A e. No -> Fun { <. dom A , X >. } )
6 1 elexi 
 |-  X e. _V
7 6 dmsnop 
 |-  dom { <. dom A , X >. } = { dom A }
8 7 ineq2i 
 |-  ( dom A i^i dom { <. dom A , X >. } ) = ( dom A i^i { dom A } )
9 nodmord 
 |-  ( A e. No -> Ord dom A )
10 ordirr 
 |-  ( Ord dom A -> -. dom A e. dom A )
11 9 10 syl 
 |-  ( A e. No -> -. dom A e. dom A )
12 disjsn 
 |-  ( ( dom A i^i { dom A } ) = (/) <-> -. dom A e. dom A )
13 11 12 sylibr 
 |-  ( A e. No -> ( dom A i^i { dom A } ) = (/) )
14 8 13 syl5eq 
 |-  ( A e. No -> ( dom A i^i dom { <. dom A , X >. } ) = (/) )
15 funun 
 |-  ( ( ( Fun A /\ Fun { <. dom A , X >. } ) /\ ( dom A i^i dom { <. dom A , X >. } ) = (/) ) -> Fun ( A u. { <. dom A , X >. } ) )
16 2 5 14 15 syl21anc 
 |-  ( A e. No -> Fun ( A u. { <. dom A , X >. } ) )
17 7 uneq2i 
 |-  ( dom A u. dom { <. dom A , X >. } ) = ( dom A u. { dom A } )
18 dmun 
 |-  dom ( A u. { <. dom A , X >. } ) = ( dom A u. dom { <. dom A , X >. } )
19 df-suc 
 |-  suc dom A = ( dom A u. { dom A } )
20 17 18 19 3eqtr4i 
 |-  dom ( A u. { <. dom A , X >. } ) = suc dom A
21 nodmon 
 |-  ( A e. No -> dom A e. On )
22 suceloni 
 |-  ( dom A e. On -> suc dom A e. On )
23 21 22 syl 
 |-  ( A e. No -> suc dom A e. On )
24 20 23 eqeltrid 
 |-  ( A e. No -> dom ( A u. { <. dom A , X >. } ) e. On )
25 rnun 
 |-  ran ( A u. { <. dom A , X >. } ) = ( ran A u. ran { <. dom A , X >. } )
26 rnsnopg 
 |-  ( dom A e. _V -> ran { <. dom A , X >. } = { X } )
27 3 26 syl 
 |-  ( A e. No -> ran { <. dom A , X >. } = { X } )
28 27 uneq2d 
 |-  ( A e. No -> ( ran A u. ran { <. dom A , X >. } ) = ( ran A u. { X } ) )
29 25 28 syl5eq 
 |-  ( A e. No -> ran ( A u. { <. dom A , X >. } ) = ( ran A u. { X } ) )
30 norn 
 |-  ( A e. No -> ran A C_ { 1o , 2o } )
31 snssi 
 |-  ( X e. { 1o , 2o } -> { X } C_ { 1o , 2o } )
32 1 31 mp1i 
 |-  ( A e. No -> { X } C_ { 1o , 2o } )
33 30 32 unssd 
 |-  ( A e. No -> ( ran A u. { X } ) C_ { 1o , 2o } )
34 29 33 eqsstrd 
 |-  ( A e. No -> ran ( A u. { <. dom A , X >. } ) C_ { 1o , 2o } )
35 elno2 
 |-  ( ( A u. { <. dom A , X >. } ) e. No <-> ( Fun ( A u. { <. dom A , X >. } ) /\ dom ( A u. { <. dom A , X >. } ) e. On /\ ran ( A u. { <. dom A , X >. } ) C_ { 1o , 2o } ) )
36 16 24 34 35 syl3anbrc 
 |-  ( A e. No -> ( A u. { <. dom A , X >. } ) e. No )