Metamath Proof Explorer


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 sltval2 ( ( 𝐴 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 ⟩ } ) )