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

Proof

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