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

Theorem oecl 7826
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) → (𝐴𝑜 𝐵) ∈ On)

Proof of Theorem oecl
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 6854 . . . . . . . 8 (𝐵 = ∅ → (∅ ↑𝑜 𝐵) = (∅ ↑𝑜 ∅))
2 oe0m0 7809 . . . . . . . . 9 (∅ ↑𝑜 ∅) = 1𝑜
3 1on 7775 . . . . . . . . 9 1𝑜 ∈ On
42, 3eqeltri 2840 . . . . . . . 8 (∅ ↑𝑜 ∅) ∈ On
51, 4syl6eqel 2852 . . . . . . 7 (𝐵 = ∅ → (∅ ↑𝑜 𝐵) ∈ On)
65adantl 473 . . . . . 6 ((𝐵 ∈ On ∧ 𝐵 = ∅) → (∅ ↑𝑜 𝐵) ∈ On)
7 oe0m1 7810 . . . . . . . . 9 (𝐵 ∈ On → (∅ ∈ 𝐵 ↔ (∅ ↑𝑜 𝐵) = ∅))
87biimpa 468 . . . . . . . 8 ((𝐵 ∈ On ∧ ∅ ∈ 𝐵) → (∅ ↑𝑜 𝐵) = ∅)
9 0elon 5963 . . . . . . . 8 ∅ ∈ On
108, 9syl6eqel 2852 . . . . . . 7 ((𝐵 ∈ On ∧ ∅ ∈ 𝐵) → (∅ ↑𝑜 𝐵) ∈ On)
1110adantll 705 . . . . . 6 (((𝐵 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈ 𝐵) → (∅ ↑𝑜 𝐵) ∈ On)
126, 11oe0lem 7802 . . . . 5 ((𝐵 ∈ On ∧ 𝐵 ∈ On) → (∅ ↑𝑜 𝐵) ∈ On)
1312anidms 562 . . . 4 (𝐵 ∈ On → (∅ ↑𝑜 𝐵) ∈ On)
14 oveq1 6853 . . . . 5 (𝐴 = ∅ → (𝐴𝑜 𝐵) = (∅ ↑𝑜 𝐵))
1514eleq1d 2829 . . . 4 (𝐴 = ∅ → ((𝐴𝑜 𝐵) ∈ On ↔ (∅ ↑𝑜 𝐵) ∈ On))
1613, 15syl5ibr 237 . . 3 (𝐴 = ∅ → (𝐵 ∈ On → (𝐴𝑜 𝐵) ∈ On))
1716impcom 396 . 2 ((𝐵 ∈ On ∧ 𝐴 = ∅) → (𝐴𝑜 𝐵) ∈ On)
18 oveq2 6854 . . . . . . 7 (𝑥 = ∅ → (𝐴𝑜 𝑥) = (𝐴𝑜 ∅))
1918eleq1d 2829 . . . . . 6 (𝑥 = ∅ → ((𝐴𝑜 𝑥) ∈ On ↔ (𝐴𝑜 ∅) ∈ On))
20 oveq2 6854 . . . . . . 7 (𝑥 = 𝑦 → (𝐴𝑜 𝑥) = (𝐴𝑜 𝑦))
2120eleq1d 2829 . . . . . 6 (𝑥 = 𝑦 → ((𝐴𝑜 𝑥) ∈ On ↔ (𝐴𝑜 𝑦) ∈ On))
22 oveq2 6854 . . . . . . 7 (𝑥 = suc 𝑦 → (𝐴𝑜 𝑥) = (𝐴𝑜 suc 𝑦))
2322eleq1d 2829 . . . . . 6 (𝑥 = suc 𝑦 → ((𝐴𝑜 𝑥) ∈ On ↔ (𝐴𝑜 suc 𝑦) ∈ On))
24 oveq2 6854 . . . . . . 7 (𝑥 = 𝐵 → (𝐴𝑜 𝑥) = (𝐴𝑜 𝐵))
2524eleq1d 2829 . . . . . 6 (𝑥 = 𝐵 → ((𝐴𝑜 𝑥) ∈ On ↔ (𝐴𝑜 𝐵) ∈ On))
26 oe0 7811 . . . . . . . 8 (𝐴 ∈ On → (𝐴𝑜 ∅) = 1𝑜)
2726, 3syl6eqel 2852 . . . . . . 7 (𝐴 ∈ On → (𝐴𝑜 ∅) ∈ On)
2827adantr 472 . . . . . 6 ((𝐴 ∈ On ∧ ∅ ∈ 𝐴) → (𝐴𝑜 ∅) ∈ On)
29 omcl 7825 . . . . . . . . . . 11 (((𝐴𝑜 𝑦) ∈ On ∧ 𝐴 ∈ On) → ((𝐴𝑜 𝑦) ·𝑜 𝐴) ∈ On)
3029expcom 402 . . . . . . . . . 10 (𝐴 ∈ On → ((𝐴𝑜 𝑦) ∈ On → ((𝐴𝑜 𝑦) ·𝑜 𝐴) ∈ On))
3130adantr 472 . . . . . . . . 9 ((𝐴 ∈ On ∧ 𝑦 ∈ On) → ((𝐴𝑜 𝑦) ∈ On → ((𝐴𝑜 𝑦) ·𝑜 𝐴) ∈ On))
32 oesuc 7816 . . . . . . . . . 10 ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴𝑜 suc 𝑦) = ((𝐴𝑜 𝑦) ·𝑜 𝐴))
3332eleq1d 2829 . . . . . . . . 9 ((𝐴 ∈ On ∧ 𝑦 ∈ On) → ((𝐴𝑜 suc 𝑦) ∈ On ↔ ((𝐴𝑜 𝑦) ·𝑜 𝐴) ∈ On))
3431, 33sylibrd 250 . . . . . . . 8 ((𝐴 ∈ On ∧ 𝑦 ∈ On) → ((𝐴𝑜 𝑦) ∈ On → (𝐴𝑜 suc 𝑦) ∈ On))
3534expcom 402 . . . . . . 7 (𝑦 ∈ On → (𝐴 ∈ On → ((𝐴𝑜 𝑦) ∈ On → (𝐴𝑜 suc 𝑦) ∈ On)))
3635adantrd 485 . . . . . 6 (𝑦 ∈ On → ((𝐴 ∈ On ∧ ∅ ∈ 𝐴) → ((𝐴𝑜 𝑦) ∈ On → (𝐴𝑜 suc 𝑦) ∈ On)))
37 vex 3353 . . . . . . . . 9 𝑥 ∈ V
38 iunon 7644 . . . . . . . . 9 ((𝑥 ∈ V ∧ ∀𝑦𝑥 (𝐴𝑜 𝑦) ∈ On) → 𝑦𝑥 (𝐴𝑜 𝑦) ∈ On)
3937, 38mpan 681 . . . . . . . 8 (∀𝑦𝑥 (𝐴𝑜 𝑦) ∈ On → 𝑦𝑥 (𝐴𝑜 𝑦) ∈ On)
40 oelim 7823 . . . . . . . . . . . 12 (((𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ ∅ ∈ 𝐴) → (𝐴𝑜 𝑥) = 𝑦𝑥 (𝐴𝑜 𝑦))
4137, 40mpanlr1 697 . . . . . . . . . . 11 (((𝐴 ∈ On ∧ Lim 𝑥) ∧ ∅ ∈ 𝐴) → (𝐴𝑜 𝑥) = 𝑦𝑥 (𝐴𝑜 𝑦))
4241anasss 458 . . . . . . . . . 10 ((𝐴 ∈ On ∧ (Lim 𝑥 ∧ ∅ ∈ 𝐴)) → (𝐴𝑜 𝑥) = 𝑦𝑥 (𝐴𝑜 𝑦))
4342an12s 639 . . . . . . . . 9 ((Lim 𝑥 ∧ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) → (𝐴𝑜 𝑥) = 𝑦𝑥 (𝐴𝑜 𝑦))
4443eleq1d 2829 . . . . . . . 8 ((Lim 𝑥 ∧ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) → ((𝐴𝑜 𝑥) ∈ On ↔ 𝑦𝑥 (𝐴𝑜 𝑦) ∈ On))
4539, 44syl5ibr 237 . . . . . . 7 ((Lim 𝑥 ∧ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) → (∀𝑦𝑥 (𝐴𝑜 𝑦) ∈ On → (𝐴𝑜 𝑥) ∈ On))
4645ex 401 . . . . . 6 (Lim 𝑥 → ((𝐴 ∈ On ∧ ∅ ∈ 𝐴) → (∀𝑦𝑥 (𝐴𝑜 𝑦) ∈ On → (𝐴𝑜 𝑥) ∈ On)))
4719, 21, 23, 25, 28, 36, 46tfinds3 7266 . . . . 5 (𝐵 ∈ On → ((𝐴 ∈ On ∧ ∅ ∈ 𝐴) → (𝐴𝑜 𝐵) ∈ On))
4847expd 404 . . . 4 (𝐵 ∈ On → (𝐴 ∈ On → (∅ ∈ 𝐴 → (𝐴𝑜 𝐵) ∈ On)))
4948com12 32 . . 3 (𝐴 ∈ On → (𝐵 ∈ On → (∅ ∈ 𝐴 → (𝐴𝑜 𝐵) ∈ On)))
5049imp31 408 . 2 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈ 𝐴) → (𝐴𝑜 𝐵) ∈ On)
5117, 50oe0lem 7802 1 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴𝑜 𝐵) ∈ On)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1652  wcel 2155  wral 3055  Vcvv 3350  c0 4081   ciun 4678  Oncon0 5910  Lim wlim 5911  suc csuc 5912  (class class class)co 6846  1𝑜c1o 7761   ·𝑜 comu 7766  𝑜 coe 7767
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7151
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-iun 4680  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-ov 6849  df-oprab 6850  df-mpt2 6851  df-om 7268  df-wrecs 7614  df-recs 7676  df-rdg 7714  df-1o 7768  df-oadd 7772  df-omul 7773  df-oexp 7774
This theorem is referenced by:  oen0  7875  oeordi  7876  oeord  7877  oecan  7878  oeword  7879  oewordri  7881  oeworde  7882  oeordsuc  7883  oeoalem  7885  oeoa  7886  oeoelem  7887  oeoe  7888  oelimcl  7889  oeeulem  7890  oeeui  7891  oaabs2  7934  omabs  7936  cantnfle  8787  cantnflt  8788  cantnfp1  8797  cantnflem1d  8804  cantnflem1  8805  cantnflem2  8806  cantnflem3  8807  cantnflem4  8808  cantnf  8809  oemapwe  8810  cantnffval2  8811  cnfcomlem  8815  cnfcom  8816  cnfcom3lem  8819  cnfcom3  8820  infxpenc  9096
  Copyright terms: Public domain W3C validator