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 𝑋 ∈ { 1o , 2o }
Assertion noextend ( 𝐴 No → ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ∈ No )

Proof

Step Hyp Ref Expression
1 noextend.1 𝑋 ∈ { 1o , 2o }
2 nofun ( 𝐴 No → Fun 𝐴 )
3 dmexg ( 𝐴 No → dom 𝐴 ∈ V )
4 funsng ( ( dom 𝐴 ∈ V ∧ 𝑋 ∈ { 1o , 2o } ) → Fun { ⟨ dom 𝐴 , 𝑋 ⟩ } )
5 3 1 4 sylancl ( 𝐴 No → Fun { ⟨ dom 𝐴 , 𝑋 ⟩ } )
6 1 elexi 𝑋 ∈ V
7 6 dmsnop dom { ⟨ dom 𝐴 , 𝑋 ⟩ } = { dom 𝐴 }
8 7 ineq2i ( dom 𝐴 ∩ dom { ⟨ dom 𝐴 , 𝑋 ⟩ } ) = ( dom 𝐴 ∩ { dom 𝐴 } )
9 nodmord ( 𝐴 No → Ord dom 𝐴 )
10 ordirr ( Ord dom 𝐴 → ¬ dom 𝐴 ∈ dom 𝐴 )
11 9 10 syl ( 𝐴 No → ¬ dom 𝐴 ∈ dom 𝐴 )
12 disjsn ( ( dom 𝐴 ∩ { dom 𝐴 } ) = ∅ ↔ ¬ dom 𝐴 ∈ dom 𝐴 )
13 11 12 sylibr ( 𝐴 No → ( dom 𝐴 ∩ { dom 𝐴 } ) = ∅ )
14 8 13 syl5eq ( 𝐴 No → ( dom 𝐴 ∩ dom { ⟨ dom 𝐴 , 𝑋 ⟩ } ) = ∅ )
15 funun ( ( ( Fun 𝐴 ∧ Fun { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ∧ ( dom 𝐴 ∩ dom { ⟨ dom 𝐴 , 𝑋 ⟩ } ) = ∅ ) → Fun ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) )
16 2 5 14 15 syl21anc ( 𝐴 No → Fun ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) )
17 7 uneq2i ( dom 𝐴 ∪ dom { ⟨ dom 𝐴 , 𝑋 ⟩ } ) = ( dom 𝐴 ∪ { dom 𝐴 } )
18 dmun dom ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) = ( dom 𝐴 ∪ dom { ⟨ dom 𝐴 , 𝑋 ⟩ } )
19 df-suc suc dom 𝐴 = ( dom 𝐴 ∪ { dom 𝐴 } )
20 17 18 19 3eqtr4i dom ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) = suc dom 𝐴
21 nodmon ( 𝐴 No → dom 𝐴 ∈ On )
22 suceloni ( dom 𝐴 ∈ On → suc dom 𝐴 ∈ On )
23 21 22 syl ( 𝐴 No → suc dom 𝐴 ∈ On )
24 20 23 eqeltrid ( 𝐴 No → dom ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ∈ On )
25 rnun ran ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) = ( ran 𝐴 ∪ ran { ⟨ dom 𝐴 , 𝑋 ⟩ } )
26 rnsnopg ( dom 𝐴 ∈ V → ran { ⟨ dom 𝐴 , 𝑋 ⟩ } = { 𝑋 } )
27 3 26 syl ( 𝐴 No → ran { ⟨ dom 𝐴 , 𝑋 ⟩ } = { 𝑋 } )
28 27 uneq2d ( 𝐴 No → ( ran 𝐴 ∪ ran { ⟨ dom 𝐴 , 𝑋 ⟩ } ) = ( ran 𝐴 ∪ { 𝑋 } ) )
29 25 28 syl5eq ( 𝐴 No → ran ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) = ( ran 𝐴 ∪ { 𝑋 } ) )
30 norn ( 𝐴 No → ran 𝐴 ⊆ { 1o , 2o } )
31 snssi ( 𝑋 ∈ { 1o , 2o } → { 𝑋 } ⊆ { 1o , 2o } )
32 1 31 mp1i ( 𝐴 No → { 𝑋 } ⊆ { 1o , 2o } )
33 30 32 unssd ( 𝐴 No → ( ran 𝐴 ∪ { 𝑋 } ) ⊆ { 1o , 2o } )
34 29 33 eqsstrd ( 𝐴 No → ran ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ⊆ { 1o , 2o } )
35 elno2 ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ∈ No ↔ ( Fun ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ∧ dom ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ∈ On ∧ ran ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ⊆ { 1o , 2o } ) )
36 16 24 34 35 syl3anbrc ( 𝐴 No → ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ∈ No )