Step | Hyp | Ref
| Expression |
1 | | oveq2 6557 |
. . . 4
⊢ (𝑥 = ∅ → ((𝐴 ↑𝑜
𝐵)
↑𝑜 𝑥) = ((𝐴 ↑𝑜 𝐵) ↑𝑜
∅)) |
2 | | oveq2 6557 |
. . . . 5
⊢ (𝑥 = ∅ → (𝐵 ·𝑜
𝑥) = (𝐵 ·𝑜
∅)) |
3 | 2 | oveq2d 6565 |
. . . 4
⊢ (𝑥 = ∅ → (𝐴 ↑𝑜
(𝐵
·𝑜 𝑥)) = (𝐴 ↑𝑜 (𝐵 ·𝑜
∅))) |
4 | 1, 3 | eqeq12d 2625 |
. . 3
⊢ (𝑥 = ∅ → (((𝐴 ↑𝑜
𝐵)
↑𝑜 𝑥) = (𝐴 ↑𝑜 (𝐵 ·𝑜
𝑥)) ↔ ((𝐴 ↑𝑜
𝐵)
↑𝑜 ∅) = (𝐴 ↑𝑜 (𝐵 ·𝑜
∅)))) |
5 | | oveq2 6557 |
. . . 4
⊢ (𝑥 = 𝑦 → ((𝐴 ↑𝑜 𝐵) ↑𝑜
𝑥) = ((𝐴 ↑𝑜 𝐵) ↑𝑜
𝑦)) |
6 | | oveq2 6557 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝐵 ·𝑜 𝑥) = (𝐵 ·𝑜 𝑦)) |
7 | 6 | oveq2d 6565 |
. . . 4
⊢ (𝑥 = 𝑦 → (𝐴 ↑𝑜 (𝐵 ·𝑜
𝑥)) = (𝐴 ↑𝑜 (𝐵 ·𝑜
𝑦))) |
8 | 5, 7 | eqeq12d 2625 |
. . 3
⊢ (𝑥 = 𝑦 → (((𝐴 ↑𝑜 𝐵) ↑𝑜
𝑥) = (𝐴 ↑𝑜 (𝐵 ·𝑜
𝑥)) ↔ ((𝐴 ↑𝑜
𝐵)
↑𝑜 𝑦) = (𝐴 ↑𝑜 (𝐵 ·𝑜
𝑦)))) |
9 | | oveq2 6557 |
. . . 4
⊢ (𝑥 = suc 𝑦 → ((𝐴 ↑𝑜 𝐵) ↑𝑜
𝑥) = ((𝐴 ↑𝑜 𝐵) ↑𝑜 suc
𝑦)) |
10 | | oveq2 6557 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → (𝐵 ·𝑜 𝑥) = (𝐵 ·𝑜 suc 𝑦)) |
11 | 10 | oveq2d 6565 |
. . . 4
⊢ (𝑥 = suc 𝑦 → (𝐴 ↑𝑜 (𝐵 ·𝑜
𝑥)) = (𝐴 ↑𝑜 (𝐵 ·𝑜
suc 𝑦))) |
12 | 9, 11 | eqeq12d 2625 |
. . 3
⊢ (𝑥 = suc 𝑦 → (((𝐴 ↑𝑜 𝐵) ↑𝑜
𝑥) = (𝐴 ↑𝑜 (𝐵 ·𝑜
𝑥)) ↔ ((𝐴 ↑𝑜
𝐵)
↑𝑜 suc 𝑦) = (𝐴 ↑𝑜 (𝐵 ·𝑜
suc 𝑦)))) |
13 | | oveq2 6557 |
. . . 4
⊢ (𝑥 = 𝐶 → ((𝐴 ↑𝑜 𝐵) ↑𝑜
𝑥) = ((𝐴 ↑𝑜 𝐵) ↑𝑜
𝐶)) |
14 | | oveq2 6557 |
. . . . 5
⊢ (𝑥 = 𝐶 → (𝐵 ·𝑜 𝑥) = (𝐵 ·𝑜 𝐶)) |
15 | 14 | oveq2d 6565 |
. . . 4
⊢ (𝑥 = 𝐶 → (𝐴 ↑𝑜 (𝐵 ·𝑜
𝑥)) = (𝐴 ↑𝑜 (𝐵 ·𝑜
𝐶))) |
16 | 13, 15 | eqeq12d 2625 |
. . 3
⊢ (𝑥 = 𝐶 → (((𝐴 ↑𝑜 𝐵) ↑𝑜
𝑥) = (𝐴 ↑𝑜 (𝐵 ·𝑜
𝑥)) ↔ ((𝐴 ↑𝑜
𝐵)
↑𝑜 𝐶) = (𝐴 ↑𝑜 (𝐵 ·𝑜
𝐶)))) |
17 | | oeoelem.1 |
. . . . . 6
⊢ 𝐴 ∈ On |
18 | | oecl 7504 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑𝑜
𝐵) ∈
On) |
19 | 17, 18 | mpan 702 |
. . . . 5
⊢ (𝐵 ∈ On → (𝐴 ↑𝑜
𝐵) ∈
On) |
20 | | oe0 7489 |
. . . . 5
⊢ ((𝐴 ↑𝑜
𝐵) ∈ On → ((𝐴 ↑𝑜
𝐵)
↑𝑜 ∅) = 1𝑜) |
21 | 19, 20 | syl 17 |
. . . 4
⊢ (𝐵 ∈ On → ((𝐴 ↑𝑜
𝐵)
↑𝑜 ∅) = 1𝑜) |
22 | | om0 7484 |
. . . . . 6
⊢ (𝐵 ∈ On → (𝐵 ·𝑜
∅) = ∅) |
23 | 22 | oveq2d 6565 |
. . . . 5
⊢ (𝐵 ∈ On → (𝐴 ↑𝑜
(𝐵
·𝑜 ∅)) = (𝐴 ↑𝑜
∅)) |
24 | | oe0 7489 |
. . . . . 6
⊢ (𝐴 ∈ On → (𝐴 ↑𝑜
∅) = 1𝑜) |
25 | 17, 24 | ax-mp 5 |
. . . . 5
⊢ (𝐴 ↑𝑜
∅) = 1𝑜 |
26 | 23, 25 | syl6eq 2660 |
. . . 4
⊢ (𝐵 ∈ On → (𝐴 ↑𝑜
(𝐵
·𝑜 ∅)) =
1𝑜) |
27 | 21, 26 | eqtr4d 2647 |
. . 3
⊢ (𝐵 ∈ On → ((𝐴 ↑𝑜
𝐵)
↑𝑜 ∅) = (𝐴 ↑𝑜 (𝐵 ·𝑜
∅))) |
28 | | oveq1 6556 |
. . . . 5
⊢ (((𝐴 ↑𝑜
𝐵)
↑𝑜 𝑦) = (𝐴 ↑𝑜 (𝐵 ·𝑜
𝑦)) → (((𝐴 ↑𝑜
𝐵)
↑𝑜 𝑦) ·𝑜 (𝐴 ↑𝑜
𝐵)) = ((𝐴 ↑𝑜 (𝐵 ·𝑜
𝑦))
·𝑜 (𝐴 ↑𝑜 𝐵))) |
29 | | oesuc 7494 |
. . . . . . 7
⊢ (((𝐴 ↑𝑜
𝐵) ∈ On ∧ 𝑦 ∈ On) → ((𝐴 ↑𝑜
𝐵)
↑𝑜 suc 𝑦) = (((𝐴 ↑𝑜 𝐵) ↑𝑜
𝑦)
·𝑜 (𝐴 ↑𝑜 𝐵))) |
30 | 19, 29 | sylan 487 |
. . . . . 6
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → ((𝐴 ↑𝑜
𝐵)
↑𝑜 suc 𝑦) = (((𝐴 ↑𝑜 𝐵) ↑𝑜
𝑦)
·𝑜 (𝐴 ↑𝑜 𝐵))) |
31 | | omsuc 7493 |
. . . . . . . 8
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ·𝑜
suc 𝑦) = ((𝐵 ·𝑜
𝑦) +𝑜
𝐵)) |
32 | 31 | oveq2d 6565 |
. . . . . . 7
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ↑𝑜
(𝐵
·𝑜 suc 𝑦)) = (𝐴 ↑𝑜 ((𝐵 ·𝑜
𝑦) +𝑜
𝐵))) |
33 | | omcl 7503 |
. . . . . . . . 9
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ·𝑜
𝑦) ∈
On) |
34 | | oeoa 7564 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ (𝐵 ·𝑜
𝑦) ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑𝑜
((𝐵
·𝑜 𝑦) +𝑜 𝐵)) = ((𝐴 ↑𝑜 (𝐵 ·𝑜
𝑦))
·𝑜 (𝐴 ↑𝑜 𝐵))) |
35 | 17, 34 | mp3an1 1403 |
. . . . . . . . 9
⊢ (((𝐵 ·𝑜
𝑦) ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑𝑜
((𝐵
·𝑜 𝑦) +𝑜 𝐵)) = ((𝐴 ↑𝑜 (𝐵 ·𝑜
𝑦))
·𝑜 (𝐴 ↑𝑜 𝐵))) |
36 | 33, 35 | sylan 487 |
. . . . . . . 8
⊢ (((𝐵 ∈ On ∧ 𝑦 ∈ On) ∧ 𝐵 ∈ On) → (𝐴 ↑𝑜
((𝐵
·𝑜 𝑦) +𝑜 𝐵)) = ((𝐴 ↑𝑜 (𝐵 ·𝑜
𝑦))
·𝑜 (𝐴 ↑𝑜 𝐵))) |
37 | 36 | anabss1 851 |
. . . . . . 7
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ↑𝑜
((𝐵
·𝑜 𝑦) +𝑜 𝐵)) = ((𝐴 ↑𝑜 (𝐵 ·𝑜
𝑦))
·𝑜 (𝐴 ↑𝑜 𝐵))) |
38 | 32, 37 | eqtrd 2644 |
. . . . . 6
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ↑𝑜
(𝐵
·𝑜 suc 𝑦)) = ((𝐴 ↑𝑜 (𝐵 ·𝑜
𝑦))
·𝑜 (𝐴 ↑𝑜 𝐵))) |
39 | 30, 38 | eqeq12d 2625 |
. . . . 5
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (((𝐴 ↑𝑜
𝐵)
↑𝑜 suc 𝑦) = (𝐴 ↑𝑜 (𝐵 ·𝑜
suc 𝑦)) ↔ (((𝐴 ↑𝑜
𝐵)
↑𝑜 𝑦) ·𝑜 (𝐴 ↑𝑜
𝐵)) = ((𝐴 ↑𝑜 (𝐵 ·𝑜
𝑦))
·𝑜 (𝐴 ↑𝑜 𝐵)))) |
40 | 28, 39 | syl5ibr 235 |
. . . 4
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (((𝐴 ↑𝑜
𝐵)
↑𝑜 𝑦) = (𝐴 ↑𝑜 (𝐵 ·𝑜
𝑦)) → ((𝐴 ↑𝑜
𝐵)
↑𝑜 suc 𝑦) = (𝐴 ↑𝑜 (𝐵 ·𝑜
suc 𝑦)))) |
41 | 40 | expcom 450 |
. . 3
⊢ (𝑦 ∈ On → (𝐵 ∈ On → (((𝐴 ↑𝑜
𝐵)
↑𝑜 𝑦) = (𝐴 ↑𝑜 (𝐵 ·𝑜
𝑦)) → ((𝐴 ↑𝑜
𝐵)
↑𝑜 suc 𝑦) = (𝐴 ↑𝑜 (𝐵 ·𝑜
suc 𝑦))))) |
42 | | iuneq2 4473 |
. . . . 5
⊢
(∀𝑦 ∈
𝑥 ((𝐴 ↑𝑜 𝐵) ↑𝑜
𝑦) = (𝐴 ↑𝑜 (𝐵 ·𝑜
𝑦)) → ∪ 𝑦 ∈ 𝑥 ((𝐴 ↑𝑜 𝐵) ↑𝑜
𝑦) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑𝑜 (𝐵 ·𝑜
𝑦))) |
43 | | vex 3176 |
. . . . . . 7
⊢ 𝑥 ∈ V |
44 | | oeoelem.2 |
. . . . . . . . . . 11
⊢ ∅
∈ 𝐴 |
45 | | oen0 7553 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈
𝐴) → ∅ ∈
(𝐴
↑𝑜 𝐵)) |
46 | 44, 45 | mpan2 703 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ∅
∈ (𝐴
↑𝑜 𝐵)) |
47 | | oelim 7501 |
. . . . . . . . . . 11
⊢ ((((𝐴 ↑𝑜
𝐵) ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ ∅ ∈ (𝐴 ↑𝑜
𝐵)) → ((𝐴 ↑𝑜
𝐵)
↑𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 ((𝐴 ↑𝑜 𝐵) ↑𝑜
𝑦)) |
48 | 18, 47 | sylanl1 680 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ ∅ ∈ (𝐴 ↑𝑜
𝐵)) → ((𝐴 ↑𝑜
𝐵)
↑𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 ((𝐴 ↑𝑜 𝐵) ↑𝑜
𝑦)) |
49 | 46, 48 | sylan2 490 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → ((𝐴 ↑𝑜 𝐵) ↑𝑜
𝑥) = ∪ 𝑦 ∈ 𝑥 ((𝐴 ↑𝑜 𝐵) ↑𝑜
𝑦)) |
50 | 49 | anabss1 851 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → ((𝐴 ↑𝑜 𝐵) ↑𝑜
𝑥) = ∪ 𝑦 ∈ 𝑥 ((𝐴 ↑𝑜 𝐵) ↑𝑜
𝑦)) |
51 | 17, 50 | mpanl1 712 |
. . . . . . 7
⊢ ((𝐵 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → ((𝐴 ↑𝑜 𝐵) ↑𝑜
𝑥) = ∪ 𝑦 ∈ 𝑥 ((𝐴 ↑𝑜 𝐵) ↑𝑜
𝑦)) |
52 | 43, 51 | mpanr1 715 |
. . . . . 6
⊢ ((𝐵 ∈ On ∧ Lim 𝑥) → ((𝐴 ↑𝑜 𝐵) ↑𝑜
𝑥) = ∪ 𝑦 ∈ 𝑥 ((𝐴 ↑𝑜 𝐵) ↑𝑜
𝑦)) |
53 | | omlim 7500 |
. . . . . . . . 9
⊢ ((𝐵 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → (𝐵 ·𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐵 ·𝑜 𝑦)) |
54 | 43, 53 | mpanr1 715 |
. . . . . . . 8
⊢ ((𝐵 ∈ On ∧ Lim 𝑥) → (𝐵 ·𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐵 ·𝑜 𝑦)) |
55 | 54 | oveq2d 6565 |
. . . . . . 7
⊢ ((𝐵 ∈ On ∧ Lim 𝑥) → (𝐴 ↑𝑜 (𝐵 ·𝑜
𝑥)) = (𝐴 ↑𝑜 ∪ 𝑦 ∈ 𝑥 (𝐵 ·𝑜 𝑦))) |
56 | 43 | a1i 11 |
. . . . . . . 8
⊢ ((𝐵 ∈ On ∧ Lim 𝑥) → 𝑥 ∈ V) |
57 | | limord 5701 |
. . . . . . . . . . . 12
⊢ (Lim
𝑥 → Ord 𝑥) |
58 | | ordelon 5664 |
. . . . . . . . . . . 12
⊢ ((Ord
𝑥 ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On) |
59 | 57, 58 | sylan 487 |
. . . . . . . . . . 11
⊢ ((Lim
𝑥 ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On) |
60 | 59, 33 | sylan2 490 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ On ∧ (Lim 𝑥 ∧ 𝑦 ∈ 𝑥)) → (𝐵 ·𝑜 𝑦) ∈ On) |
61 | 60 | anassrs 678 |
. . . . . . . . 9
⊢ (((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝑦 ∈ 𝑥) → (𝐵 ·𝑜 𝑦) ∈ On) |
62 | 61 | ralrimiva 2949 |
. . . . . . . 8
⊢ ((𝐵 ∈ On ∧ Lim 𝑥) → ∀𝑦 ∈ 𝑥 (𝐵 ·𝑜 𝑦) ∈ On) |
63 | | 0ellim 5704 |
. . . . . . . . . 10
⊢ (Lim
𝑥 → ∅ ∈
𝑥) |
64 | | ne0i 3880 |
. . . . . . . . . 10
⊢ (∅
∈ 𝑥 → 𝑥 ≠ ∅) |
65 | 63, 64 | syl 17 |
. . . . . . . . 9
⊢ (Lim
𝑥 → 𝑥 ≠ ∅) |
66 | 65 | adantl 481 |
. . . . . . . 8
⊢ ((𝐵 ∈ On ∧ Lim 𝑥) → 𝑥 ≠ ∅) |
67 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑤 ∈ V |
68 | | oelim 7501 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ On ∧ (𝑤 ∈ V ∧ Lim 𝑤)) ∧ ∅ ∈ 𝐴) → (𝐴 ↑𝑜 𝑤) = ∪ 𝑧 ∈ 𝑤 (𝐴 ↑𝑜 𝑧)) |
69 | 44, 68 | mpan2 703 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ (𝑤 ∈ V ∧ Lim 𝑤)) → (𝐴 ↑𝑜 𝑤) = ∪ 𝑧 ∈ 𝑤 (𝐴 ↑𝑜 𝑧)) |
70 | 17, 69 | mpan 702 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ V ∧ Lim 𝑤) → (𝐴 ↑𝑜 𝑤) = ∪ 𝑧 ∈ 𝑤 (𝐴 ↑𝑜 𝑧)) |
71 | 67, 70 | mpan 702 |
. . . . . . . . 9
⊢ (Lim
𝑤 → (𝐴 ↑𝑜 𝑤) = ∪ 𝑧 ∈ 𝑤 (𝐴 ↑𝑜 𝑧)) |
72 | | oewordi 7558 |
. . . . . . . . . . . 12
⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈
𝐴) → (𝑧 ⊆ 𝑤 → (𝐴 ↑𝑜 𝑧) ⊆ (𝐴 ↑𝑜 𝑤))) |
73 | 44, 72 | mpan2 703 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On ∧ 𝐴 ∈ On) → (𝑧 ⊆ 𝑤 → (𝐴 ↑𝑜 𝑧) ⊆ (𝐴 ↑𝑜 𝑤))) |
74 | 17, 73 | mp3an3 1405 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧 ⊆ 𝑤 → (𝐴 ↑𝑜 𝑧) ⊆ (𝐴 ↑𝑜 𝑤))) |
75 | 74 | 3impia 1253 |
. . . . . . . . 9
⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On ∧ 𝑧 ⊆ 𝑤) → (𝐴 ↑𝑜 𝑧) ⊆ (𝐴 ↑𝑜 𝑤)) |
76 | 71, 75 | onoviun 7327 |
. . . . . . . 8
⊢ ((𝑥 ∈ V ∧ ∀𝑦 ∈ 𝑥 (𝐵 ·𝑜 𝑦) ∈ On ∧ 𝑥 ≠ ∅) → (𝐴 ↑𝑜
∪ 𝑦 ∈ 𝑥 (𝐵 ·𝑜 𝑦)) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑𝑜 (𝐵 ·𝑜
𝑦))) |
77 | 56, 62, 66, 76 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝐵 ∈ On ∧ Lim 𝑥) → (𝐴 ↑𝑜 ∪ 𝑦 ∈ 𝑥 (𝐵 ·𝑜 𝑦)) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑𝑜 (𝐵 ·𝑜
𝑦))) |
78 | 55, 77 | eqtrd 2644 |
. . . . . 6
⊢ ((𝐵 ∈ On ∧ Lim 𝑥) → (𝐴 ↑𝑜 (𝐵 ·𝑜
𝑥)) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑𝑜 (𝐵 ·𝑜
𝑦))) |
79 | 52, 78 | eqeq12d 2625 |
. . . . 5
⊢ ((𝐵 ∈ On ∧ Lim 𝑥) → (((𝐴 ↑𝑜 𝐵) ↑𝑜
𝑥) = (𝐴 ↑𝑜 (𝐵 ·𝑜
𝑥)) ↔ ∪ 𝑦 ∈ 𝑥 ((𝐴 ↑𝑜 𝐵) ↑𝑜
𝑦) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑𝑜 (𝐵 ·𝑜
𝑦)))) |
80 | 42, 79 | syl5ibr 235 |
. . . 4
⊢ ((𝐵 ∈ On ∧ Lim 𝑥) → (∀𝑦 ∈ 𝑥 ((𝐴 ↑𝑜 𝐵) ↑𝑜
𝑦) = (𝐴 ↑𝑜 (𝐵 ·𝑜
𝑦)) → ((𝐴 ↑𝑜
𝐵)
↑𝑜 𝑥) = (𝐴 ↑𝑜 (𝐵 ·𝑜
𝑥)))) |
81 | 80 | expcom 450 |
. . 3
⊢ (Lim
𝑥 → (𝐵 ∈ On → (∀𝑦 ∈ 𝑥 ((𝐴 ↑𝑜 𝐵) ↑𝑜
𝑦) = (𝐴 ↑𝑜 (𝐵 ·𝑜
𝑦)) → ((𝐴 ↑𝑜
𝐵)
↑𝑜 𝑥) = (𝐴 ↑𝑜 (𝐵 ·𝑜
𝑥))))) |
82 | 4, 8, 12, 16, 27, 41, 81 | tfinds3 6956 |
. 2
⊢ (𝐶 ∈ On → (𝐵 ∈ On → ((𝐴 ↑𝑜
𝐵)
↑𝑜 𝐶) = (𝐴 ↑𝑜 (𝐵 ·𝑜
𝐶)))) |
83 | 82 | impcom 445 |
1
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ↑𝑜
𝐵)
↑𝑜 𝐶) = (𝐴 ↑𝑜 (𝐵 ·𝑜
𝐶))) |