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

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

Proof of Theorem oesuclem
StepHypRef Expression
1 oveq1 7229 . . . 4 (𝐴 = ∅ → (𝐴o suc 𝐵) = (∅ ↑o suc 𝐵))
2 oesuclem.1 . . . . . . . 8 Lim 𝑋
3 limord 6281 . . . . . . . 8 (Lim 𝑋 → Ord 𝑋)
42, 3ax-mp 5 . . . . . . 7 Ord 𝑋
5 ordelord 6244 . . . . . . 7 ((Ord 𝑋𝐵𝑋) → Ord 𝐵)
64, 5mpan 690 . . . . . 6 (𝐵𝑋 → Ord 𝐵)
7 0elsuc 7623 . . . . . 6 (Ord 𝐵 → ∅ ∈ suc 𝐵)
86, 7syl 17 . . . . 5 (𝐵𝑋 → ∅ ∈ suc 𝐵)
9 limsuc 7637 . . . . . . 7 (Lim 𝑋 → (𝐵𝑋 ↔ suc 𝐵𝑋))
102, 9ax-mp 5 . . . . . 6 (𝐵𝑋 ↔ suc 𝐵𝑋)
11 ordelon 6246 . . . . . . . 8 ((Ord 𝑋 ∧ suc 𝐵𝑋) → suc 𝐵 ∈ On)
124, 11mpan 690 . . . . . . 7 (suc 𝐵𝑋 → suc 𝐵 ∈ On)
13 oe0m1 8257 . . . . . . 7 (suc 𝐵 ∈ On → (∅ ∈ suc 𝐵 ↔ (∅ ↑o suc 𝐵) = ∅))
1412, 13syl 17 . . . . . 6 (suc 𝐵𝑋 → (∅ ∈ suc 𝐵 ↔ (∅ ↑o suc 𝐵) = ∅))
1510, 14sylbi 220 . . . . 5 (𝐵𝑋 → (∅ ∈ suc 𝐵 ↔ (∅ ↑o suc 𝐵) = ∅))
168, 15mpbid 235 . . . 4 (𝐵𝑋 → (∅ ↑o suc 𝐵) = ∅)
171, 16sylan9eqr 2801 . . 3 ((𝐵𝑋𝐴 = ∅) → (𝐴o suc 𝐵) = ∅)
18 oveq1 7229 . . . . 5 (𝐴 = ∅ → (𝐴o 𝐵) = (∅ ↑o 𝐵))
19 id 22 . . . . 5 (𝐴 = ∅ → 𝐴 = ∅)
2018, 19oveq12d 7240 . . . 4 (𝐴 = ∅ → ((𝐴o 𝐵) ·o 𝐴) = ((∅ ↑o 𝐵) ·o ∅))
21 ordelon 6246 . . . . . . 7 ((Ord 𝑋𝐵𝑋) → 𝐵 ∈ On)
224, 21mpan 690 . . . . . 6 (𝐵𝑋𝐵 ∈ On)
23 oveq2 7230 . . . . . . . . 9 (𝐵 = ∅ → (∅ ↑o 𝐵) = (∅ ↑o ∅))
24 oe0m0 8256 . . . . . . . . . 10 (∅ ↑o ∅) = 1o
25 1on 8218 . . . . . . . . . 10 1o ∈ On
2624, 25eqeltri 2835 . . . . . . . . 9 (∅ ↑o ∅) ∈ On
2723, 26eqeltrdi 2847 . . . . . . . 8 (𝐵 = ∅ → (∅ ↑o 𝐵) ∈ On)
2827adantl 485 . . . . . . 7 ((𝐵𝑋𝐵 = ∅) → (∅ ↑o 𝐵) ∈ On)
29 oe0m1 8257 . . . . . . . . . . 11 (𝐵 ∈ On → (∅ ∈ 𝐵 ↔ (∅ ↑o 𝐵) = ∅))
3022, 29syl 17 . . . . . . . . . 10 (𝐵𝑋 → (∅ ∈ 𝐵 ↔ (∅ ↑o 𝐵) = ∅))
3130biimpa 480 . . . . . . . . 9 ((𝐵𝑋 ∧ ∅ ∈ 𝐵) → (∅ ↑o 𝐵) = ∅)
32 0elon 6275 . . . . . . . . 9 ∅ ∈ On
3331, 32eqeltrdi 2847 . . . . . . . 8 ((𝐵𝑋 ∧ ∅ ∈ 𝐵) → (∅ ↑o 𝐵) ∈ On)
3433adantll 714 . . . . . . 7 (((𝐵 ∈ On ∧ 𝐵𝑋) ∧ ∅ ∈ 𝐵) → (∅ ↑o 𝐵) ∈ On)
3528, 34oe0lem 8249 . . . . . 6 ((𝐵 ∈ On ∧ 𝐵𝑋) → (∅ ↑o 𝐵) ∈ On)
3622, 35mpancom 688 . . . . 5 (𝐵𝑋 → (∅ ↑o 𝐵) ∈ On)
37 om0 8253 . . . . 5 ((∅ ↑o 𝐵) ∈ On → ((∅ ↑o 𝐵) ·o ∅) = ∅)
3836, 37syl 17 . . . 4 (𝐵𝑋 → ((∅ ↑o 𝐵) ·o ∅) = ∅)
3920, 38sylan9eqr 2801 . . 3 ((𝐵𝑋𝐴 = ∅) → ((𝐴o 𝐵) ·o 𝐴) = ∅)
4017, 39eqtr4d 2781 . 2 ((𝐵𝑋𝐴 = ∅) → (𝐴o suc 𝐵) = ((𝐴o 𝐵) ·o 𝐴))
41 oesuclem.2 . . . 4 (𝐵𝑋 → (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘suc 𝐵) = ((𝑥 ∈ V ↦ (𝑥 ·o 𝐴))‘(rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵)))
4241ad2antlr 727 . . 3 (((𝐴 ∈ On ∧ 𝐵𝑋) ∧ ∅ ∈ 𝐴) → (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘suc 𝐵) = ((𝑥 ∈ V ↦ (𝑥 ·o 𝐴))‘(rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵)))
4310, 12sylbi 220 . . . 4 (𝐵𝑋 → suc 𝐵 ∈ On)
44 oevn0 8251 . . . 4 (((𝐴 ∈ On ∧ suc 𝐵 ∈ On) ∧ ∅ ∈ 𝐴) → (𝐴o suc 𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘suc 𝐵))
4543, 44sylanl2 681 . . 3 (((𝐴 ∈ On ∧ 𝐵𝑋) ∧ ∅ ∈ 𝐴) → (𝐴o suc 𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘suc 𝐵))
46 ovex 7255 . . . . 5 (𝐴o 𝐵) ∈ V
47 oveq1 7229 . . . . . 6 (𝑥 = (𝐴o 𝐵) → (𝑥 ·o 𝐴) = ((𝐴o 𝐵) ·o 𝐴))
48 eqid 2738 . . . . . 6 (𝑥 ∈ V ↦ (𝑥 ·o 𝐴)) = (𝑥 ∈ V ↦ (𝑥 ·o 𝐴))
49 ovex 7255 . . . . . 6 ((𝐴o 𝐵) ·o 𝐴) ∈ V
5047, 48, 49fvmpt 6827 . . . . 5 ((𝐴o 𝐵) ∈ V → ((𝑥 ∈ V ↦ (𝑥 ·o 𝐴))‘(𝐴o 𝐵)) = ((𝐴o 𝐵) ·o 𝐴))
5146, 50ax-mp 5 . . . 4 ((𝑥 ∈ V ↦ (𝑥 ·o 𝐴))‘(𝐴o 𝐵)) = ((𝐴o 𝐵) ·o 𝐴)
52 oevn0 8251 . . . . . 6 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈ 𝐴) → (𝐴o 𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵))
5322, 52sylanl2 681 . . . . 5 (((𝐴 ∈ On ∧ 𝐵𝑋) ∧ ∅ ∈ 𝐴) → (𝐴o 𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵))
5453fveq2d 6730 . . . 4 (((𝐴 ∈ On ∧ 𝐵𝑋) ∧ ∅ ∈ 𝐴) → ((𝑥 ∈ V ↦ (𝑥 ·o 𝐴))‘(𝐴o 𝐵)) = ((𝑥 ∈ V ↦ (𝑥 ·o 𝐴))‘(rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵)))
5551, 54eqtr3id 2793 . . 3 (((𝐴 ∈ On ∧ 𝐵𝑋) ∧ ∅ ∈ 𝐴) → ((𝐴o 𝐵) ·o 𝐴) = ((𝑥 ∈ V ↦ (𝑥 ·o 𝐴))‘(rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵)))
5642, 45, 553eqtr4d 2788 . 2 (((𝐴 ∈ On ∧ 𝐵𝑋) ∧ ∅ ∈ 𝐴) → (𝐴o suc 𝐵) = ((𝐴o 𝐵) ·o 𝐴))
5740, 56oe0lem 8249 1 ((𝐴 ∈ On ∧ 𝐵𝑋) → (𝐴o suc 𝐵) = ((𝐴o 𝐵) ·o 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1543  wcel 2111  Vcvv 3415  c0 4246  cmpt 5144  Ord word 6221  Oncon0 6222  Lim wlim 6223  suc csuc 6224  cfv 6389  (class class class)co 7222  reccrdg 8154  1oc1o 8204   ·o comu 8209  o coe 8210
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-sep 5201  ax-nul 5208  ax-pr 5331  ax-un 7532
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-ral 3067  df-rex 3068  df-reu 3069  df-rab 3071  df-v 3417  df-sbc 3704  df-csb 3821  df-dif 3878  df-un 3880  df-in 3882  df-ss 3892  df-pss 3894  df-nul 4247  df-if 4449  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4829  df-iun 4915  df-br 5063  df-opab 5125  df-mpt 5145  df-tr 5171  df-id 5464  df-eprel 5469  df-po 5477  df-so 5478  df-fr 5518  df-we 5520  df-xp 5566  df-rel 5567  df-cnv 5568  df-co 5569  df-dm 5570  df-rn 5571  df-res 5572  df-ima 5573  df-pred 6169  df-ord 6225  df-on 6226  df-lim 6227  df-suc 6228  df-iota 6347  df-fun 6391  df-fn 6392  df-f 6393  df-f1 6394  df-fo 6395  df-f1o 6396  df-fv 6397  df-ov 7225  df-oprab 7226  df-mpo 7227  df-om 7654  df-wrecs 8056  df-recs 8117  df-rdg 8155  df-1o 8211  df-omul 8216  df-oexp 8217
This theorem is referenced by:  oesuc  8263  onesuc  8266
  Copyright terms: Public domain W3C validator