MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  noextendseq Structured version   Visualization version   GIF version

Theorem noextendseq 27726
Description: Extend a surreal by a sequence of ordinals. (Contributed by Scott Fenton, 30-Nov-2021.)
Hypothesis
Ref Expression
noextend.1 𝑋 ∈ {1o, 2o}
Assertion
Ref Expression
noextendseq ((𝐴 No 𝐵 ∈ On) → (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) ∈ No )

Proof of Theorem noextendseq
StepHypRef Expression
1 nofun 27708 . . . 4 (𝐴 No → Fun 𝐴)
2 noextend.1 . . . . 5 𝑋 ∈ {1o, 2o}
3 fnconstg 6796 . . . . 5 (𝑋 ∈ {1o, 2o} → ((𝐵 ∖ dom 𝐴) × {𝑋}) Fn (𝐵 ∖ dom 𝐴))
4 fnfun 6668 . . . . 5 (((𝐵 ∖ dom 𝐴) × {𝑋}) Fn (𝐵 ∖ dom 𝐴) → Fun ((𝐵 ∖ dom 𝐴) × {𝑋}))
52, 3, 4mp2b 10 . . . 4 Fun ((𝐵 ∖ dom 𝐴) × {𝑋})
6 snnzg 4778 . . . . . . . 8 (𝑋 ∈ {1o, 2o} → {𝑋} ≠ ∅)
7 dmxp 5941 . . . . . . . 8 ({𝑋} ≠ ∅ → dom ((𝐵 ∖ dom 𝐴) × {𝑋}) = (𝐵 ∖ dom 𝐴))
82, 6, 7mp2b 10 . . . . . . 7 dom ((𝐵 ∖ dom 𝐴) × {𝑋}) = (𝐵 ∖ dom 𝐴)
98ineq2i 4224 . . . . . 6 (dom 𝐴 ∩ dom ((𝐵 ∖ dom 𝐴) × {𝑋})) = (dom 𝐴 ∩ (𝐵 ∖ dom 𝐴))
10 disjdif 4477 . . . . . 6 (dom 𝐴 ∩ (𝐵 ∖ dom 𝐴)) = ∅
119, 10eqtri 2762 . . . . 5 (dom 𝐴 ∩ dom ((𝐵 ∖ dom 𝐴) × {𝑋})) = ∅
12 funun 6613 . . . . 5 (((Fun 𝐴 ∧ Fun ((𝐵 ∖ dom 𝐴) × {𝑋})) ∧ (dom 𝐴 ∩ dom ((𝐵 ∖ dom 𝐴) × {𝑋})) = ∅) → Fun (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})))
1311, 12mpan2 691 . . . 4 ((Fun 𝐴 ∧ Fun ((𝐵 ∖ dom 𝐴) × {𝑋})) → Fun (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})))
141, 5, 13sylancl 586 . . 3 (𝐴 No → Fun (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})))
1514adantr 480 . 2 ((𝐴 No 𝐵 ∈ On) → Fun (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})))
16 dmun 5923 . . . 4 dom (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) = (dom 𝐴 ∪ dom ((𝐵 ∖ dom 𝐴) × {𝑋}))
178uneq2i 4174 . . . 4 (dom 𝐴 ∪ dom ((𝐵 ∖ dom 𝐴) × {𝑋})) = (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴))
1816, 17eqtri 2762 . . 3 dom (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) = (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴))
19 nodmon 27709 . . . 4 (𝐴 No → dom 𝐴 ∈ On)
20 undif 4487 . . . . . 6 (dom 𝐴𝐵 ↔ (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) = 𝐵)
21 eleq1a 2833 . . . . . . 7 (𝐵 ∈ On → ((dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) = 𝐵 → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On))
2221adantl 481 . . . . . 6 ((dom 𝐴 ∈ On ∧ 𝐵 ∈ On) → ((dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) = 𝐵 → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On))
2320, 22biimtrid 242 . . . . 5 ((dom 𝐴 ∈ On ∧ 𝐵 ∈ On) → (dom 𝐴𝐵 → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On))
24 ssdif0 4371 . . . . . 6 (𝐵 ⊆ dom 𝐴 ↔ (𝐵 ∖ dom 𝐴) = ∅)
25 uneq2 4171 . . . . . . . . . 10 ((𝐵 ∖ dom 𝐴) = ∅ → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) = (dom 𝐴 ∪ ∅))
26 un0 4399 . . . . . . . . . 10 (dom 𝐴 ∪ ∅) = dom 𝐴
2725, 26eqtrdi 2790 . . . . . . . . 9 ((𝐵 ∖ dom 𝐴) = ∅ → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) = dom 𝐴)
2827eleq1d 2823 . . . . . . . 8 ((𝐵 ∖ dom 𝐴) = ∅ → ((dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On ↔ dom 𝐴 ∈ On))
2928biimprcd 250 . . . . . . 7 (dom 𝐴 ∈ On → ((𝐵 ∖ dom 𝐴) = ∅ → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On))
3029adantr 480 . . . . . 6 ((dom 𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 ∖ dom 𝐴) = ∅ → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On))
3124, 30biimtrid 242 . . . . 5 ((dom 𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐵 ⊆ dom 𝐴 → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On))
32 eloni 6395 . . . . . 6 (dom 𝐴 ∈ On → Ord dom 𝐴)
33 eloni 6395 . . . . . 6 (𝐵 ∈ On → Ord 𝐵)
34 ordtri2or2 6484 . . . . . 6 ((Ord dom 𝐴 ∧ Ord 𝐵) → (dom 𝐴𝐵𝐵 ⊆ dom 𝐴))
3532, 33, 34syl2an 596 . . . . 5 ((dom 𝐴 ∈ On ∧ 𝐵 ∈ On) → (dom 𝐴𝐵𝐵 ⊆ dom 𝐴))
3623, 31, 35mpjaod 860 . . . 4 ((dom 𝐴 ∈ On ∧ 𝐵 ∈ On) → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On)
3719, 36sylan 580 . . 3 ((𝐴 No 𝐵 ∈ On) → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On)
3818, 37eqeltrid 2842 . 2 ((𝐴 No 𝐵 ∈ On) → dom (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) ∈ On)
39 rnun 6167 . . 3 ran (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) = (ran 𝐴 ∪ ran ((𝐵 ∖ dom 𝐴) × {𝑋}))
40 norn 27710 . . . . 5 (𝐴 No → ran 𝐴 ⊆ {1o, 2o})
4140adantr 480 . . . 4 ((𝐴 No 𝐵 ∈ On) → ran 𝐴 ⊆ {1o, 2o})
42 rnxpss 6193 . . . . 5 ran ((𝐵 ∖ dom 𝐴) × {𝑋}) ⊆ {𝑋}
43 snssi 4812 . . . . . 6 (𝑋 ∈ {1o, 2o} → {𝑋} ⊆ {1o, 2o})
442, 43ax-mp 5 . . . . 5 {𝑋} ⊆ {1o, 2o}
4542, 44sstri 4004 . . . 4 ran ((𝐵 ∖ dom 𝐴) × {𝑋}) ⊆ {1o, 2o}
46 unss 4199 . . . 4 ((ran 𝐴 ⊆ {1o, 2o} ∧ ran ((𝐵 ∖ dom 𝐴) × {𝑋}) ⊆ {1o, 2o}) ↔ (ran 𝐴 ∪ ran ((𝐵 ∖ dom 𝐴) × {𝑋})) ⊆ {1o, 2o})
4741, 45, 46sylanblc 589 . . 3 ((𝐴 No 𝐵 ∈ On) → (ran 𝐴 ∪ ran ((𝐵 ∖ dom 𝐴) × {𝑋})) ⊆ {1o, 2o})
4839, 47eqsstrid 4043 . 2 ((𝐴 No 𝐵 ∈ On) → ran (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) ⊆ {1o, 2o})
49 elno2 27713 . 2 ((𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) ∈ No ↔ (Fun (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) ∧ dom (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) ∈ On ∧ ran (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) ⊆ {1o, 2o}))
5015, 38, 48, 49syl3anbrc 1342 1 ((𝐴 No 𝐵 ∈ On) → (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) ∈ No )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wo 847   = wceq 1536  wcel 2105  wne 2937  cdif 3959  cun 3960  cin 3961  wss 3962  c0 4338  {csn 4630  {cpr 4632   × cxp 5686  dom cdm 5688  ran crn 5689  Ord word 6384  Oncon0 6385  Fun wfun 6556   Fn wfn 6557  1oc1o 8497  2oc2o 8498   No csur 27698
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-ord 6388  df-on 6389  df-fun 6564  df-fn 6565  df-f 6566  df-no 27701
This theorem is referenced by:  noetasuplem1  27792  noetainflem1  27796
  Copyright terms: Public domain W3C validator