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

Theorem noextendseq 27177
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 27159 . . . 4 (𝐴 No → Fun 𝐴)
2 noextend.1 . . . . 5 𝑋 ∈ {1o, 2o}
3 fnconstg 6779 . . . . 5 (𝑋 ∈ {1o, 2o} → ((𝐵 ∖ dom 𝐴) × {𝑋}) Fn (𝐵 ∖ dom 𝐴))
4 fnfun 6649 . . . . 5 (((𝐵 ∖ dom 𝐴) × {𝑋}) Fn (𝐵 ∖ dom 𝐴) → Fun ((𝐵 ∖ dom 𝐴) × {𝑋}))
52, 3, 4mp2b 10 . . . 4 Fun ((𝐵 ∖ dom 𝐴) × {𝑋})
6 snnzg 4778 . . . . . . . 8 (𝑋 ∈ {1o, 2o} → {𝑋} ≠ ∅)
7 dmxp 5928 . . . . . . . 8 ({𝑋} ≠ ∅ → dom ((𝐵 ∖ dom 𝐴) × {𝑋}) = (𝐵 ∖ dom 𝐴))
82, 6, 7mp2b 10 . . . . . . 7 dom ((𝐵 ∖ dom 𝐴) × {𝑋}) = (𝐵 ∖ dom 𝐴)
98ineq2i 4209 . . . . . 6 (dom 𝐴 ∩ dom ((𝐵 ∖ dom 𝐴) × {𝑋})) = (dom 𝐴 ∩ (𝐵 ∖ dom 𝐴))
10 disjdif 4471 . . . . . 6 (dom 𝐴 ∩ (𝐵 ∖ dom 𝐴)) = ∅
119, 10eqtri 2760 . . . . 5 (dom 𝐴 ∩ dom ((𝐵 ∖ dom 𝐴) × {𝑋})) = ∅
12 funun 6594 . . . . 5 (((Fun 𝐴 ∧ Fun ((𝐵 ∖ dom 𝐴) × {𝑋})) ∧ (dom 𝐴 ∩ dom ((𝐵 ∖ dom 𝐴) × {𝑋})) = ∅) → Fun (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})))
1311, 12mpan2 689 . . . 4 ((Fun 𝐴 ∧ Fun ((𝐵 ∖ dom 𝐴) × {𝑋})) → Fun (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})))
141, 5, 13sylancl 586 . . 3 (𝐴 No → Fun (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})))
1514adantr 481 . 2 ((𝐴 No 𝐵 ∈ On) → Fun (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})))
16 dmun 5910 . . . 4 dom (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) = (dom 𝐴 ∪ dom ((𝐵 ∖ dom 𝐴) × {𝑋}))
178uneq2i 4160 . . . 4 (dom 𝐴 ∪ dom ((𝐵 ∖ dom 𝐴) × {𝑋})) = (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴))
1816, 17eqtri 2760 . . 3 dom (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) = (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴))
19 nodmon 27160 . . . 4 (𝐴 No → dom 𝐴 ∈ On)
20 undif 4481 . . . . . 6 (dom 𝐴𝐵 ↔ (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) = 𝐵)
21 eleq1a 2828 . . . . . . 7 (𝐵 ∈ On → ((dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) = 𝐵 → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On))
2221adantl 482 . . . . . 6 ((dom 𝐴 ∈ On ∧ 𝐵 ∈ On) → ((dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) = 𝐵 → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On))
2320, 22biimtrid 241 . . . . 5 ((dom 𝐴 ∈ On ∧ 𝐵 ∈ On) → (dom 𝐴𝐵 → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On))
24 ssdif0 4363 . . . . . 6 (𝐵 ⊆ dom 𝐴 ↔ (𝐵 ∖ dom 𝐴) = ∅)
25 uneq2 4157 . . . . . . . . . 10 ((𝐵 ∖ dom 𝐴) = ∅ → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) = (dom 𝐴 ∪ ∅))
26 un0 4390 . . . . . . . . . 10 (dom 𝐴 ∪ ∅) = dom 𝐴
2725, 26eqtrdi 2788 . . . . . . . . 9 ((𝐵 ∖ dom 𝐴) = ∅ → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) = dom 𝐴)
2827eleq1d 2818 . . . . . . . 8 ((𝐵 ∖ dom 𝐴) = ∅ → ((dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On ↔ dom 𝐴 ∈ On))
2928biimprcd 249 . . . . . . 7 (dom 𝐴 ∈ On → ((𝐵 ∖ dom 𝐴) = ∅ → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On))
3029adantr 481 . . . . . 6 ((dom 𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 ∖ dom 𝐴) = ∅ → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On))
3124, 30biimtrid 241 . . . . 5 ((dom 𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐵 ⊆ dom 𝐴 → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On))
32 eloni 6374 . . . . . 6 (dom 𝐴 ∈ On → Ord dom 𝐴)
33 eloni 6374 . . . . . 6 (𝐵 ∈ On → Ord 𝐵)
34 ordtri2or2 6463 . . . . . 6 ((Ord dom 𝐴 ∧ Ord 𝐵) → (dom 𝐴𝐵𝐵 ⊆ dom 𝐴))
3532, 33, 34syl2an 596 . . . . 5 ((dom 𝐴 ∈ On ∧ 𝐵 ∈ On) → (dom 𝐴𝐵𝐵 ⊆ dom 𝐴))
3623, 31, 35mpjaod 858 . . . 4 ((dom 𝐴 ∈ On ∧ 𝐵 ∈ On) → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On)
3719, 36sylan 580 . . 3 ((𝐴 No 𝐵 ∈ On) → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On)
3818, 37eqeltrid 2837 . 2 ((𝐴 No 𝐵 ∈ On) → dom (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) ∈ On)
39 rnun 6145 . . 3 ran (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) = (ran 𝐴 ∪ ran ((𝐵 ∖ dom 𝐴) × {𝑋}))
40 norn 27161 . . . . 5 (𝐴 No → ran 𝐴 ⊆ {1o, 2o})
4140adantr 481 . . . 4 ((𝐴 No 𝐵 ∈ On) → ran 𝐴 ⊆ {1o, 2o})
42 rnxpss 6171 . . . . 5 ran ((𝐵 ∖ dom 𝐴) × {𝑋}) ⊆ {𝑋}
43 snssi 4811 . . . . . 6 (𝑋 ∈ {1o, 2o} → {𝑋} ⊆ {1o, 2o})
442, 43ax-mp 5 . . . . 5 {𝑋} ⊆ {1o, 2o}
4542, 44sstri 3991 . . . 4 ran ((𝐵 ∖ dom 𝐴) × {𝑋}) ⊆ {1o, 2o}
46 unss 4184 . . . 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 4030 . 2 ((𝐴 No 𝐵 ∈ On) → ran (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) ⊆ {1o, 2o})
49 elno2 27164 . 2 ((𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) ∈ No ↔ (Fun (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) ∧ dom (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) ∈ On ∧ ran (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) ⊆ {1o, 2o}))
5015, 38, 48, 49syl3anbrc 1343 1 ((𝐴 No 𝐵 ∈ On) → (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) ∈ No )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wo 845   = wceq 1541  wcel 2106  wne 2940  cdif 3945  cun 3946  cin 3947  wss 3948  c0 4322  {csn 4628  {cpr 4630   × cxp 5674  dom cdm 5676  ran crn 5677  Ord word 6363  Oncon0 6364  Fun wfun 6537   Fn wfn 6538  1oc1o 8461  2oc2o 8462   No csur 27150
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pr 5427
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-ord 6367  df-on 6368  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-no 27153
This theorem is referenced by:  noetasuplem1  27243  noetainflem1  27247
  Copyright terms: Public domain W3C validator