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

Theorem oen0 8190
 Description: Ordinal exponentiation with a nonzero mantissa is nonzero. Proposition 8.32 of [TakeutiZaring] p. 67. (Contributed by NM, 4-Jan-2005.)
Assertion
Ref Expression
oen0 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴o 𝐵))

Proof of Theorem oen0
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 7141 . . . . . 6 (𝑥 = ∅ → (𝐴o 𝑥) = (𝐴o ∅))
21eleq2d 2896 . . . . 5 (𝑥 = ∅ → (∅ ∈ (𝐴o 𝑥) ↔ ∅ ∈ (𝐴o ∅)))
3 oveq2 7141 . . . . . 6 (𝑥 = 𝑦 → (𝐴o 𝑥) = (𝐴o 𝑦))
43eleq2d 2896 . . . . 5 (𝑥 = 𝑦 → (∅ ∈ (𝐴o 𝑥) ↔ ∅ ∈ (𝐴o 𝑦)))
5 oveq2 7141 . . . . . 6 (𝑥 = suc 𝑦 → (𝐴o 𝑥) = (𝐴o suc 𝑦))
65eleq2d 2896 . . . . 5 (𝑥 = suc 𝑦 → (∅ ∈ (𝐴o 𝑥) ↔ ∅ ∈ (𝐴o suc 𝑦)))
7 oveq2 7141 . . . . . 6 (𝑥 = 𝐵 → (𝐴o 𝑥) = (𝐴o 𝐵))
87eleq2d 2896 . . . . 5 (𝑥 = 𝐵 → (∅ ∈ (𝐴o 𝑥) ↔ ∅ ∈ (𝐴o 𝐵)))
9 0lt1o 8107 . . . . . . 7 ∅ ∈ 1o
10 oe0 8125 . . . . . . 7 (𝐴 ∈ On → (𝐴o ∅) = 1o)
119, 10eleqtrrid 2918 . . . . . 6 (𝐴 ∈ On → ∅ ∈ (𝐴o ∅))
1211adantr 483 . . . . 5 ((𝐴 ∈ On ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴o ∅))
13 oecl 8140 . . . . . . . . . . 11 ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴o 𝑦) ∈ On)
14 omordi 8170 . . . . . . . . . . . 12 (((𝐴 ∈ On ∧ (𝐴o 𝑦) ∈ On) ∧ ∅ ∈ (𝐴o 𝑦)) → (∅ ∈ 𝐴 → ((𝐴o 𝑦) ·o ∅) ∈ ((𝐴o 𝑦) ·o 𝐴)))
15 om0 8120 . . . . . . . . . . . . . 14 ((𝐴o 𝑦) ∈ On → ((𝐴o 𝑦) ·o ∅) = ∅)
1615eleq1d 2895 . . . . . . . . . . . . 13 ((𝐴o 𝑦) ∈ On → (((𝐴o 𝑦) ·o ∅) ∈ ((𝐴o 𝑦) ·o 𝐴) ↔ ∅ ∈ ((𝐴o 𝑦) ·o 𝐴)))
1716ad2antlr 725 . . . . . . . . . . . 12 (((𝐴 ∈ On ∧ (𝐴o 𝑦) ∈ On) ∧ ∅ ∈ (𝐴o 𝑦)) → (((𝐴o 𝑦) ·o ∅) ∈ ((𝐴o 𝑦) ·o 𝐴) ↔ ∅ ∈ ((𝐴o 𝑦) ·o 𝐴)))
1814, 17sylibd 241 . . . . . . . . . . 11 (((𝐴 ∈ On ∧ (𝐴o 𝑦) ∈ On) ∧ ∅ ∈ (𝐴o 𝑦)) → (∅ ∈ 𝐴 → ∅ ∈ ((𝐴o 𝑦) ·o 𝐴)))
1913, 18syldanl 603 . . . . . . . . . 10 (((𝐴 ∈ On ∧ 𝑦 ∈ On) ∧ ∅ ∈ (𝐴o 𝑦)) → (∅ ∈ 𝐴 → ∅ ∈ ((𝐴o 𝑦) ·o 𝐴)))
20 oesuc 8130 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴o suc 𝑦) = ((𝐴o 𝑦) ·o 𝐴))
2120eleq2d 2896 . . . . . . . . . . 11 ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (∅ ∈ (𝐴o suc 𝑦) ↔ ∅ ∈ ((𝐴o 𝑦) ·o 𝐴)))
2221adantr 483 . . . . . . . . . 10 (((𝐴 ∈ On ∧ 𝑦 ∈ On) ∧ ∅ ∈ (𝐴o 𝑦)) → (∅ ∈ (𝐴o suc 𝑦) ↔ ∅ ∈ ((𝐴o 𝑦) ·o 𝐴)))
2319, 22sylibrd 261 . . . . . . . . 9 (((𝐴 ∈ On ∧ 𝑦 ∈ On) ∧ ∅ ∈ (𝐴o 𝑦)) → (∅ ∈ 𝐴 → ∅ ∈ (𝐴o suc 𝑦)))
2423exp31 422 . . . . . . . 8 (𝐴 ∈ On → (𝑦 ∈ On → (∅ ∈ (𝐴o 𝑦) → (∅ ∈ 𝐴 → ∅ ∈ (𝐴o suc 𝑦)))))
2524com12 32 . . . . . . 7 (𝑦 ∈ On → (𝐴 ∈ On → (∅ ∈ (𝐴o 𝑦) → (∅ ∈ 𝐴 → ∅ ∈ (𝐴o suc 𝑦)))))
2625com34 91 . . . . . 6 (𝑦 ∈ On → (𝐴 ∈ On → (∅ ∈ 𝐴 → (∅ ∈ (𝐴o 𝑦) → ∅ ∈ (𝐴o suc 𝑦)))))
2726impd 413 . . . . 5 (𝑦 ∈ On → ((𝐴 ∈ On ∧ ∅ ∈ 𝐴) → (∅ ∈ (𝐴o 𝑦) → ∅ ∈ (𝐴o suc 𝑦))))
28 0ellim 6229 . . . . . . . . . . . 12 (Lim 𝑥 → ∅ ∈ 𝑥)
29 eqimss2 4003 . . . . . . . . . . . . 13 ((𝐴o ∅) = 1o → 1o ⊆ (𝐴o ∅))
3010, 29syl 17 . . . . . . . . . . . 12 (𝐴 ∈ On → 1o ⊆ (𝐴o ∅))
31 oveq2 7141 . . . . . . . . . . . . . 14 (𝑦 = ∅ → (𝐴o 𝑦) = (𝐴o ∅))
3231sseq2d 3978 . . . . . . . . . . . . 13 (𝑦 = ∅ → (1o ⊆ (𝐴o 𝑦) ↔ 1o ⊆ (𝐴o ∅)))
3332rspcev 3602 . . . . . . . . . . . 12 ((∅ ∈ 𝑥 ∧ 1o ⊆ (𝐴o ∅)) → ∃𝑦𝑥 1o ⊆ (𝐴o 𝑦))
3428, 30, 33syl2an 597 . . . . . . . . . . 11 ((Lim 𝑥𝐴 ∈ On) → ∃𝑦𝑥 1o ⊆ (𝐴o 𝑦))
35 ssiun 4946 . . . . . . . . . . 11 (∃𝑦𝑥 1o ⊆ (𝐴o 𝑦) → 1o 𝑦𝑥 (𝐴o 𝑦))
3634, 35syl 17 . . . . . . . . . 10 ((Lim 𝑥𝐴 ∈ On) → 1o 𝑦𝑥 (𝐴o 𝑦))
3736adantrr 715 . . . . . . . . 9 ((Lim 𝑥 ∧ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) → 1o 𝑦𝑥 (𝐴o 𝑦))
38 vex 3476 . . . . . . . . . . . 12 𝑥 ∈ V
39 oelim 8137 . . . . . . . . . . . 12 (((𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ ∅ ∈ 𝐴) → (𝐴o 𝑥) = 𝑦𝑥 (𝐴o 𝑦))
4038, 39mpanlr1 704 . . . . . . . . . . 11 (((𝐴 ∈ On ∧ Lim 𝑥) ∧ ∅ ∈ 𝐴) → (𝐴o 𝑥) = 𝑦𝑥 (𝐴o 𝑦))
4140anasss 469 . . . . . . . . . 10 ((𝐴 ∈ On ∧ (Lim 𝑥 ∧ ∅ ∈ 𝐴)) → (𝐴o 𝑥) = 𝑦𝑥 (𝐴o 𝑦))
4241an12s 647 . . . . . . . . 9 ((Lim 𝑥 ∧ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) → (𝐴o 𝑥) = 𝑦𝑥 (𝐴o 𝑦))
4337, 42sseqtrrd 3987 . . . . . . . 8 ((Lim 𝑥 ∧ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) → 1o ⊆ (𝐴o 𝑥))
44 limelon 6230 . . . . . . . . . . . 12 ((𝑥 ∈ V ∧ Lim 𝑥) → 𝑥 ∈ On)
4538, 44mpan 688 . . . . . . . . . . 11 (Lim 𝑥𝑥 ∈ On)
46 oecl 8140 . . . . . . . . . . . 12 ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴o 𝑥) ∈ On)
4746ancoms 461 . . . . . . . . . . 11 ((𝑥 ∈ On ∧ 𝐴 ∈ On) → (𝐴o 𝑥) ∈ On)
4845, 47sylan 582 . . . . . . . . . 10 ((Lim 𝑥𝐴 ∈ On) → (𝐴o 𝑥) ∈ On)
49 eloni 6177 . . . . . . . . . 10 ((𝐴o 𝑥) ∈ On → Ord (𝐴o 𝑥))
50 ordgt0ge1 8100 . . . . . . . . . 10 (Ord (𝐴o 𝑥) → (∅ ∈ (𝐴o 𝑥) ↔ 1o ⊆ (𝐴o 𝑥)))
5148, 49, 503syl 18 . . . . . . . . 9 ((Lim 𝑥𝐴 ∈ On) → (∅ ∈ (𝐴o 𝑥) ↔ 1o ⊆ (𝐴o 𝑥)))
5251adantrr 715 . . . . . . . 8 ((Lim 𝑥 ∧ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) → (∅ ∈ (𝐴o 𝑥) ↔ 1o ⊆ (𝐴o 𝑥)))
5343, 52mpbird 259 . . . . . . 7 ((Lim 𝑥 ∧ (𝐴 ∈ On ∧ ∅ ∈ 𝐴)) → ∅ ∈ (𝐴o 𝑥))
5453ex 415 . . . . . 6 (Lim 𝑥 → ((𝐴 ∈ On ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴o 𝑥)))
5554a1dd 50 . . . . 5 (Lim 𝑥 → ((𝐴 ∈ On ∧ ∅ ∈ 𝐴) → (∀𝑦𝑥 ∅ ∈ (𝐴o 𝑦) → ∅ ∈ (𝐴o 𝑥))))
562, 4, 6, 8, 12, 27, 55tfinds3 7557 . . . 4 (𝐵 ∈ On → ((𝐴 ∈ On ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴o 𝐵)))
5756expd 418 . . 3 (𝐵 ∈ On → (𝐴 ∈ On → (∅ ∈ 𝐴 → ∅ ∈ (𝐴o 𝐵))))
5857com12 32 . 2 (𝐴 ∈ On → (𝐵 ∈ On → (∅ ∈ 𝐴 → ∅ ∈ (𝐴o 𝐵))))
5958imp31 420 1 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴o 𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ∀wral 3125  ∃wrex 3126  Vcvv 3473   ⊆ wss 3913  ∅c0 4269  ∪ ciun 4895  Ord word 6166  Oncon0 6167  Lim wlim 6168  suc csuc 6169  (class class class)co 7133  1oc1o 8073   ·o comu 8078   ↑o coe 8079 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5242  ax-pr 5306  ax-un 7439 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-ral 3130  df-rex 3131  df-reu 3132  df-rab 3134  df-v 3475  df-sbc 3753  df-csb 3861  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4270  df-if 4444  df-pw 4517  df-sn 4544  df-pr 4546  df-tp 4548  df-op 4550  df-uni 4815  df-iun 4897  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5436  df-eprel 5441  df-po 5450  df-so 5451  df-fr 5490  df-we 5492  df-xp 5537  df-rel 5538  df-cnv 5539  df-co 5540  df-dm 5541  df-rn 5542  df-res 5543  df-ima 5544  df-pred 6124  df-ord 6170  df-on 6171  df-lim 6172  df-suc 6173  df-iota 6290  df-fun 6333  df-fn 6334  df-f 6335  df-f1 6336  df-fo 6337  df-f1o 6338  df-fv 6339  df-ov 7136  df-oprab 7137  df-mpo 7138  df-om 7559  df-wrecs 7925  df-recs 7986  df-rdg 8024  df-1o 8080  df-oadd 8084  df-omul 8085  df-oexp 8086 This theorem is referenced by:  oeordi  8191  oeordsuc  8198  oeoelem  8202  oelimcl  8204  oeeui  8206  cantnflt  9113  cnfcom  9141  infxpenc  9422  infxpenc2  9426
 Copyright terms: Public domain W3C validator