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

Theorem oesuclem 7809
Description: Lemma for oesuc 7811. (Contributed by NM, 31-Dec-2004.) (Revised by Mario Carneiro, 15-Nov-2014.)
Hypotheses
Ref Expression
oesuclem.1 Lim 𝑋
oesuclem.2 (𝐵𝑋 → (rec((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴)), 1𝑜)‘suc 𝐵) = ((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴))‘(rec((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴)), 1𝑜)‘𝐵)))
Assertion
Ref Expression
oesuclem ((𝐴 ∈ On ∧ 𝐵𝑋) → (𝐴𝑜 suc 𝐵) = ((𝐴𝑜 𝐵) ·𝑜 𝐴))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hint:   𝑋(𝑥)

Proof of Theorem oesuclem
StepHypRef Expression
1 oveq1 6848 . . . 4 (𝐴 = ∅ → (𝐴𝑜 suc 𝐵) = (∅ ↑𝑜 suc 𝐵))
2 oesuclem.1 . . . . . . . 8 Lim 𝑋
3 limord 5966 . . . . . . . 8 (Lim 𝑋 → Ord 𝑋)
42, 3ax-mp 5 . . . . . . 7 Ord 𝑋
5 ordelord 5929 . . . . . . 7 ((Ord 𝑋𝐵𝑋) → Ord 𝐵)
64, 5mpan 681 . . . . . 6 (𝐵𝑋 → Ord 𝐵)
7 0elsuc 7232 . . . . . 6 (Ord 𝐵 → ∅ ∈ suc 𝐵)
86, 7syl 17 . . . . 5 (𝐵𝑋 → ∅ ∈ suc 𝐵)
9 limsuc 7246 . . . . . . 7 (Lim 𝑋 → (𝐵𝑋 ↔ suc 𝐵𝑋))
102, 9ax-mp 5 . . . . . 6 (𝐵𝑋 ↔ suc 𝐵𝑋)
11 ordelon 5931 . . . . . . . 8 ((Ord 𝑋 ∧ suc 𝐵𝑋) → suc 𝐵 ∈ On)
124, 11mpan 681 . . . . . . 7 (suc 𝐵𝑋 → suc 𝐵 ∈ On)
13 oe0m1 7805 . . . . . . 7 (suc 𝐵 ∈ On → (∅ ∈ suc 𝐵 ↔ (∅ ↑𝑜 suc 𝐵) = ∅))
1412, 13syl 17 . . . . . 6 (suc 𝐵𝑋 → (∅ ∈ suc 𝐵 ↔ (∅ ↑𝑜 suc 𝐵) = ∅))
1510, 14sylbi 208 . . . . 5 (𝐵𝑋 → (∅ ∈ suc 𝐵 ↔ (∅ ↑𝑜 suc 𝐵) = ∅))
168, 15mpbid 223 . . . 4 (𝐵𝑋 → (∅ ↑𝑜 suc 𝐵) = ∅)
171, 16sylan9eqr 2820 . . 3 ((𝐵𝑋𝐴 = ∅) → (𝐴𝑜 suc 𝐵) = ∅)
18 oveq1 6848 . . . . 5 (𝐴 = ∅ → (𝐴𝑜 𝐵) = (∅ ↑𝑜 𝐵))
19 id 22 . . . . 5 (𝐴 = ∅ → 𝐴 = ∅)
2018, 19oveq12d 6859 . . . 4 (𝐴 = ∅ → ((𝐴𝑜 𝐵) ·𝑜 𝐴) = ((∅ ↑𝑜 𝐵) ·𝑜 ∅))
21 ordelon 5931 . . . . . . 7 ((Ord 𝑋𝐵𝑋) → 𝐵 ∈ On)
224, 21mpan 681 . . . . . 6 (𝐵𝑋𝐵 ∈ On)
23 oveq2 6849 . . . . . . . . 9 (𝐵 = ∅ → (∅ ↑𝑜 𝐵) = (∅ ↑𝑜 ∅))
24 oe0m0 7804 . . . . . . . . . 10 (∅ ↑𝑜 ∅) = 1𝑜
25 1on 7770 . . . . . . . . . 10 1𝑜 ∈ On
2624, 25eqeltri 2839 . . . . . . . . 9 (∅ ↑𝑜 ∅) ∈ On
2723, 26syl6eqel 2851 . . . . . . . 8 (𝐵 = ∅ → (∅ ↑𝑜 𝐵) ∈ On)
2827adantl 473 . . . . . . 7 ((𝐵𝑋𝐵 = ∅) → (∅ ↑𝑜 𝐵) ∈ On)
29 oe0m1 7805 . . . . . . . . . . 11 (𝐵 ∈ On → (∅ ∈ 𝐵 ↔ (∅ ↑𝑜 𝐵) = ∅))
3022, 29syl 17 . . . . . . . . . 10 (𝐵𝑋 → (∅ ∈ 𝐵 ↔ (∅ ↑𝑜 𝐵) = ∅))
3130biimpa 468 . . . . . . . . 9 ((𝐵𝑋 ∧ ∅ ∈ 𝐵) → (∅ ↑𝑜 𝐵) = ∅)
32 0elon 5960 . . . . . . . . 9 ∅ ∈ On
3331, 32syl6eqel 2851 . . . . . . . 8 ((𝐵𝑋 ∧ ∅ ∈ 𝐵) → (∅ ↑𝑜 𝐵) ∈ On)
3433adantll 705 . . . . . . 7 (((𝐵 ∈ On ∧ 𝐵𝑋) ∧ ∅ ∈ 𝐵) → (∅ ↑𝑜 𝐵) ∈ On)
3528, 34oe0lem 7797 . . . . . 6 ((𝐵 ∈ On ∧ 𝐵𝑋) → (∅ ↑𝑜 𝐵) ∈ On)
3622, 35mpancom 679 . . . . 5 (𝐵𝑋 → (∅ ↑𝑜 𝐵) ∈ On)
37 om0 7801 . . . . 5 ((∅ ↑𝑜 𝐵) ∈ On → ((∅ ↑𝑜 𝐵) ·𝑜 ∅) = ∅)
3836, 37syl 17 . . . 4 (𝐵𝑋 → ((∅ ↑𝑜 𝐵) ·𝑜 ∅) = ∅)
3920, 38sylan9eqr 2820 . . 3 ((𝐵𝑋𝐴 = ∅) → ((𝐴𝑜 𝐵) ·𝑜 𝐴) = ∅)
4017, 39eqtr4d 2801 . 2 ((𝐵𝑋𝐴 = ∅) → (𝐴𝑜 suc 𝐵) = ((𝐴𝑜 𝐵) ·𝑜 𝐴))
41 oesuclem.2 . . . 4 (𝐵𝑋 → (rec((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴)), 1𝑜)‘suc 𝐵) = ((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴))‘(rec((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴)), 1𝑜)‘𝐵)))
4241ad2antlr 718 . . 3 (((𝐴 ∈ On ∧ 𝐵𝑋) ∧ ∅ ∈ 𝐴) → (rec((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴)), 1𝑜)‘suc 𝐵) = ((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴))‘(rec((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴)), 1𝑜)‘𝐵)))
4310, 12sylbi 208 . . . 4 (𝐵𝑋 → suc 𝐵 ∈ On)
44 oevn0 7799 . . . 4 (((𝐴 ∈ On ∧ suc 𝐵 ∈ On) ∧ ∅ ∈ 𝐴) → (𝐴𝑜 suc 𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴)), 1𝑜)‘suc 𝐵))
4543, 44sylanl2 671 . . 3 (((𝐴 ∈ On ∧ 𝐵𝑋) ∧ ∅ ∈ 𝐴) → (𝐴𝑜 suc 𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴)), 1𝑜)‘suc 𝐵))
46 ovex 6873 . . . . 5 (𝐴𝑜 𝐵) ∈ V
47 oveq1 6848 . . . . . 6 (𝑥 = (𝐴𝑜 𝐵) → (𝑥 ·𝑜 𝐴) = ((𝐴𝑜 𝐵) ·𝑜 𝐴))
48 eqid 2764 . . . . . 6 (𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴)) = (𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴))
49 ovex 6873 . . . . . 6 ((𝐴𝑜 𝐵) ·𝑜 𝐴) ∈ V
5047, 48, 49fvmpt 6470 . . . . 5 ((𝐴𝑜 𝐵) ∈ V → ((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴))‘(𝐴𝑜 𝐵)) = ((𝐴𝑜 𝐵) ·𝑜 𝐴))
5146, 50ax-mp 5 . . . 4 ((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴))‘(𝐴𝑜 𝐵)) = ((𝐴𝑜 𝐵) ·𝑜 𝐴)
52 oevn0 7799 . . . . . 6 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈ 𝐴) → (𝐴𝑜 𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴)), 1𝑜)‘𝐵))
5322, 52sylanl2 671 . . . . 5 (((𝐴 ∈ On ∧ 𝐵𝑋) ∧ ∅ ∈ 𝐴) → (𝐴𝑜 𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴)), 1𝑜)‘𝐵))
5453fveq2d 6378 . . . 4 (((𝐴 ∈ On ∧ 𝐵𝑋) ∧ ∅ ∈ 𝐴) → ((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴))‘(𝐴𝑜 𝐵)) = ((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴))‘(rec((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴)), 1𝑜)‘𝐵)))
5551, 54syl5eqr 2812 . . 3 (((𝐴 ∈ On ∧ 𝐵𝑋) ∧ ∅ ∈ 𝐴) → ((𝐴𝑜 𝐵) ·𝑜 𝐴) = ((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴))‘(rec((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴)), 1𝑜)‘𝐵)))
5642, 45, 553eqtr4d 2808 . 2 (((𝐴 ∈ On ∧ 𝐵𝑋) ∧ ∅ ∈ 𝐴) → (𝐴𝑜 suc 𝐵) = ((𝐴𝑜 𝐵) ·𝑜 𝐴))
5740, 56oe0lem 7797 1 ((𝐴 ∈ On ∧ 𝐵𝑋) → (𝐴𝑜 suc 𝐵) = ((𝐴𝑜 𝐵) ·𝑜 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1652  wcel 2155  Vcvv 3349  c0 4078  cmpt 4887  Ord word 5906  Oncon0 5907  Lim wlim 5908  suc csuc 5909  cfv 6067  (class class class)co 6841  reccrdg 7708  1𝑜c1o 7756   ·𝑜 comu 7761  𝑜 coe 7762
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 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146
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 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-ral 3059  df-rex 3060  df-reu 3061  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-pss 3747  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-tp 4338  df-op 4340  df-uni 4594  df-iun 4677  df-br 4809  df-opab 4871  df-mpt 4888  df-tr 4911  df-id 5184  df-eprel 5189  df-po 5197  df-so 5198  df-fr 5235  df-we 5237  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-pred 5864  df-ord 5910  df-on 5911  df-lim 5912  df-suc 5913  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-ov 6844  df-oprab 6845  df-mpt2 6846  df-om 7263  df-wrecs 7609  df-recs 7671  df-rdg 7709  df-1o 7763  df-omul 7768  df-oexp 7769
This theorem is referenced by:  oesuc  7811  onesuc  7814
  Copyright terms: Public domain W3C validator