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	eqtrid	⊢ ( 𝐴 ∈ 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		onsuc	⊢ ( 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	eqtrid	⊢ ( 𝐴 ∈ 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 )