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

Theorem oeoelem 8218
 Description: Lemma for oeoe 8219. (Contributed by Eric Schmidt, 26-May-2009.)
Hypotheses
Ref Expression
oeoelem.1 𝐴 ∈ On
oeoelem.2 ∅ ∈ 𝐴
Assertion
Ref Expression
oeoelem ((𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴o 𝐵) ↑o 𝐶) = (𝐴o (𝐵 ·o 𝐶)))

Proof of Theorem oeoelem
Dummy variables 𝑥 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 7158 . . . 4 (𝑥 = ∅ → ((𝐴o 𝐵) ↑o 𝑥) = ((𝐴o 𝐵) ↑o ∅))
2 oveq2 7158 . . . . 5 (𝑥 = ∅ → (𝐵 ·o 𝑥) = (𝐵 ·o ∅))
32oveq2d 7166 . . . 4 (𝑥 = ∅ → (𝐴o (𝐵 ·o 𝑥)) = (𝐴o (𝐵 ·o ∅)))
41, 3eqeq12d 2837 . . 3 (𝑥 = ∅ → (((𝐴o 𝐵) ↑o 𝑥) = (𝐴o (𝐵 ·o 𝑥)) ↔ ((𝐴o 𝐵) ↑o ∅) = (𝐴o (𝐵 ·o ∅))))
5 oveq2 7158 . . . 4 (𝑥 = 𝑦 → ((𝐴o 𝐵) ↑o 𝑥) = ((𝐴o 𝐵) ↑o 𝑦))
6 oveq2 7158 . . . . 5 (𝑥 = 𝑦 → (𝐵 ·o 𝑥) = (𝐵 ·o 𝑦))
76oveq2d 7166 . . . 4 (𝑥 = 𝑦 → (𝐴o (𝐵 ·o 𝑥)) = (𝐴o (𝐵 ·o 𝑦)))
85, 7eqeq12d 2837 . . 3 (𝑥 = 𝑦 → (((𝐴o 𝐵) ↑o 𝑥) = (𝐴o (𝐵 ·o 𝑥)) ↔ ((𝐴o 𝐵) ↑o 𝑦) = (𝐴o (𝐵 ·o 𝑦))))
9 oveq2 7158 . . . 4 (𝑥 = suc 𝑦 → ((𝐴o 𝐵) ↑o 𝑥) = ((𝐴o 𝐵) ↑o suc 𝑦))
10 oveq2 7158 . . . . 5 (𝑥 = suc 𝑦 → (𝐵 ·o 𝑥) = (𝐵 ·o suc 𝑦))
1110oveq2d 7166 . . . 4 (𝑥 = suc 𝑦 → (𝐴o (𝐵 ·o 𝑥)) = (𝐴o (𝐵 ·o suc 𝑦)))
129, 11eqeq12d 2837 . . 3 (𝑥 = suc 𝑦 → (((𝐴o 𝐵) ↑o 𝑥) = (𝐴o (𝐵 ·o 𝑥)) ↔ ((𝐴o 𝐵) ↑o suc 𝑦) = (𝐴o (𝐵 ·o suc 𝑦))))
13 oveq2 7158 . . . 4 (𝑥 = 𝐶 → ((𝐴o 𝐵) ↑o 𝑥) = ((𝐴o 𝐵) ↑o 𝐶))
14 oveq2 7158 . . . . 5 (𝑥 = 𝐶 → (𝐵 ·o 𝑥) = (𝐵 ·o 𝐶))
1514oveq2d 7166 . . . 4 (𝑥 = 𝐶 → (𝐴o (𝐵 ·o 𝑥)) = (𝐴o (𝐵 ·o 𝐶)))
1613, 15eqeq12d 2837 . . 3 (𝑥 = 𝐶 → (((𝐴o 𝐵) ↑o 𝑥) = (𝐴o (𝐵 ·o 𝑥)) ↔ ((𝐴o 𝐵) ↑o 𝐶) = (𝐴o (𝐵 ·o 𝐶))))
17 oeoelem.1 . . . . . 6 𝐴 ∈ On
18 oecl 8156 . . . . . 6 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴o 𝐵) ∈ On)
1917, 18mpan 688 . . . . 5 (𝐵 ∈ On → (𝐴o 𝐵) ∈ On)
20 oe0 8141 . . . . 5 ((𝐴o 𝐵) ∈ On → ((𝐴o 𝐵) ↑o ∅) = 1o)
2119, 20syl 17 . . . 4 (𝐵 ∈ On → ((𝐴o 𝐵) ↑o ∅) = 1o)
22 om0 8136 . . . . . 6 (𝐵 ∈ On → (𝐵 ·o ∅) = ∅)
2322oveq2d 7166 . . . . 5 (𝐵 ∈ On → (𝐴o (𝐵 ·o ∅)) = (𝐴o ∅))
24 oe0 8141 . . . . . 6 (𝐴 ∈ On → (𝐴o ∅) = 1o)
2517, 24ax-mp 5 . . . . 5 (𝐴o ∅) = 1o
2623, 25syl6eq 2872 . . . 4 (𝐵 ∈ On → (𝐴o (𝐵 ·o ∅)) = 1o)
2721, 26eqtr4d 2859 . . 3 (𝐵 ∈ On → ((𝐴o 𝐵) ↑o ∅) = (𝐴o (𝐵 ·o ∅)))
28 oveq1 7157 . . . . 5 (((𝐴o 𝐵) ↑o 𝑦) = (𝐴o (𝐵 ·o 𝑦)) → (((𝐴o 𝐵) ↑o 𝑦) ·o (𝐴o 𝐵)) = ((𝐴o (𝐵 ·o 𝑦)) ·o (𝐴o 𝐵)))
29 oesuc 8146 . . . . . . 7 (((𝐴o 𝐵) ∈ On ∧ 𝑦 ∈ On) → ((𝐴o 𝐵) ↑o suc 𝑦) = (((𝐴o 𝐵) ↑o 𝑦) ·o (𝐴o 𝐵)))
3019, 29sylan 582 . . . . . 6 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → ((𝐴o 𝐵) ↑o suc 𝑦) = (((𝐴o 𝐵) ↑o 𝑦) ·o (𝐴o 𝐵)))
31 omsuc 8145 . . . . . . . 8 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ·o suc 𝑦) = ((𝐵 ·o 𝑦) +o 𝐵))
3231oveq2d 7166 . . . . . . 7 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴o (𝐵 ·o suc 𝑦)) = (𝐴o ((𝐵 ·o 𝑦) +o 𝐵)))
33 omcl 8155 . . . . . . . . 9 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ·o 𝑦) ∈ On)
34 oeoa 8217 . . . . . . . . . 10 ((𝐴 ∈ On ∧ (𝐵 ·o 𝑦) ∈ On ∧ 𝐵 ∈ On) → (𝐴o ((𝐵 ·o 𝑦) +o 𝐵)) = ((𝐴o (𝐵 ·o 𝑦)) ·o (𝐴o 𝐵)))
3517, 34mp3an1 1444 . . . . . . . . 9 (((𝐵 ·o 𝑦) ∈ On ∧ 𝐵 ∈ On) → (𝐴o ((𝐵 ·o 𝑦) +o 𝐵)) = ((𝐴o (𝐵 ·o 𝑦)) ·o (𝐴o 𝐵)))
3633, 35sylan 582 . . . . . . . 8 (((𝐵 ∈ On ∧ 𝑦 ∈ On) ∧ 𝐵 ∈ On) → (𝐴o ((𝐵 ·o 𝑦) +o 𝐵)) = ((𝐴o (𝐵 ·o 𝑦)) ·o (𝐴o 𝐵)))
3736anabss1 664 . . . . . . 7 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴o ((𝐵 ·o 𝑦) +o 𝐵)) = ((𝐴o (𝐵 ·o 𝑦)) ·o (𝐴o 𝐵)))
3832, 37eqtrd 2856 . . . . . 6 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴o (𝐵 ·o suc 𝑦)) = ((𝐴o (𝐵 ·o 𝑦)) ·o (𝐴o 𝐵)))
3930, 38eqeq12d 2837 . . . . 5 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (((𝐴o 𝐵) ↑o suc 𝑦) = (𝐴o (𝐵 ·o suc 𝑦)) ↔ (((𝐴o 𝐵) ↑o 𝑦) ·o (𝐴o 𝐵)) = ((𝐴o (𝐵 ·o 𝑦)) ·o (𝐴o 𝐵))))
4028, 39syl5ibr 248 . . . 4 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (((𝐴o 𝐵) ↑o 𝑦) = (𝐴o (𝐵 ·o 𝑦)) → ((𝐴o 𝐵) ↑o suc 𝑦) = (𝐴o (𝐵 ·o suc 𝑦))))
4140expcom 416 . . 3 (𝑦 ∈ On → (𝐵 ∈ On → (((𝐴o 𝐵) ↑o 𝑦) = (𝐴o (𝐵 ·o 𝑦)) → ((𝐴o 𝐵) ↑o suc 𝑦) = (𝐴o (𝐵 ·o suc 𝑦)))))
42 iuneq2 4931 . . . . 5 (∀𝑦𝑥 ((𝐴o 𝐵) ↑o 𝑦) = (𝐴o (𝐵 ·o 𝑦)) → 𝑦𝑥 ((𝐴o 𝐵) ↑o 𝑦) = 𝑦𝑥 (𝐴o (𝐵 ·o 𝑦)))
43 vex 3498 . . . . . . 7 𝑥 ∈ V
44 oeoelem.2 . . . . . . . . . 10 ∅ ∈ 𝐴
45 oen0 8206 . . . . . . . . . 10 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴o 𝐵))
4644, 45mpan2 689 . . . . . . . . 9 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ∅ ∈ (𝐴o 𝐵))
47 oelim 8153 . . . . . . . . . 10 ((((𝐴o 𝐵) ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ ∅ ∈ (𝐴o 𝐵)) → ((𝐴o 𝐵) ↑o 𝑥) = 𝑦𝑥 ((𝐴o 𝐵) ↑o 𝑦))
4818, 47sylanl1 678 . . . . . . . . 9 ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ ∅ ∈ (𝐴o 𝐵)) → ((𝐴o 𝐵) ↑o 𝑥) = 𝑦𝑥 ((𝐴o 𝐵) ↑o 𝑦))
4946, 48mpidan 687 . . . . . . . 8 (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → ((𝐴o 𝐵) ↑o 𝑥) = 𝑦𝑥 ((𝐴o 𝐵) ↑o 𝑦))
5017, 49mpanl1 698 . . . . . . 7 ((𝐵 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → ((𝐴o 𝐵) ↑o 𝑥) = 𝑦𝑥 ((𝐴o 𝐵) ↑o 𝑦))
5143, 50mpanr1 701 . . . . . 6 ((𝐵 ∈ On ∧ Lim 𝑥) → ((𝐴o 𝐵) ↑o 𝑥) = 𝑦𝑥 ((𝐴o 𝐵) ↑o 𝑦))
52 omlim 8152 . . . . . . . . 9 ((𝐵 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → (𝐵 ·o 𝑥) = 𝑦𝑥 (𝐵 ·o 𝑦))
5343, 52mpanr1 701 . . . . . . . 8 ((𝐵 ∈ On ∧ Lim 𝑥) → (𝐵 ·o 𝑥) = 𝑦𝑥 (𝐵 ·o 𝑦))
5453oveq2d 7166 . . . . . . 7 ((𝐵 ∈ On ∧ Lim 𝑥) → (𝐴o (𝐵 ·o 𝑥)) = (𝐴o 𝑦𝑥 (𝐵 ·o 𝑦)))
55 limord 6245 . . . . . . . . . . . 12 (Lim 𝑥 → Ord 𝑥)
56 ordelon 6210 . . . . . . . . . . . 12 ((Ord 𝑥𝑦𝑥) → 𝑦 ∈ On)
5755, 56sylan 582 . . . . . . . . . . 11 ((Lim 𝑥𝑦𝑥) → 𝑦 ∈ On)
5857, 33sylan2 594 . . . . . . . . . 10 ((𝐵 ∈ On ∧ (Lim 𝑥𝑦𝑥)) → (𝐵 ·o 𝑦) ∈ On)
5958anassrs 470 . . . . . . . . 9 (((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝑦𝑥) → (𝐵 ·o 𝑦) ∈ On)
6059ralrimiva 3182 . . . . . . . 8 ((𝐵 ∈ On ∧ Lim 𝑥) → ∀𝑦𝑥 (𝐵 ·o 𝑦) ∈ On)
61 0ellim 6248 . . . . . . . . . 10 (Lim 𝑥 → ∅ ∈ 𝑥)
6261ne0d 4301 . . . . . . . . 9 (Lim 𝑥𝑥 ≠ ∅)
6362adantl 484 . . . . . . . 8 ((𝐵 ∈ On ∧ Lim 𝑥) → 𝑥 ≠ ∅)
64 vex 3498 . . . . . . . . . 10 𝑤 ∈ V
65 oelim 8153 . . . . . . . . . . . 12 (((𝐴 ∈ On ∧ (𝑤 ∈ V ∧ Lim 𝑤)) ∧ ∅ ∈ 𝐴) → (𝐴o 𝑤) = 𝑧𝑤 (𝐴o 𝑧))
6644, 65mpan2 689 . . . . . . . . . . 11 ((𝐴 ∈ On ∧ (𝑤 ∈ V ∧ Lim 𝑤)) → (𝐴o 𝑤) = 𝑧𝑤 (𝐴o 𝑧))
6717, 66mpan 688 . . . . . . . . . 10 ((𝑤 ∈ V ∧ Lim 𝑤) → (𝐴o 𝑤) = 𝑧𝑤 (𝐴o 𝑧))
6864, 67mpan 688 . . . . . . . . 9 (Lim 𝑤 → (𝐴o 𝑤) = 𝑧𝑤 (𝐴o 𝑧))
69 oewordi 8211 . . . . . . . . . . . 12 (((𝑧 ∈ On ∧ 𝑤 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (𝑧𝑤 → (𝐴o 𝑧) ⊆ (𝐴o 𝑤)))
7044, 69mpan2 689 . . . . . . . . . . 11 ((𝑧 ∈ On ∧ 𝑤 ∈ On ∧ 𝐴 ∈ On) → (𝑧𝑤 → (𝐴o 𝑧) ⊆ (𝐴o 𝑤)))
7117, 70mp3an3 1446 . . . . . . . . . 10 ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧𝑤 → (𝐴o 𝑧) ⊆ (𝐴o 𝑤)))
72713impia 1113 . . . . . . . . 9 ((𝑧 ∈ On ∧ 𝑤 ∈ On ∧ 𝑧𝑤) → (𝐴o 𝑧) ⊆ (𝐴o 𝑤))
7368, 72onoviun 7974 . . . . . . . 8 ((𝑥 ∈ V ∧ ∀𝑦𝑥 (𝐵 ·o 𝑦) ∈ On ∧ 𝑥 ≠ ∅) → (𝐴o 𝑦𝑥 (𝐵 ·o 𝑦)) = 𝑦𝑥 (𝐴o (𝐵 ·o 𝑦)))
7443, 60, 63, 73mp3an2i 1462 . . . . . . 7 ((𝐵 ∈ On ∧ Lim 𝑥) → (𝐴o 𝑦𝑥 (𝐵 ·o 𝑦)) = 𝑦𝑥 (𝐴o (𝐵 ·o 𝑦)))
7554, 74eqtrd 2856 . . . . . 6 ((𝐵 ∈ On ∧ Lim 𝑥) → (𝐴o (𝐵 ·o 𝑥)) = 𝑦𝑥 (𝐴o (𝐵 ·o 𝑦)))
7651, 75eqeq12d 2837 . . . . 5 ((𝐵 ∈ On ∧ Lim 𝑥) → (((𝐴o 𝐵) ↑o 𝑥) = (𝐴o (𝐵 ·o 𝑥)) ↔ 𝑦𝑥 ((𝐴o 𝐵) ↑o 𝑦) = 𝑦𝑥 (𝐴o (𝐵 ·o 𝑦))))
7742, 76syl5ibr 248 . . . 4 ((𝐵 ∈ On ∧ Lim 𝑥) → (∀𝑦𝑥 ((𝐴o 𝐵) ↑o 𝑦) = (𝐴o (𝐵 ·o 𝑦)) → ((𝐴o 𝐵) ↑o 𝑥) = (𝐴o (𝐵 ·o 𝑥))))
7877expcom 416 . . 3 (Lim 𝑥 → (𝐵 ∈ On → (∀𝑦𝑥 ((𝐴o 𝐵) ↑o 𝑦) = (𝐴o (𝐵 ·o 𝑦)) → ((𝐴o 𝐵) ↑o 𝑥) = (𝐴o (𝐵 ·o 𝑥)))))
794, 8, 12, 16, 27, 41, 78tfinds3 7573 . 2 (𝐶 ∈ On → (𝐵 ∈ On → ((𝐴o 𝐵) ↑o 𝐶) = (𝐴o (𝐵 ·o 𝐶))))
8079impcom 410 1 ((𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴o 𝐵) ↑o 𝐶) = (𝐴o (𝐵 ·o 𝐶)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083   = wceq 1533   ∈ wcel 2110   ≠ wne 3016  ∀wral 3138  Vcvv 3495   ⊆ wss 3936  ∅c0 4291  ∪ ciun 4912  Ord word 6185  Oncon0 6186  Lim wlim 6187  suc csuc 6188  (class class class)co 7150  1oc1o 8089   +o coa 8093   ·o comu 8094   ↑o coe 8095 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-rep 5183  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5322  ax-un 7455 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3497  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4833  df-int 4870  df-iun 4914  df-br 5060  df-opab 5122  df-mpt 5140  df-tr 5166  df-id 5455  df-eprel 5460  df-po 5469  df-so 5470  df-fr 5509  df-we 5511  df-xp 5556  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-res 5562  df-ima 5563  df-pred 6143  df-ord 6189  df-on 6190  df-lim 6191  df-suc 6192  df-iota 6309  df-fun 6352  df-fn 6353  df-f 6354  df-f1 6355  df-fo 6356  df-f1o 6357  df-fv 6358  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7575  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-2o 8097  df-oadd 8100  df-omul 8101  df-oexp 8102 This theorem is referenced by:  oeoe  8219
 Copyright terms: Public domain W3C validator