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

Theorem oecl 8172
 Description: Closure law for ordinal exponentiation. (Contributed by NM, 1-Jan-2005.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
Assertion
Ref Expression
oecl ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴o 𝐵) ∈ On)

Proof of Theorem oecl
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 7158 . . . . . . . 8 (𝐵 = ∅ → (∅ ↑o 𝐵) = (∅ ↑o ∅))
2 oe0m0 8155 . . . . . . . . 9 (∅ ↑o ∅) = 1o
3 1on 8119 . . . . . . . . 9 1o ∈ On
42, 3eqeltri 2848 . . . . . . . 8 (∅ ↑o ∅) ∈ On
51, 4eqeltrdi 2860 . . . . . . 7 (𝐵 = ∅ → (∅ ↑o 𝐵) ∈ On)
65adantl 485 . . . . . 6 ((𝐵 ∈ On ∧ 𝐵 = ∅) → (∅ ↑o 𝐵) ∈ On)
7 oe0m1 8156 . . . . . . . . 9 (𝐵 ∈ On → (∅ ∈ 𝐵 ↔ (∅ ↑o 𝐵) = ∅))
87biimpa 480 . . . . . . . 8 ((𝐵 ∈ On ∧ ∅ ∈ 𝐵) → (∅ ↑o 𝐵) = ∅)
9 0elon 6222 . . . . . . . 8 ∅ ∈ On
108, 9eqeltrdi 2860 . . . . . . 7 ((𝐵 ∈ On ∧ ∅ ∈ 𝐵) → (∅ ↑o 𝐵) ∈ On)
1110adantll 713 . . . . . 6 (((𝐵 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈ 𝐵) → (∅ ↑o 𝐵) ∈ On)
126, 11oe0lem 8148 . . . . 5 ((𝐵 ∈ On ∧ 𝐵 ∈ On) → (∅ ↑o 𝐵) ∈ On)
1312anidms 570 . . . 4 (𝐵 ∈ On → (∅ ↑o 𝐵) ∈ On)
14 oveq1 7157 . . . . 5 (𝐴 = ∅ → (𝐴o 𝐵) = (∅ ↑o 𝐵))
1514eleq1d 2836 . . . 4 (𝐴 = ∅ → ((𝐴o 𝐵) ∈ On ↔ (∅ ↑o 𝐵) ∈ On))
1613, 15syl5ibr 249 . . 3 (𝐴 = ∅ → (𝐵 ∈ On → (𝐴o 𝐵) ∈ On))
1716impcom 411 . 2 ((𝐵 ∈ On ∧ 𝐴 = ∅) → (𝐴o 𝐵) ∈ On)
18 oveq2 7158 . . . . . . 7 (𝑥 = ∅ → (𝐴o 𝑥) = (𝐴o ∅))
1918eleq1d 2836 . . . . . 6 (𝑥 = ∅ → ((𝐴o 𝑥) ∈ On ↔ (𝐴o ∅) ∈ On))
20 oveq2 7158 . . . . . . 7 (𝑥 = 𝑦 → (𝐴o 𝑥) = (𝐴o 𝑦))
2120eleq1d 2836 . . . . . 6 (𝑥 = 𝑦 → ((𝐴o 𝑥) ∈ On ↔ (𝐴o 𝑦) ∈ On))
22 oveq2 7158 . . . . . . 7 (𝑥 = suc 𝑦 → (𝐴o 𝑥) = (𝐴o suc 𝑦))
2322eleq1d 2836 . . . . . 6 (𝑥 = suc 𝑦 → ((𝐴o 𝑥) ∈ On ↔ (𝐴o suc 𝑦) ∈ On))
24 oveq2 7158 . . . . . . 7 (𝑥 = 𝐵 → (𝐴o 𝑥) = (𝐴o 𝐵))
2524eleq1d 2836 . . . . . 6 (𝑥 = 𝐵 → ((𝐴o 𝑥) ∈ On ↔ (𝐴o 𝐵) ∈ On))
26 oe0 8157 . . . . . . . 8 (𝐴 ∈ On → (𝐴o ∅) = 1o)
2726, 3eqeltrdi 2860 . . . . . . 7 (𝐴 ∈ On → (𝐴o ∅) ∈ On)
2827adantr 484 . . . . . 6 ((𝐴 ∈ On ∧ ∅ ∈ 𝐴) → (𝐴o ∅) ∈ On)
29 omcl 8171 . . . . . . . . . . 11 (((𝐴o 𝑦) ∈ On ∧ 𝐴 ∈ On) → ((𝐴o 𝑦) ·o 𝐴) ∈ On)
3029expcom 417 . . . . . . . . . 10 (𝐴 ∈ On → ((𝐴o 𝑦) ∈ On → ((𝐴o 𝑦) ·o 𝐴) ∈ On))
3130adantr 484 . . . . . . . . 9 ((𝐴 ∈ On ∧ 𝑦 ∈ On) → ((𝐴o 𝑦) ∈ On → ((𝐴o 𝑦) ·o 𝐴) ∈ On))
32 oesuc 8162 . . . . . . . . . 10 ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴o suc 𝑦) = ((𝐴o 𝑦) ·o 𝐴))
3332eleq1d 2836 . . . . . . . . 9 ((𝐴 ∈ On ∧ 𝑦 ∈ On) → ((𝐴o suc 𝑦) ∈ On ↔ ((𝐴o 𝑦) ·o 𝐴) ∈ On))
3431, 33sylibrd 262 . . . . . . . 8 ((𝐴 ∈ On ∧ 𝑦 ∈ On) → ((𝐴o 𝑦) ∈ On → (𝐴o suc 𝑦) ∈ On))
3534expcom 417 . . . . . . 7 (𝑦 ∈ On → (𝐴 ∈ On → ((𝐴o 𝑦) ∈ On → (𝐴o suc 𝑦) ∈ On)))
3635adantrd 495 . . . . . 6 (𝑦 ∈ On → ((𝐴 ∈ On ∧ ∅ ∈ 𝐴) → ((𝐴o 𝑦) ∈ On → (𝐴o suc 𝑦) ∈ On)))
37 vex 3413 . . . . . . . . 9 𝑥 ∈ V
38 iunon 7986 . . . . . . . . 9 ((𝑥 ∈ V ∧ ∀𝑦𝑥 (𝐴o 𝑦) ∈ On) → 𝑦𝑥 (𝐴o 𝑦) ∈ On)
3937, 38mpan 689 . . . . . . . 8 (∀𝑦𝑥 (𝐴o 𝑦) ∈ On → 𝑦𝑥 (𝐴o 𝑦) ∈ On)
40 oelim 8169 . . . . . . . . . . . 12 (((𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ ∅ ∈ 𝐴) → (𝐴o 𝑥) = 𝑦𝑥 (𝐴o 𝑦))
4137, 40mpanlr1 705 . . . . . . . . . . 11 (((𝐴 ∈ On ∧ Lim 𝑥) ∧ ∅ ∈ 𝐴) → (𝐴o 𝑥) = 𝑦𝑥 (𝐴o 𝑦))
4241anasss 470 . . . . . . . . . 10 ((𝐴 ∈ On ∧ (Lim 𝑥 ∧ ∅ ∈ 𝐴)) → (𝐴o 𝑥) = 𝑦𝑥 (𝐴o 𝑦))
4342an12s 648 . . . . . . . . 9 ((Lim 𝑥 ∧ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) → (𝐴o 𝑥) = 𝑦𝑥 (𝐴o 𝑦))
4443eleq1d 2836 . . . . . . . 8 ((Lim 𝑥 ∧ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) → ((𝐴o 𝑥) ∈ On ↔ 𝑦𝑥 (𝐴o 𝑦) ∈ On))
4539, 44syl5ibr 249 . . . . . . 7 ((Lim 𝑥 ∧ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) → (∀𝑦𝑥 (𝐴o 𝑦) ∈ On → (𝐴o 𝑥) ∈ On))
4645ex 416 . . . . . 6 (Lim 𝑥 → ((𝐴 ∈ On ∧ ∅ ∈ 𝐴) → (∀𝑦𝑥 (𝐴o 𝑦) ∈ On → (𝐴o 𝑥) ∈ On)))
4719, 21, 23, 25, 28, 36, 46tfinds3 7578 . . . . 5 (𝐵 ∈ On → ((𝐴 ∈ On ∧ ∅ ∈ 𝐴) → (𝐴o 𝐵) ∈ On))
4847expd 419 . . . 4 (𝐵 ∈ On → (𝐴 ∈ On → (∅ ∈ 𝐴 → (𝐴o 𝐵) ∈ On)))
4948com12 32 . . 3 (𝐴 ∈ On → (𝐵 ∈ On → (∅ ∈ 𝐴 → (𝐴o 𝐵) ∈ On)))
5049imp31 421 . 2 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈ 𝐴) → (𝐴o 𝐵) ∈ On)
5117, 50oe0lem 8148 1 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴o 𝐵) ∈ On)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3070  Vcvv 3409  ∅c0 4225  ∪ ciun 4883  Oncon0 6169  Lim wlim 6170  suc csuc 6171  (class class class)co 7150  1oc1o 8105   ·o comu 8110   ↑o coe 8111 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5156  ax-sep 5169  ax-nul 5176  ax-pr 5298  ax-un 7459 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-reu 3077  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-pss 3877  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-tp 4527  df-op 4529  df-uni 4799  df-iun 4885  df-br 5033  df-opab 5095  df-mpt 5113  df-tr 5139  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5483  df-we 5485  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7580  df-wrecs 7957  df-recs 8018  df-rdg 8056  df-1o 8112  df-oadd 8116  df-omul 8117  df-oexp 8118 This theorem is referenced by:  oen0  8222  oeordi  8223  oeord  8224  oecan  8225  oeword  8226  oewordri  8228  oeworde  8229  oeordsuc  8230  oeoalem  8232  oeoa  8233  oeoelem  8234  oeoe  8235  oelimcl  8236  oeeulem  8237  oeeui  8238  oaabs2  8282  omabs  8284  cantnfle  9167  cantnflt  9168  cantnfp1  9177  cantnflem1d  9184  cantnflem1  9185  cantnflem2  9186  cantnflem3  9187  cantnflem4  9188  cantnf  9189  oemapwe  9190  cantnffval2  9191  cnfcomlem  9195  cnfcom  9196  cnfcom3lem  9199  cnfcom3  9200  infxpenc  9478
 Copyright terms: Public domain W3C validator