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

Theorem oelim2 7660
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 5776 . . . . . 6 ((𝐵𝐶 ∧ Lim 𝐵) → 𝐵 ∈ On)
2 0ellim 5775 . . . . . . 7 (Lim 𝐵 → ∅ ∈ 𝐵)
32adantl 482 . . . . . 6 ((𝐵𝐶 ∧ Lim 𝐵) → ∅ ∈ 𝐵)
4 oe0m1 7586 . . . . . . 7 (𝐵 ∈ On → (∅ ∈ 𝐵 ↔ (∅ ↑𝑜 𝐵) = ∅))
54biimpa 501 . . . . . 6 ((𝐵 ∈ On ∧ ∅ ∈ 𝐵) → (∅ ↑𝑜 𝐵) = ∅)
61, 3, 5syl2anc 692 . . . . 5 ((𝐵𝐶 ∧ Lim 𝐵) → (∅ ↑𝑜 𝐵) = ∅)
7 eldif 3577 . . . . . . . . 9 (𝑥 ∈ (𝐵 ∖ 1𝑜) ↔ (𝑥𝐵 ∧ ¬ 𝑥 ∈ 1𝑜))
8 limord 5772 . . . . . . . . . . . 12 (Lim 𝐵 → Ord 𝐵)
9 ordelon 5735 . . . . . . . . . . . 12 ((Ord 𝐵𝑥𝐵) → 𝑥 ∈ On)
108, 9sylan 488 . . . . . . . . . . 11 ((Lim 𝐵𝑥𝐵) → 𝑥 ∈ On)
11 on0eln0 5768 . . . . . . . . . . . . 13 (𝑥 ∈ On → (∅ ∈ 𝑥𝑥 ≠ ∅))
12 el1o 7564 . . . . . . . . . . . . . 14 (𝑥 ∈ 1𝑜𝑥 = ∅)
1312necon3bbii 2838 . . . . . . . . . . . . 13 𝑥 ∈ 1𝑜𝑥 ≠ ∅)
1411, 13syl6bbr 278 . . . . . . . . . . . 12 (𝑥 ∈ On → (∅ ∈ 𝑥 ↔ ¬ 𝑥 ∈ 1𝑜))
15 oe0m1 7586 . . . . . . . . . . . . 13 (𝑥 ∈ On → (∅ ∈ 𝑥 ↔ (∅ ↑𝑜 𝑥) = ∅))
1615biimpd 219 . . . . . . . . . . . 12 (𝑥 ∈ On → (∅ ∈ 𝑥 → (∅ ↑𝑜 𝑥) = ∅))
1714, 16sylbird 250 . . . . . . . . . . 11 (𝑥 ∈ On → (¬ 𝑥 ∈ 1𝑜 → (∅ ↑𝑜 𝑥) = ∅))
1810, 17syl 17 . . . . . . . . . 10 ((Lim 𝐵𝑥𝐵) → (¬ 𝑥 ∈ 1𝑜 → (∅ ↑𝑜 𝑥) = ∅))
1918impr 648 . . . . . . . . 9 ((Lim 𝐵 ∧ (𝑥𝐵 ∧ ¬ 𝑥 ∈ 1𝑜)) → (∅ ↑𝑜 𝑥) = ∅)
207, 19sylan2b 492 . . . . . . . 8 ((Lim 𝐵𝑥 ∈ (𝐵 ∖ 1𝑜)) → (∅ ↑𝑜 𝑥) = ∅)
2120iuneq2dv 4533 . . . . . . 7 (Lim 𝐵 𝑥 ∈ (𝐵 ∖ 1𝑜)(∅ ↑𝑜 𝑥) = 𝑥 ∈ (𝐵 ∖ 1𝑜)∅)
22 df-1o 7545 . . . . . . . . . . 11 1𝑜 = suc ∅
23 limsuc 7034 . . . . . . . . . . . 12 (Lim 𝐵 → (∅ ∈ 𝐵 ↔ suc ∅ ∈ 𝐵))
242, 23mpbid 222 . . . . . . . . . . 11 (Lim 𝐵 → suc ∅ ∈ 𝐵)
2522, 24syl5eqel 2703 . . . . . . . . . 10 (Lim 𝐵 → 1𝑜𝐵)
26 1on 7552 . . . . . . . . . . 11 1𝑜 ∈ On
2726onirri 5822 . . . . . . . . . 10 ¬ 1𝑜 ∈ 1𝑜
2825, 27jctir 560 . . . . . . . . 9 (Lim 𝐵 → (1𝑜𝐵 ∧ ¬ 1𝑜 ∈ 1𝑜))
29 eldif 3577 . . . . . . . . 9 (1𝑜 ∈ (𝐵 ∖ 1𝑜) ↔ (1𝑜𝐵 ∧ ¬ 1𝑜 ∈ 1𝑜))
3028, 29sylibr 224 . . . . . . . 8 (Lim 𝐵 → 1𝑜 ∈ (𝐵 ∖ 1𝑜))
31 ne0i 3913 . . . . . . . 8 (1𝑜 ∈ (𝐵 ∖ 1𝑜) → (𝐵 ∖ 1𝑜) ≠ ∅)
32 iunconst 4520 . . . . . . . 8 ((𝐵 ∖ 1𝑜) ≠ ∅ → 𝑥 ∈ (𝐵 ∖ 1𝑜)∅ = ∅)
3330, 31, 323syl 18 . . . . . . 7 (Lim 𝐵 𝑥 ∈ (𝐵 ∖ 1𝑜)∅ = ∅)
3421, 33eqtrd 2654 . . . . . 6 (Lim 𝐵 𝑥 ∈ (𝐵 ∖ 1𝑜)(∅ ↑𝑜 𝑥) = ∅)
3534adantl 482 . . . . 5 ((𝐵𝐶 ∧ Lim 𝐵) → 𝑥 ∈ (𝐵 ∖ 1𝑜)(∅ ↑𝑜 𝑥) = ∅)
366, 35eqtr4d 2657 . . . 4 ((𝐵𝐶 ∧ Lim 𝐵) → (∅ ↑𝑜 𝐵) = 𝑥 ∈ (𝐵 ∖ 1𝑜)(∅ ↑𝑜 𝑥))
37 oveq1 6642 . . . . 5 (𝐴 = ∅ → (𝐴𝑜 𝐵) = (∅ ↑𝑜 𝐵))
38 oveq1 6642 . . . . . 6 (𝐴 = ∅ → (𝐴𝑜 𝑥) = (∅ ↑𝑜 𝑥))
3938iuneq2d 4538 . . . . 5 (𝐴 = ∅ → 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴𝑜 𝑥) = 𝑥 ∈ (𝐵 ∖ 1𝑜)(∅ ↑𝑜 𝑥))
4037, 39eqeq12d 2635 . . . 4 (𝐴 = ∅ → ((𝐴𝑜 𝐵) = 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴𝑜 𝑥) ↔ (∅ ↑𝑜 𝐵) = 𝑥 ∈ (𝐵 ∖ 1𝑜)(∅ ↑𝑜 𝑥)))
4136, 40syl5ibr 236 . . 3 (𝐴 = ∅ → ((𝐵𝐶 ∧ Lim 𝐵) → (𝐴𝑜 𝐵) = 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴𝑜 𝑥)))
4241impcom 446 . 2 (((𝐵𝐶 ∧ Lim 𝐵) ∧ 𝐴 = ∅) → (𝐴𝑜 𝐵) = 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴𝑜 𝑥))
43 oelim 7599 . . 3 (((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → (𝐴𝑜 𝐵) = 𝑦𝐵 (𝐴𝑜 𝑦))
44 limsuc 7034 . . . . . . . . . . . . 13 (Lim 𝐵 → (𝑦𝐵 ↔ suc 𝑦𝐵))
4544biimpa 501 . . . . . . . . . . . 12 ((Lim 𝐵𝑦𝐵) → suc 𝑦𝐵)
46 nsuceq0 5793 . . . . . . . . . . . . 13 suc 𝑦 ≠ ∅
4746a1i 11 . . . . . . . . . . . 12 ((Lim 𝐵𝑦𝐵) → suc 𝑦 ≠ ∅)
48 dif1o 7565 . . . . . . . . . . . 12 (suc 𝑦 ∈ (𝐵 ∖ 1𝑜) ↔ (suc 𝑦𝐵 ∧ suc 𝑦 ≠ ∅))
4945, 47, 48sylanbrc 697 . . . . . . . . . . 11 ((Lim 𝐵𝑦𝐵) → suc 𝑦 ∈ (𝐵 ∖ 1𝑜))
5049ex 450 . . . . . . . . . 10 (Lim 𝐵 → (𝑦𝐵 → suc 𝑦 ∈ (𝐵 ∖ 1𝑜)))
5150ad2antlr 762 . . . . . . . . 9 (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → (𝑦𝐵 → suc 𝑦 ∈ (𝐵 ∖ 1𝑜)))
52 sssucid 5790 . . . . . . . . . . 11 𝑦 ⊆ suc 𝑦
53 ordelon 5735 . . . . . . . . . . . . . . . . 17 ((Ord 𝐵𝑦𝐵) → 𝑦 ∈ On)
548, 53sylan 488 . . . . . . . . . . . . . . . 16 ((Lim 𝐵𝑦𝐵) → 𝑦 ∈ On)
55 suceloni 6998 . . . . . . . . . . . . . . . 16 (𝑦 ∈ On → suc 𝑦 ∈ On)
5654, 55jccir 561 . . . . . . . . . . . . . . 15 ((Lim 𝐵𝑦𝐵) → (𝑦 ∈ On ∧ suc 𝑦 ∈ On))
57 id 22 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On) → (𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On))
58573expa 1263 . . . . . . . . . . . . . . . 16 (((𝑦 ∈ On ∧ suc 𝑦 ∈ On) ∧ 𝐴 ∈ On) → (𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On))
5958ancoms 469 . . . . . . . . . . . . . . 15 ((𝐴 ∈ On ∧ (𝑦 ∈ On ∧ suc 𝑦 ∈ On)) → (𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On))
6056, 59sylan2 491 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ (Lim 𝐵𝑦𝐵)) → (𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On))
6160anassrs 679 . . . . . . . . . . . . 13 (((𝐴 ∈ On ∧ Lim 𝐵) ∧ 𝑦𝐵) → (𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On))
62 oewordi 7656 . . . . . . . . . . . . 13 (((𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (𝑦 ⊆ suc 𝑦 → (𝐴𝑜 𝑦) ⊆ (𝐴𝑜 suc 𝑦)))
6361, 62sylan 488 . . . . . . . . . . . 12 ((((𝐴 ∈ On ∧ Lim 𝐵) ∧ 𝑦𝐵) ∧ ∅ ∈ 𝐴) → (𝑦 ⊆ suc 𝑦 → (𝐴𝑜 𝑦) ⊆ (𝐴𝑜 suc 𝑦)))
6463an32s 845 . . . . . . . . . . 11 ((((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) ∧ 𝑦𝐵) → (𝑦 ⊆ suc 𝑦 → (𝐴𝑜 𝑦) ⊆ (𝐴𝑜 suc 𝑦)))
6552, 64mpi 20 . . . . . . . . . 10 ((((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) ∧ 𝑦𝐵) → (𝐴𝑜 𝑦) ⊆ (𝐴𝑜 suc 𝑦))
6665ex 450 . . . . . . . . 9 (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → (𝑦𝐵 → (𝐴𝑜 𝑦) ⊆ (𝐴𝑜 suc 𝑦)))
6751, 66jcad 555 . . . . . . . 8 (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → (𝑦𝐵 → (suc 𝑦 ∈ (𝐵 ∖ 1𝑜) ∧ (𝐴𝑜 𝑦) ⊆ (𝐴𝑜 suc 𝑦))))
68 oveq2 6643 . . . . . . . . . 10 (𝑥 = suc 𝑦 → (𝐴𝑜 𝑥) = (𝐴𝑜 suc 𝑦))
6968sseq2d 3625 . . . . . . . . 9 (𝑥 = suc 𝑦 → ((𝐴𝑜 𝑦) ⊆ (𝐴𝑜 𝑥) ↔ (𝐴𝑜 𝑦) ⊆ (𝐴𝑜 suc 𝑦)))
7069rspcev 3304 . . . . . . . 8 ((suc 𝑦 ∈ (𝐵 ∖ 1𝑜) ∧ (𝐴𝑜 𝑦) ⊆ (𝐴𝑜 suc 𝑦)) → ∃𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴𝑜 𝑦) ⊆ (𝐴𝑜 𝑥))
7167, 70syl6 35 . . . . . . 7 (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → (𝑦𝐵 → ∃𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴𝑜 𝑦) ⊆ (𝐴𝑜 𝑥)))
7271ralrimiv 2962 . . . . . 6 (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → ∀𝑦𝐵𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴𝑜 𝑦) ⊆ (𝐴𝑜 𝑥))
73 iunss2 4556 . . . . . 6 (∀𝑦𝐵𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴𝑜 𝑦) ⊆ (𝐴𝑜 𝑥) → 𝑦𝐵 (𝐴𝑜 𝑦) ⊆ 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴𝑜 𝑥))
7472, 73syl 17 . . . . 5 (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → 𝑦𝐵 (𝐴𝑜 𝑦) ⊆ 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴𝑜 𝑥))
75 difss 3729 . . . . . . . 8 (𝐵 ∖ 1𝑜) ⊆ 𝐵
76 iunss1 4523 . . . . . . . 8 ((𝐵 ∖ 1𝑜) ⊆ 𝐵 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴𝑜 𝑥) ⊆ 𝑥𝐵 (𝐴𝑜 𝑥))
7775, 76ax-mp 5 . . . . . . 7 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴𝑜 𝑥) ⊆ 𝑥𝐵 (𝐴𝑜 𝑥)
78 oveq2 6643 . . . . . . . 8 (𝑥 = 𝑦 → (𝐴𝑜 𝑥) = (𝐴𝑜 𝑦))
7978cbviunv 4550 . . . . . . 7 𝑥𝐵 (𝐴𝑜 𝑥) = 𝑦𝐵 (𝐴𝑜 𝑦)
8077, 79sseqtri 3629 . . . . . 6 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴𝑜 𝑥) ⊆ 𝑦𝐵 (𝐴𝑜 𝑦)
8180a1i 11 . . . . 5 (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴𝑜 𝑥) ⊆ 𝑦𝐵 (𝐴𝑜 𝑦))
8274, 81eqssd 3612 . . . 4 (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → 𝑦𝐵 (𝐴𝑜 𝑦) = 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴𝑜 𝑥))
8382adantlrl 755 . . 3 (((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → 𝑦𝐵 (𝐴𝑜 𝑦) = 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴𝑜 𝑥))
8443, 83eqtrd 2654 . 2 (((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → (𝐴𝑜 𝐵) = 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴𝑜 𝑥))
8542, 84oe0lem 7578 1 ((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) → (𝐴𝑜 𝐵) = 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴𝑜 𝑥))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384  w3a 1036   = wceq 1481  wcel 1988  wne 2791  wral 2909  wrex 2910  cdif 3564  wss 3567  c0 3907   ciun 4511  Ord word 5710  Oncon0 5711  Lim wlim 5712  suc csuc 5713  (class class class)co 6635  1𝑜c1o 7538  𝑜 coe 7544
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-reu 2916  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-om 7051  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-1o 7545  df-2o 7546  df-oadd 7549  df-omul 7550  df-oexp 7551
This theorem is referenced by:  oelimcl  7665  oaabs2  7710  omabs  7712
  Copyright terms: Public domain W3C validator