Metamath Proof Explorer


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 syl5eq ( 𝐴 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 sltval2 ( ( ( 𝐴 ∪ { ⟨ 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 𝐴 )