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

Theorem oelim2 7947
 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 𝐵)) → (𝐴o 𝐵) = 𝑥 ∈ (𝐵 ∖ 1o)(𝐴o 𝑥))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hint:   𝐶(𝑥)

Proof of Theorem oelim2
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 limelon 6030 . . . . . 6 ((𝐵𝐶 ∧ Lim 𝐵) → 𝐵 ∈ On)
2 0ellim 6029 . . . . . . 7 (Lim 𝐵 → ∅ ∈ 𝐵)
32adantl 475 . . . . . 6 ((𝐵𝐶 ∧ Lim 𝐵) → ∅ ∈ 𝐵)
4 oe0m1 7873 . . . . . . 7 (𝐵 ∈ On → (∅ ∈ 𝐵 ↔ (∅ ↑o 𝐵) = ∅))
54biimpa 470 . . . . . 6 ((𝐵 ∈ On ∧ ∅ ∈ 𝐵) → (∅ ↑o 𝐵) = ∅)
61, 3, 5syl2anc 579 . . . . 5 ((𝐵𝐶 ∧ Lim 𝐵) → (∅ ↑o 𝐵) = ∅)
7 eldif 3808 . . . . . . . . 9 (𝑥 ∈ (𝐵 ∖ 1o) ↔ (𝑥𝐵 ∧ ¬ 𝑥 ∈ 1o))
8 limord 6026 . . . . . . . . . . . 12 (Lim 𝐵 → Ord 𝐵)
9 ordelon 5991 . . . . . . . . . . . 12 ((Ord 𝐵𝑥𝐵) → 𝑥 ∈ On)
108, 9sylan 575 . . . . . . . . . . 11 ((Lim 𝐵𝑥𝐵) → 𝑥 ∈ On)
11 on0eln0 6022 . . . . . . . . . . . . 13 (𝑥 ∈ On → (∅ ∈ 𝑥𝑥 ≠ ∅))
12 el1o 7851 . . . . . . . . . . . . . 14 (𝑥 ∈ 1o𝑥 = ∅)
1312necon3bbii 3046 . . . . . . . . . . . . 13 𝑥 ∈ 1o𝑥 ≠ ∅)
1411, 13syl6bbr 281 . . . . . . . . . . . 12 (𝑥 ∈ On → (∅ ∈ 𝑥 ↔ ¬ 𝑥 ∈ 1o))
15 oe0m1 7873 . . . . . . . . . . . . 13 (𝑥 ∈ On → (∅ ∈ 𝑥 ↔ (∅ ↑o 𝑥) = ∅))
1615biimpd 221 . . . . . . . . . . . 12 (𝑥 ∈ On → (∅ ∈ 𝑥 → (∅ ↑o 𝑥) = ∅))
1714, 16sylbird 252 . . . . . . . . . . 11 (𝑥 ∈ On → (¬ 𝑥 ∈ 1o → (∅ ↑o 𝑥) = ∅))
1810, 17syl 17 . . . . . . . . . 10 ((Lim 𝐵𝑥𝐵) → (¬ 𝑥 ∈ 1o → (∅ ↑o 𝑥) = ∅))
1918impr 448 . . . . . . . . 9 ((Lim 𝐵 ∧ (𝑥𝐵 ∧ ¬ 𝑥 ∈ 1o)) → (∅ ↑o 𝑥) = ∅)
207, 19sylan2b 587 . . . . . . . 8 ((Lim 𝐵𝑥 ∈ (𝐵 ∖ 1o)) → (∅ ↑o 𝑥) = ∅)
2120iuneq2dv 4764 . . . . . . 7 (Lim 𝐵 𝑥 ∈ (𝐵 ∖ 1o)(∅ ↑o 𝑥) = 𝑥 ∈ (𝐵 ∖ 1o)∅)
22 df-1o 7831 . . . . . . . . . . 11 1o = suc ∅
23 limsuc 7315 . . . . . . . . . . . 12 (Lim 𝐵 → (∅ ∈ 𝐵 ↔ suc ∅ ∈ 𝐵))
242, 23mpbid 224 . . . . . . . . . . 11 (Lim 𝐵 → suc ∅ ∈ 𝐵)
2522, 24syl5eqel 2910 . . . . . . . . . 10 (Lim 𝐵 → 1o𝐵)
26 1on 7838 . . . . . . . . . . 11 1o ∈ On
2726onirri 6073 . . . . . . . . . 10 ¬ 1o ∈ 1o
2825, 27jctir 516 . . . . . . . . 9 (Lim 𝐵 → (1o𝐵 ∧ ¬ 1o ∈ 1o))
29 eldif 3808 . . . . . . . . 9 (1o ∈ (𝐵 ∖ 1o) ↔ (1o𝐵 ∧ ¬ 1o ∈ 1o))
3028, 29sylibr 226 . . . . . . . 8 (Lim 𝐵 → 1o ∈ (𝐵 ∖ 1o))
31 ne0i 4152 . . . . . . . 8 (1o ∈ (𝐵 ∖ 1o) → (𝐵 ∖ 1o) ≠ ∅)
32 iunconst 4751 . . . . . . . 8 ((𝐵 ∖ 1o) ≠ ∅ → 𝑥 ∈ (𝐵 ∖ 1o)∅ = ∅)
3330, 31, 323syl 18 . . . . . . 7 (Lim 𝐵 𝑥 ∈ (𝐵 ∖ 1o)∅ = ∅)
3421, 33eqtrd 2861 . . . . . 6 (Lim 𝐵 𝑥 ∈ (𝐵 ∖ 1o)(∅ ↑o 𝑥) = ∅)
3534adantl 475 . . . . 5 ((𝐵𝐶 ∧ Lim 𝐵) → 𝑥 ∈ (𝐵 ∖ 1o)(∅ ↑o 𝑥) = ∅)
366, 35eqtr4d 2864 . . . 4 ((𝐵𝐶 ∧ Lim 𝐵) → (∅ ↑o 𝐵) = 𝑥 ∈ (𝐵 ∖ 1o)(∅ ↑o 𝑥))
37 oveq1 6917 . . . . 5 (𝐴 = ∅ → (𝐴o 𝐵) = (∅ ↑o 𝐵))
38 oveq1 6917 . . . . . 6 (𝐴 = ∅ → (𝐴o 𝑥) = (∅ ↑o 𝑥))
3938iuneq2d 4769 . . . . 5 (𝐴 = ∅ → 𝑥 ∈ (𝐵 ∖ 1o)(𝐴o 𝑥) = 𝑥 ∈ (𝐵 ∖ 1o)(∅ ↑o 𝑥))
4037, 39eqeq12d 2840 . . . 4 (𝐴 = ∅ → ((𝐴o 𝐵) = 𝑥 ∈ (𝐵 ∖ 1o)(𝐴o 𝑥) ↔ (∅ ↑o 𝐵) = 𝑥 ∈ (𝐵 ∖ 1o)(∅ ↑o 𝑥)))
4136, 40syl5ibr 238 . . 3 (𝐴 = ∅ → ((𝐵𝐶 ∧ Lim 𝐵) → (𝐴o 𝐵) = 𝑥 ∈ (𝐵 ∖ 1o)(𝐴o 𝑥)))
4241impcom 398 . 2 (((𝐵𝐶 ∧ Lim 𝐵) ∧ 𝐴 = ∅) → (𝐴o 𝐵) = 𝑥 ∈ (𝐵 ∖ 1o)(𝐴o 𝑥))
43 oelim 7886 . . 3 (((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → (𝐴o 𝐵) = 𝑦𝐵 (𝐴o 𝑦))
44 limsuc 7315 . . . . . . . . . . . . 13 (Lim 𝐵 → (𝑦𝐵 ↔ suc 𝑦𝐵))
4544biimpa 470 . . . . . . . . . . . 12 ((Lim 𝐵𝑦𝐵) → suc 𝑦𝐵)
46 nsuceq0 6047 . . . . . . . . . . . . 13 suc 𝑦 ≠ ∅
4746a1i 11 . . . . . . . . . . . 12 ((Lim 𝐵𝑦𝐵) → suc 𝑦 ≠ ∅)
48 dif1o 7852 . . . . . . . . . . . 12 (suc 𝑦 ∈ (𝐵 ∖ 1o) ↔ (suc 𝑦𝐵 ∧ suc 𝑦 ≠ ∅))
4945, 47, 48sylanbrc 578 . . . . . . . . . . 11 ((Lim 𝐵𝑦𝐵) → suc 𝑦 ∈ (𝐵 ∖ 1o))
5049ex 403 . . . . . . . . . 10 (Lim 𝐵 → (𝑦𝐵 → suc 𝑦 ∈ (𝐵 ∖ 1o)))
5150ad2antlr 718 . . . . . . . . 9 (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → (𝑦𝐵 → suc 𝑦 ∈ (𝐵 ∖ 1o)))
52 sssucid 6044 . . . . . . . . . . 11 𝑦 ⊆ suc 𝑦
53 ordelon 5991 . . . . . . . . . . . . . . . . 17 ((Ord 𝐵𝑦𝐵) → 𝑦 ∈ On)
548, 53sylan 575 . . . . . . . . . . . . . . . 16 ((Lim 𝐵𝑦𝐵) → 𝑦 ∈ On)
55 suceloni 7279 . . . . . . . . . . . . . . . 16 (𝑦 ∈ On → suc 𝑦 ∈ On)
5654, 55jccir 517 . . . . . . . . . . . . . . 15 ((Lim 𝐵𝑦𝐵) → (𝑦 ∈ On ∧ suc 𝑦 ∈ On))
57 id 22 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On) → (𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On))
58573expa 1151 . . . . . . . . . . . . . . . 16 (((𝑦 ∈ On ∧ suc 𝑦 ∈ On) ∧ 𝐴 ∈ On) → (𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On))
5958ancoms 452 . . . . . . . . . . . . . . 15 ((𝐴 ∈ On ∧ (𝑦 ∈ On ∧ suc 𝑦 ∈ On)) → (𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On))
6056, 59sylan2 586 . . . . . . . . . . . . . 14 ((𝐴 ∈ On ∧ (Lim 𝐵𝑦𝐵)) → (𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On))
6160anassrs 461 . . . . . . . . . . . . 13 (((𝐴 ∈ On ∧ Lim 𝐵) ∧ 𝑦𝐵) → (𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On))
62 oewordi 7943 . . . . . . . . . . . . 13 (((𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (𝑦 ⊆ suc 𝑦 → (𝐴o 𝑦) ⊆ (𝐴o suc 𝑦)))
6361, 62sylan 575 . . . . . . . . . . . 12 ((((𝐴 ∈ On ∧ Lim 𝐵) ∧ 𝑦𝐵) ∧ ∅ ∈ 𝐴) → (𝑦 ⊆ suc 𝑦 → (𝐴o 𝑦) ⊆ (𝐴o suc 𝑦)))
6463an32s 642 . . . . . . . . . . 11 ((((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) ∧ 𝑦𝐵) → (𝑦 ⊆ suc 𝑦 → (𝐴o 𝑦) ⊆ (𝐴o suc 𝑦)))
6552, 64mpi 20 . . . . . . . . . 10 ((((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) ∧ 𝑦𝐵) → (𝐴o 𝑦) ⊆ (𝐴o suc 𝑦))
6665ex 403 . . . . . . . . 9 (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → (𝑦𝐵 → (𝐴o 𝑦) ⊆ (𝐴o suc 𝑦)))
6751, 66jcad 508 . . . . . . . 8 (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → (𝑦𝐵 → (suc 𝑦 ∈ (𝐵 ∖ 1o) ∧ (𝐴o 𝑦) ⊆ (𝐴o suc 𝑦))))
68 oveq2 6918 . . . . . . . . . 10 (𝑥 = suc 𝑦 → (𝐴o 𝑥) = (𝐴o suc 𝑦))
6968sseq2d 3858 . . . . . . . . 9 (𝑥 = suc 𝑦 → ((𝐴o 𝑦) ⊆ (𝐴o 𝑥) ↔ (𝐴o 𝑦) ⊆ (𝐴o suc 𝑦)))
7069rspcev 3526 . . . . . . . 8 ((suc 𝑦 ∈ (𝐵 ∖ 1o) ∧ (𝐴o 𝑦) ⊆ (𝐴o suc 𝑦)) → ∃𝑥 ∈ (𝐵 ∖ 1o)(𝐴o 𝑦) ⊆ (𝐴o 𝑥))
7167, 70syl6 35 . . . . . . 7 (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → (𝑦𝐵 → ∃𝑥 ∈ (𝐵 ∖ 1o)(𝐴o 𝑦) ⊆ (𝐴o 𝑥)))
7271ralrimiv 3174 . . . . . 6 (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → ∀𝑦𝐵𝑥 ∈ (𝐵 ∖ 1o)(𝐴o 𝑦) ⊆ (𝐴o 𝑥))
73 iunss2 4787 . . . . . 6 (∀𝑦𝐵𝑥 ∈ (𝐵 ∖ 1o)(𝐴o 𝑦) ⊆ (𝐴o 𝑥) → 𝑦𝐵 (𝐴o 𝑦) ⊆ 𝑥 ∈ (𝐵 ∖ 1o)(𝐴o 𝑥))
7472, 73syl 17 . . . . 5 (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → 𝑦𝐵 (𝐴o 𝑦) ⊆ 𝑥 ∈ (𝐵 ∖ 1o)(𝐴o 𝑥))
75 difss 3966 . . . . . . . 8 (𝐵 ∖ 1o) ⊆ 𝐵
76 iunss1 4754 . . . . . . . 8 ((𝐵 ∖ 1o) ⊆ 𝐵 𝑥 ∈ (𝐵 ∖ 1o)(𝐴o 𝑥) ⊆ 𝑥𝐵 (𝐴o 𝑥))
7775, 76ax-mp 5 . . . . . . 7 𝑥 ∈ (𝐵 ∖ 1o)(𝐴o 𝑥) ⊆ 𝑥𝐵 (𝐴o 𝑥)
78 oveq2 6918 . . . . . . . 8 (𝑥 = 𝑦 → (𝐴o 𝑥) = (𝐴o 𝑦))
7978cbviunv 4781 . . . . . . 7 𝑥𝐵 (𝐴o 𝑥) = 𝑦𝐵 (𝐴o 𝑦)
8077, 79sseqtri 3862 . . . . . 6 𝑥 ∈ (𝐵 ∖ 1o)(𝐴o 𝑥) ⊆ 𝑦𝐵 (𝐴o 𝑦)
8180a1i 11 . . . . 5 (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → 𝑥 ∈ (𝐵 ∖ 1o)(𝐴o 𝑥) ⊆ 𝑦𝐵 (𝐴o 𝑦))
8274, 81eqssd 3844 . . . 4 (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → 𝑦𝐵 (𝐴o 𝑦) = 𝑥 ∈ (𝐵 ∖ 1o)(𝐴o 𝑥))
8382adantlrl 711 . . 3 (((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → 𝑦𝐵 (𝐴o 𝑦) = 𝑥 ∈ (𝐵 ∖ 1o)(𝐴o 𝑥))
8443, 83eqtrd 2861 . 2 (((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → (𝐴o 𝐵) = 𝑥 ∈ (𝐵 ∖ 1o)(𝐴o 𝑥))
8542, 84oe0lem 7865 1 ((𝐴 ∈ On ∧ (𝐵𝐶 ∧ Lim 𝐵)) → (𝐴o 𝐵) = 𝑥 ∈ (𝐵 ∖ 1o)(𝐴o 𝑥))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 386   ∧ w3a 1111   = wceq 1656   ∈ wcel 2164   ≠ wne 2999  ∀wral 3117  ∃wrex 3118   ∖ cdif 3795   ⊆ wss 3798  ∅c0 4146  ∪ ciun 4742  Ord word 5966  Oncon0 5967  Lim wlim 5968  suc csuc 5969  (class class class)co 6910  1oc1o 7824   ↑o coe 7830 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-rep 4996  ax-sep 5007  ax-nul 5015  ax-pow 5067  ax-pr 5129  ax-un 7214 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3or 1112  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-reu 3124  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4147  df-if 4309  df-pw 4382  df-sn 4400  df-pr 4402  df-tp 4404  df-op 4406  df-uni 4661  df-iun 4744  df-br 4876  df-opab 4938  df-mpt 4955  df-tr 4978  df-id 5252  df-eprel 5257  df-po 5265  df-so 5266  df-fr 5305  df-we 5307  df-xp 5352  df-rel 5353  df-cnv 5354  df-co 5355  df-dm 5356  df-rn 5357  df-res 5358  df-ima 5359  df-pred 5924  df-ord 5970  df-on 5971  df-lim 5972  df-suc 5973  df-iota 6090  df-fun 6129  df-fn 6130  df-f 6131  df-f1 6132  df-fo 6133  df-f1o 6134  df-fv 6135  df-ov 6913  df-oprab 6914  df-mpt2 6915  df-om 7332  df-wrecs 7677  df-recs 7739  df-rdg 7777  df-1o 7831  df-2o 7832  df-oadd 7835  df-omul 7836  df-oexp 7837 This theorem is referenced by:  oelimcl  7952  oaabs2  7997  omabs  7999
 Copyright terms: Public domain W3C validator