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

Theorem oelim2 7562
 Description: Ordinal exponentiation with a limit exponent. Part of Exercise 4.36 of [Mendelson] p. 250. (Contributed by NM, 6-Jan-2005.)
Assertion
Ref Expression
oelim2 ((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) → (𝐴𝑜 𝐵) = 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴𝑜 𝑥))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hint:   𝐶(𝑥)

Proof of Theorem oelim2
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 limelon 5705 . . . . . 6 ((𝐵𝐶 ∧ Lim 𝐵) → 𝐵 ∈ On)
2 0ellim 5704 . . . . . . 7 (Lim 𝐵 → ∅ ∈ 𝐵)
32adantl 481 . . . . . 6 ((𝐵𝐶 ∧ Lim 𝐵) → ∅ ∈ 𝐵)
4 oe0m1 7488 . . . . . . 7 (𝐵 ∈ On → (∅ ∈ 𝐵 ↔ (∅ ↑𝑜 𝐵) = ∅))
54biimpa 500 . . . . . 6 ((𝐵 ∈ On ∧ ∅ ∈ 𝐵) → (∅ ↑𝑜 𝐵) = ∅)
61, 3, 5syl2anc 691 . . . . 5 ((𝐵𝐶 ∧ Lim 𝐵) → (∅ ↑𝑜 𝐵) = ∅)
7 eldif 3550 . . . . . . . . 9 (𝑥 ∈ (𝐵 ∖ 1𝑜) ↔ (𝑥𝐵 ∧ ¬ 𝑥 ∈ 1𝑜))
8 limord 5701 . . . . . . . . . . . 12 (Lim 𝐵 → Ord 𝐵)
9 ordelon 5664 . . . . . . . . . . . 12 ((Ord 𝐵𝑥𝐵) → 𝑥 ∈ On)
108, 9sylan 487 . . . . . . . . . . 11 ((Lim 𝐵𝑥𝐵) → 𝑥 ∈ On)
11 on0eln0 5697 . . . . . . . . . . . . 13 (𝑥 ∈ On → (∅ ∈ 𝑥𝑥 ≠ ∅))
12 el1o 7466 . . . . . . . . . . . . . 14 (𝑥 ∈ 1𝑜𝑥 = ∅)
1312necon3bbii 2829 . . . . . . . . . . . . 13 𝑥 ∈ 1𝑜𝑥 ≠ ∅)
1411, 13syl6bbr 277 . . . . . . . . . . . 12 (𝑥 ∈ On → (∅ ∈ 𝑥 ↔ ¬ 𝑥 ∈ 1𝑜))
15 oe0m1 7488 . . . . . . . . . . . . 13 (𝑥 ∈ On → (∅ ∈ 𝑥 ↔ (∅ ↑𝑜 𝑥) = ∅))
1615biimpd 218 . . . . . . . . . . . 12 (𝑥 ∈ On → (∅ ∈ 𝑥 → (∅ ↑𝑜 𝑥) = ∅))
1714, 16sylbird 249 . . . . . . . . . . 11 (𝑥 ∈ On → (¬ 𝑥 ∈ 1𝑜 → (∅ ↑𝑜 𝑥) = ∅))
1810, 17syl 17 . . . . . . . . . 10 ((Lim 𝐵𝑥𝐵) → (¬ 𝑥 ∈ 1𝑜 → (∅ ↑𝑜 𝑥) = ∅))
1918impr 647 . . . . . . . . 9 ((Lim 𝐵 ∧ (𝑥𝐵 ∧ ¬ 𝑥 ∈ 1𝑜)) → (∅ ↑𝑜 𝑥) = ∅)
207, 19sylan2b 491 . . . . . . . 8 ((Lim 𝐵𝑥 ∈ (𝐵 ∖ 1𝑜)) → (∅ ↑𝑜 𝑥) = ∅)
2120iuneq2dv 4478 . . . . . . 7 (Lim 𝐵 𝑥 ∈ (𝐵 ∖ 1𝑜)(∅ ↑𝑜 𝑥) = 𝑥 ∈ (𝐵 ∖ 1𝑜)∅)
22 df-1o 7447 . . . . . . . . . . 11 1𝑜 = suc ∅
23 limsuc 6941 . . . . . . . . . . . 12 (Lim 𝐵 → (∅ ∈ 𝐵 ↔ suc ∅ ∈ 𝐵))
242, 23mpbid 221 . . . . . . . . . . 11 (Lim 𝐵 → suc ∅ ∈ 𝐵)
2522, 24syl5eqel 2692 . . . . . . . . . 10 (Lim 𝐵 → 1𝑜𝐵)
26 1on 7454 . . . . . . . . . . 11 1𝑜 ∈ On
2726onirri 5751 . . . . . . . . . 10 ¬ 1𝑜 ∈ 1𝑜
2825, 27jctir 559 . . . . . . . . 9 (Lim 𝐵 → (1𝑜𝐵 ∧ ¬ 1𝑜 ∈ 1𝑜))
29 eldif 3550 . . . . . . . . 9 (1𝑜 ∈ (𝐵 ∖ 1𝑜) ↔ (1𝑜𝐵 ∧ ¬ 1𝑜 ∈ 1𝑜))
3028, 29sylibr 223 . . . . . . . 8 (Lim 𝐵 → 1𝑜 ∈ (𝐵 ∖ 1𝑜))
31 ne0i 3880 . . . . . . . 8 (1𝑜 ∈ (𝐵 ∖ 1𝑜) → (𝐵 ∖ 1𝑜) ≠ ∅)
32 iunconst 4465 . . . . . . . 8 ((𝐵 ∖ 1𝑜) ≠ ∅ → 𝑥 ∈ (𝐵 ∖ 1𝑜)∅ = ∅)
3330, 31, 323syl 18 . . . . . . 7 (Lim 𝐵 𝑥 ∈ (𝐵 ∖ 1𝑜)∅ = ∅)
3421, 33eqtrd 2644 . . . . . 6 (Lim 𝐵 𝑥 ∈ (𝐵 ∖ 1𝑜)(∅ ↑𝑜 𝑥) = ∅)
3534adantl 481 . . . . 5 ((𝐵𝐶 ∧ Lim 𝐵) → 𝑥 ∈ (𝐵 ∖ 1𝑜)(∅ ↑𝑜 𝑥) = ∅)
366, 35eqtr4d 2647 . . . 4 ((𝐵𝐶 ∧ Lim 𝐵) → (∅ ↑𝑜 𝐵) = 𝑥 ∈ (𝐵 ∖ 1𝑜)(∅ ↑𝑜 𝑥))
37 oveq1 6556 . . . . 5 (𝐴 = ∅ → (𝐴𝑜 𝐵) = (∅ ↑𝑜 𝐵))
38 oveq1 6556 . . . . . 6 (𝐴 = ∅ → (𝐴𝑜 𝑥) = (∅ ↑𝑜 𝑥))
3938iuneq2d 4483 . . . . 5 (𝐴 = ∅ → 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴𝑜 𝑥) = 𝑥 ∈ (𝐵 ∖ 1𝑜)(∅ ↑𝑜 𝑥))
4037, 39eqeq12d 2625 . . . 4 (𝐴 = ∅ → ((𝐴𝑜 𝐵) = 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴𝑜 𝑥) ↔ (∅ ↑𝑜 𝐵) = 𝑥 ∈ (𝐵 ∖ 1𝑜)(∅ ↑𝑜 𝑥)))
4136, 40syl5ibr 235 . . 3 (𝐴 = ∅ → ((𝐵𝐶 ∧ Lim 𝐵) → (𝐴𝑜 𝐵) = 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴𝑜 𝑥)))
4241impcom 445 . 2 (((𝐵𝐶 ∧ Lim 𝐵) ∧ 𝐴 = ∅) → (𝐴𝑜 𝐵) = 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴𝑜 𝑥))
43 oelim 7501 . . 3 (((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → (𝐴𝑜 𝐵) = 𝑦𝐵 (𝐴𝑜 𝑦))
44 limsuc 6941 . . . . . . . . . . . . 13 (Lim 𝐵 → (𝑦𝐵 ↔ suc 𝑦𝐵))
4544biimpa 500 . . . . . . . . . . . 12 ((Lim 𝐵𝑦𝐵) → suc 𝑦𝐵)
46 nsuceq0 5722 . . . . . . . . . . . . 13 suc 𝑦 ≠ ∅
4746a1i 11 . . . . . . . . . . . 12 ((Lim 𝐵𝑦𝐵) → suc 𝑦 ≠ ∅)
48 dif1o 7467 . . . . . . . . . . . 12 (suc 𝑦 ∈ (𝐵 ∖ 1𝑜) ↔ (suc 𝑦𝐵 ∧ suc 𝑦 ≠ ∅))
4945, 47, 48sylanbrc 695 . . . . . . . . . . 11 ((Lim 𝐵𝑦𝐵) → suc 𝑦 ∈ (𝐵 ∖ 1𝑜))
5049ex 449 . . . . . . . . . 10 (Lim 𝐵 → (𝑦𝐵 → suc 𝑦 ∈ (𝐵 ∖ 1𝑜)))
5150ad2antlr 759 . . . . . . . . 9 (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → (𝑦𝐵 → suc 𝑦 ∈ (𝐵 ∖ 1𝑜)))
52 sssucid 5719 . . . . . . . . . . 11 𝑦 ⊆ suc 𝑦
53 ordelon 5664 . . . . . . . . . . . . . . . . 17 ((Ord 𝐵𝑦𝐵) → 𝑦 ∈ On)
548, 53sylan 487 . . . . . . . . . . . . . . . 16 ((Lim 𝐵𝑦𝐵) → 𝑦 ∈ On)
55 suceloni 6905 . . . . . . . . . . . . . . . 16 (𝑦 ∈ On → suc 𝑦 ∈ On)
5654, 55jccir 560 . . . . . . . . . . . . . . 15 ((Lim 𝐵𝑦𝐵) → (𝑦 ∈ On ∧ suc 𝑦 ∈ On))
57 id 22 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On) → (𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On))
58573expa 1257 . . . . . . . . . . . . . . . 16 (((𝑦 ∈ On ∧ suc 𝑦 ∈ On) ∧ 𝐴 ∈ On) → (𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On))
5958ancoms 468 . . . . . . . . . . . . . . 15 ((𝐴 ∈ On ∧ (𝑦 ∈ On ∧ suc 𝑦 ∈ On)) → (𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On))
6056, 59sylan2 490 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ (Lim 𝐵𝑦𝐵)) → (𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On))
6160anassrs 678 . . . . . . . . . . . . 13 (((𝐴 ∈ On ∧ Lim 𝐵) ∧ 𝑦𝐵) → (𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On))
62 oewordi 7558 . . . . . . . . . . . . 13 (((𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (𝑦 ⊆ suc 𝑦 → (𝐴𝑜 𝑦) ⊆ (𝐴𝑜 suc 𝑦)))
6361, 62sylan 487 . . . . . . . . . . . 12 ((((𝐴 ∈ On ∧ Lim 𝐵) ∧ 𝑦𝐵) ∧ ∅ ∈ 𝐴) → (𝑦 ⊆ suc 𝑦 → (𝐴𝑜 𝑦) ⊆ (𝐴𝑜 suc 𝑦)))
6463an32s 842 . . . . . . . . . . 11 ((((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) ∧ 𝑦𝐵) → (𝑦 ⊆ suc 𝑦 → (𝐴𝑜 𝑦) ⊆ (𝐴𝑜 suc 𝑦)))
6552, 64mpi 20 . . . . . . . . . 10 ((((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) ∧ 𝑦𝐵) → (𝐴𝑜 𝑦) ⊆ (𝐴𝑜 suc 𝑦))
6665ex 449 . . . . . . . . 9 (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → (𝑦𝐵 → (𝐴𝑜 𝑦) ⊆ (𝐴𝑜 suc 𝑦)))
6751, 66jcad 554 . . . . . . . 8 (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → (𝑦𝐵 → (suc 𝑦 ∈ (𝐵 ∖ 1𝑜) ∧ (𝐴𝑜 𝑦) ⊆ (𝐴𝑜 suc 𝑦))))
68 oveq2 6557 . . . . . . . . . 10 (𝑥 = suc 𝑦 → (𝐴𝑜 𝑥) = (𝐴𝑜 suc 𝑦))
6968sseq2d 3596 . . . . . . . . 9 (𝑥 = suc 𝑦 → ((𝐴𝑜 𝑦) ⊆ (𝐴𝑜 𝑥) ↔ (𝐴𝑜 𝑦) ⊆ (𝐴𝑜 suc 𝑦)))
7069rspcev 3282 . . . . . . . 8 ((suc 𝑦 ∈ (𝐵 ∖ 1𝑜) ∧ (𝐴𝑜 𝑦) ⊆ (𝐴𝑜 suc 𝑦)) → ∃𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴𝑜 𝑦) ⊆ (𝐴𝑜 𝑥))
7167, 70syl6 34 . . . . . . 7 (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → (𝑦𝐵 → ∃𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴𝑜 𝑦) ⊆ (𝐴𝑜 𝑥)))
7271ralrimiv 2948 . . . . . 6 (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → ∀𝑦𝐵𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴𝑜 𝑦) ⊆ (𝐴𝑜 𝑥))
73 iunss2 4501 . . . . . 6 (∀𝑦𝐵𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴𝑜 𝑦) ⊆ (𝐴𝑜 𝑥) → 𝑦𝐵 (𝐴𝑜 𝑦) ⊆ 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴𝑜 𝑥))
7472, 73syl 17 . . . . 5 (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → 𝑦𝐵 (𝐴𝑜 𝑦) ⊆ 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴𝑜 𝑥))
75 difss 3699 . . . . . . . 8 (𝐵 ∖ 1𝑜) ⊆ 𝐵
76 iunss1 4468 . . . . . . . 8 ((𝐵 ∖ 1𝑜) ⊆ 𝐵 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴𝑜 𝑥) ⊆ 𝑥𝐵 (𝐴𝑜 𝑥))
7775, 76ax-mp 5 . . . . . . 7 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴𝑜 𝑥) ⊆ 𝑥𝐵 (𝐴𝑜 𝑥)
78 oveq2 6557 . . . . . . . 8 (𝑥 = 𝑦 → (𝐴𝑜 𝑥) = (𝐴𝑜 𝑦))
7978cbviunv 4495 . . . . . . 7 𝑥𝐵 (𝐴𝑜 𝑥) = 𝑦𝐵 (𝐴𝑜 𝑦)
8077, 79sseqtri 3600 . . . . . 6 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴𝑜 𝑥) ⊆ 𝑦𝐵 (𝐴𝑜 𝑦)
8180a1i 11 . . . . 5 (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴𝑜 𝑥) ⊆ 𝑦𝐵 (𝐴𝑜 𝑦))
8274, 81eqssd 3585 . . . 4 (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → 𝑦𝐵 (𝐴𝑜 𝑦) = 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴𝑜 𝑥))
8382adantlrl 752 . . 3 (((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → 𝑦𝐵 (𝐴𝑜 𝑦) = 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴𝑜 𝑥))
8443, 83eqtrd 2644 . 2 (((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → (𝐴𝑜 𝐵) = 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴𝑜 𝑥))
8542, 84oe0lem 7480 1 ((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) → (𝐴𝑜 𝐵) = 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴𝑜 𝑥))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897   ∖ cdif 3537   ⊆ wss 3540  ∅c0 3874  ∪ ciun 4455  Ord word 5639  Oncon0 5640  Lim wlim 5641  suc csuc 5642  (class class class)co 6549  1𝑜c1o 7440   ↑𝑜 coe 7446 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-omul 7452  df-oexp 7453 This theorem is referenced by:  oelimcl  7567  oaabs2  7612  omabs  7614
 Copyright terms: Public domain W3C validator