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	⊢ ( 𝐴 ∈ No → 𝐴 <s ( 𝐴 ∪ { ⟨ dom 𝐴 , 2o ⟩ } ) )

Proof

Step	Hyp	Ref	Expression
1		nodmord	⊢ ( 𝐴 ∈ No → Ord dom 𝐴 )
2		ordirr	⊢ ( Ord dom 𝐴 → ¬ dom 𝐴 ∈ dom 𝐴 )
3	1 2	syl	⊢ ( 𝐴 ∈ No → ¬ dom 𝐴 ∈ dom 𝐴 )
4		ndmfv	⊢ ( ¬ dom 𝐴 ∈ dom 𝐴 → ( 𝐴 ‘ dom 𝐴 ) = ∅ )
5	3 4	syl	⊢ ( 𝐴 ∈ No → ( 𝐴 ‘ dom 𝐴 ) = ∅ )
6		nofun	⊢ ( 𝐴 ∈ No → Fun 𝐴 )
7		funfn	⊢ ( Fun 𝐴 ↔ 𝐴 Fn dom 𝐴 )
8	6 7	sylib	⊢ ( 𝐴 ∈ No → 𝐴 Fn dom 𝐴 )
9		nodmon	⊢ ( 𝐴 ∈ No → dom 𝐴 ∈ On )
10		2on	⊢ 2o ∈ On
11		fnsng	⊢ ( ( dom 𝐴 ∈ On ∧ 2o ∈ On ) → { ⟨ dom 𝐴 , 2o ⟩ } Fn { dom 𝐴 } )
12	9 10 11	sylancl	⊢ ( 𝐴 ∈ No → { ⟨ dom 𝐴 , 2o ⟩ } Fn { dom 𝐴 } )
13		disjsn	⊢ ( ( dom 𝐴 ∩ { dom 𝐴 } ) = ∅ ↔ ¬ dom 𝐴 ∈ dom 𝐴 )
14	3 13	sylibr	⊢ ( 𝐴 ∈ No → ( dom 𝐴 ∩ { dom 𝐴 } ) = ∅ )
15		snidg	⊢ ( dom 𝐴 ∈ On → dom 𝐴 ∈ { dom 𝐴 } )
16	9 15	syl	⊢ ( 𝐴 ∈ No → dom 𝐴 ∈ { dom 𝐴 } )
17		fvun2	⊢ ( ( 𝐴 Fn dom 𝐴 ∧ { ⟨ dom 𝐴 , 2o ⟩ } Fn { dom 𝐴 } ∧ ( ( dom 𝐴 ∩ { dom 𝐴 } ) = ∅ ∧ dom 𝐴 ∈ { dom 𝐴 } ) ) → ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 2o ⟩ } ) ‘ dom 𝐴 ) = ( { ⟨ dom 𝐴 , 2o ⟩ } ‘ dom 𝐴 ) )
18	8 12 14 16 17	syl112anc	⊢ ( 𝐴 ∈ No → ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 2o ⟩ } ) ‘ dom 𝐴 ) = ( { ⟨ dom 𝐴 , 2o ⟩ } ‘ dom 𝐴 ) )
19		fvsng	⊢ ( ( dom 𝐴 ∈ On ∧ 2o ∈ On ) → ( { ⟨ dom 𝐴 , 2o ⟩ } ‘ dom 𝐴 ) = 2o )
20	9 10 19	sylancl	⊢ ( 𝐴 ∈ No → ( { ⟨ dom 𝐴 , 2o ⟩ } ‘ dom 𝐴 ) = 2o )
21	18 20	eqtrd	⊢ ( 𝐴 ∈ No → ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 2o ⟩ } ) ‘ dom 𝐴 ) = 2o )
22	5 21	jca	⊢ ( 𝐴 ∈ No → ( ( 𝐴 ‘ dom 𝐴 ) = ∅ ∧ ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 2o ⟩ } ) ‘ dom 𝐴 ) = 2o ) )
23	22	3mix3d	⊢ ( 𝐴 ∈ No → ( ( ( 𝐴 ‘ dom 𝐴 ) = 1o ∧ ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 2o ⟩ } ) ‘ dom 𝐴 ) = ∅ ) ∨ ( ( 𝐴 ‘ dom 𝐴 ) = 1o ∧ ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 2o ⟩ } ) ‘ dom 𝐴 ) = 2o ) ∨ ( ( 𝐴 ‘ dom 𝐴 ) = ∅ ∧ ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 2o ⟩ } ) ‘ dom 𝐴 ) = 2o ) ) )
24		fvex	⊢ ( 𝐴 ‘ dom 𝐴 ) ∈ V
25		fvex	⊢ ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 2o ⟩ } ) ‘ dom 𝐴 ) ∈ V
26	24 25	brtp	⊢ ( ( 𝐴 ‘ dom 𝐴 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 2o ⟩ } ) ‘ dom 𝐴 ) ↔ ( ( ( 𝐴 ‘ dom 𝐴 ) = 1o ∧ ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 2o ⟩ } ) ‘ dom 𝐴 ) = ∅ ) ∨ ( ( 𝐴 ‘ dom 𝐴 ) = 1o ∧ ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 2o ⟩ } ) ‘ dom 𝐴 ) = 2o ) ∨ ( ( 𝐴 ‘ dom 𝐴 ) = ∅ ∧ ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 2o ⟩ } ) ‘ dom 𝐴 ) = 2o ) ) )
27	23 26	sylibr	⊢ ( 𝐴 ∈ No → ( 𝐴 ‘ dom 𝐴 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 2o ⟩ } ) ‘ dom 𝐴 ) )
28	10	elexi	⊢ 2o ∈ V
29	28	prid2	⊢ 2o ∈ { 1o , 2o }
30	29	noextenddif	⊢ ( 𝐴 ∈ No → ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 2o ⟩ } ) ‘ 𝑥 ) } = dom 𝐴 )
31	30	fveq2d	⊢ ( 𝐴 ∈ No → ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 2o ⟩ } ) ‘ 𝑥 ) } ) = ( 𝐴 ‘ dom 𝐴 ) )
32	30	fveq2d	⊢ ( 𝐴 ∈ No → ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 2o ⟩ } ) ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 2o ⟩ } ) ‘ 𝑥 ) } ) = ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 2o ⟩ } ) ‘ dom 𝐴 ) )
33	27 31 32	3brtr4d	⊢ ( 𝐴 ∈ No → ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 2o ⟩ } ) ‘ 𝑥 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 2o ⟩ } ) ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 2o ⟩ } ) ‘ 𝑥 ) } ) )
34	29	noextend	⊢ ( 𝐴 ∈ No → ( 𝐴 ∪ { ⟨ dom 𝐴 , 2o ⟩ } ) ∈ No )
35		ltsval2	⊢ ( ( 𝐴 ∈ No ∧ ( 𝐴 ∪ { ⟨ dom 𝐴 , 2o ⟩ } ) ∈ No ) → ( 𝐴 <s ( 𝐴 ∪ { ⟨ dom 𝐴 , 2o ⟩ } ) ↔ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 2o ⟩ } ) ‘ 𝑥 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 2o ⟩ } ) ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 2o ⟩ } ) ‘ 𝑥 ) } ) ) )
36	34 35	mpdan	⊢ ( 𝐴 ∈ No → ( 𝐴 <s ( 𝐴 ∪ { ⟨ dom 𝐴 , 2o ⟩ } ) ↔ ( 𝐴 ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 2o ⟩ } ) ‘ 𝑥 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 2o ⟩ } ) ‘ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 2o ⟩ } ) ‘ 𝑥 ) } ) ) )
37	33 36	mpbird	⊢ ( 𝐴 ∈ No → 𝐴 <s ( 𝐴 ∪ { ⟨ dom 𝐴 , 2o ⟩ } ) )