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 ⊢ A ∈ No → A < s A ∪ dom ⁡ A 2 𝑜

Proof

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