Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  noextend Structured version   Visualization version   GIF version

Theorem noextend 33419
 Description: Extending a surreal by one sign value results in a new surreal. (Contributed by Scott Fenton, 22-Nov-2021.)
Hypothesis
Ref Expression
noextend.1 𝑋 ∈ {1o, 2o}
Assertion
Ref Expression
noextend (𝐴 No → (𝐴 ∪ {⟨dom 𝐴, 𝑋⟩}) ∈ No )

Proof of Theorem noextend
StepHypRef Expression
1 nofun 33402 . . 3 (𝐴 No → Fun 𝐴)
2 dmexg 7606 . . . 4 (𝐴 No → dom 𝐴 ∈ V)
3 noextend.1 . . . 4 𝑋 ∈ {1o, 2o}
4 funsng 6379 . . . 4 ((dom 𝐴 ∈ V ∧ 𝑋 ∈ {1o, 2o}) → Fun {⟨dom 𝐴, 𝑋⟩})
52, 3, 4sylancl 590 . . 3 (𝐴 No → Fun {⟨dom 𝐴, 𝑋⟩})
63elexi 3428 . . . . . 6 𝑋 ∈ V
76dmsnop 6038 . . . . 5 dom {⟨dom 𝐴, 𝑋⟩} = {dom 𝐴}
87ineq2i 4110 . . . 4 (dom 𝐴 ∩ dom {⟨dom 𝐴, 𝑋⟩}) = (dom 𝐴 ∩ {dom 𝐴})
9 nodmord 33406 . . . . . 6 (𝐴 No → Ord dom 𝐴)
10 ordirr 6180 . . . . . 6 (Ord dom 𝐴 → ¬ dom 𝐴 ∈ dom 𝐴)
119, 10syl 17 . . . . 5 (𝐴 No → ¬ dom 𝐴 ∈ dom 𝐴)
12 disjsn 4597 . . . . 5 ((dom 𝐴 ∩ {dom 𝐴}) = ∅ ↔ ¬ dom 𝐴 ∈ dom 𝐴)
1311, 12sylibr 237 . . . 4 (𝐴 No → (dom 𝐴 ∩ {dom 𝐴}) = ∅)
148, 13syl5eq 2806 . . 3 (𝐴 No → (dom 𝐴 ∩ dom {⟨dom 𝐴, 𝑋⟩}) = ∅)
15 funun 6374 . . 3 (((Fun 𝐴 ∧ Fun {⟨dom 𝐴, 𝑋⟩}) ∧ (dom 𝐴 ∩ dom {⟨dom 𝐴, 𝑋⟩}) = ∅) → Fun (𝐴 ∪ {⟨dom 𝐴, 𝑋⟩}))
161, 5, 14, 15syl21anc 837 . 2 (𝐴 No → Fun (𝐴 ∪ {⟨dom 𝐴, 𝑋⟩}))
177uneq2i 4061 . . . 4 (dom 𝐴 ∪ dom {⟨dom 𝐴, 𝑋⟩}) = (dom 𝐴 ∪ {dom 𝐴})
18 dmun 5743 . . . 4 dom (𝐴 ∪ {⟨dom 𝐴, 𝑋⟩}) = (dom 𝐴 ∪ dom {⟨dom 𝐴, 𝑋⟩})
19 df-suc 6168 . . . 4 suc dom 𝐴 = (dom 𝐴 ∪ {dom 𝐴})
2017, 18, 193eqtr4i 2792 . . 3 dom (𝐴 ∪ {⟨dom 𝐴, 𝑋⟩}) = suc dom 𝐴
21 nodmon 33403 . . . 4 (𝐴 No → dom 𝐴 ∈ On)
22 suceloni 7520 . . . 4 (dom 𝐴 ∈ On → suc dom 𝐴 ∈ On)
2321, 22syl 17 . . 3 (𝐴 No → suc dom 𝐴 ∈ On)
2420, 23eqeltrid 2855 . 2 (𝐴 No → dom (𝐴 ∪ {⟨dom 𝐴, 𝑋⟩}) ∈ On)
25 rnun 5969 . . . 4 ran (𝐴 ∪ {⟨dom 𝐴, 𝑋⟩}) = (ran 𝐴 ∪ ran {⟨dom 𝐴, 𝑋⟩})
26 rnsnopg 6043 . . . . . 6 (dom 𝐴 ∈ V → ran {⟨dom 𝐴, 𝑋⟩} = {𝑋})
272, 26syl 17 . . . . 5 (𝐴 No → ran {⟨dom 𝐴, 𝑋⟩} = {𝑋})
2827uneq2d 4064 . . . 4 (𝐴 No → (ran 𝐴 ∪ ran {⟨dom 𝐴, 𝑋⟩}) = (ran 𝐴 ∪ {𝑋}))
2925, 28syl5eq 2806 . . 3 (𝐴 No → ran (𝐴 ∪ {⟨dom 𝐴, 𝑋⟩}) = (ran 𝐴 ∪ {𝑋}))
30 norn 33404 . . . 4 (𝐴 No → ran 𝐴 ⊆ {1o, 2o})
31 snssi 4691 . . . . 5 (𝑋 ∈ {1o, 2o} → {𝑋} ⊆ {1o, 2o})
323, 31mp1i 13 . . . 4 (𝐴 No → {𝑋} ⊆ {1o, 2o})
3330, 32unssd 4087 . . 3 (𝐴 No → (ran 𝐴 ∪ {𝑋}) ⊆ {1o, 2o})
3429, 33eqsstrd 3926 . 2 (𝐴 No → ran (𝐴 ∪ {⟨dom 𝐴, 𝑋⟩}) ⊆ {1o, 2o})
35 elno2 33407 . 2 ((𝐴 ∪ {⟨dom 𝐴, 𝑋⟩}) ∈ No ↔ (Fun (𝐴 ∪ {⟨dom 𝐴, 𝑋⟩}) ∧ dom (𝐴 ∪ {⟨dom 𝐴, 𝑋⟩}) ∈ On ∧ ran (𝐴 ∪ {⟨dom 𝐴, 𝑋⟩}) ⊆ {1o, 2o}))
3616, 24, 34, 35syl3anbrc 1341 1 (𝐴 No → (𝐴 ∪ {⟨dom 𝐴, 𝑋⟩}) ∈ No )
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ∈ wcel 2112  Vcvv 3407   ∪ cun 3852   ∩ cin 3853   ⊆ wss 3854  ∅c0 4221  {csn 4515  {cpr 4517  ⟨cop 4521  dom cdm 5517  ran crn 5518  Ord word 6161  Oncon0 6162  suc csuc 6164  Fun wfun 6322  1oc1o 8098  2oc2o 8099   No csur 33393 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5149  ax-sep 5162  ax-nul 5169  ax-pr 5291  ax-un 7452 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2899  df-ne 2950  df-ral 3073  df-rex 3074  df-reu 3075  df-rab 3077  df-v 3409  df-sbc 3694  df-csb 3802  df-dif 3857  df-un 3859  df-in 3861  df-ss 3871  df-pss 3873  df-nul 4222  df-if 4414  df-sn 4516  df-pr 4518  df-tp 4520  df-op 4522  df-uni 4792  df-iun 4878  df-br 5026  df-opab 5088  df-mpt 5106  df-tr 5132  df-id 5423  df-eprel 5428  df-po 5436  df-so 5437  df-fr 5476  df-we 5478  df-xp 5523  df-rel 5524  df-cnv 5525  df-co 5526  df-dm 5527  df-rn 5528  df-res 5529  df-ima 5530  df-ord 6165  df-on 6166  df-suc 6168  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-no 33396 This theorem is referenced by:  noextendlt  33422  noextendgt  33423  nosupno  33456  nosupbnd1  33467  nosupbnd2lem1  33468  noinfno  33471  noinfbnd1  33482  noinfbnd2lem1  33483
 Copyright terms: Public domain W3C validator