Step | Hyp | Ref
| Expression |
1 | | oveq2 6658 |
. . . . . 6
⊢ (𝑥 = ∅ → ((𝐴 ·𝑜
𝐵)
·𝑜 𝑥) = ((𝐴 ·𝑜 𝐵) ·𝑜
∅)) |
2 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑥 = ∅ → (𝐵 ·𝑜
𝑥) = (𝐵 ·𝑜
∅)) |
3 | 2 | oveq2d 6666 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝐴 ·𝑜
(𝐵
·𝑜 𝑥)) = (𝐴 ·𝑜 (𝐵 ·𝑜
∅))) |
4 | 1, 3 | eqeq12d 2637 |
. . . . 5
⊢ (𝑥 = ∅ → (((𝐴 ·𝑜
𝐵)
·𝑜 𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑥)) ↔ ((𝐴 ·𝑜
𝐵)
·𝑜 ∅) = (𝐴 ·𝑜 (𝐵 ·𝑜
∅)))) |
5 | | oveq2 6658 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝐴 ·𝑜 𝐵) ·𝑜
𝑥) = ((𝐴 ·𝑜 𝐵) ·𝑜
𝑦)) |
6 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝐵 ·𝑜 𝑥) = (𝐵 ·𝑜 𝑦)) |
7 | 6 | oveq2d 6666 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝐴 ·𝑜 (𝐵 ·𝑜
𝑥)) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦))) |
8 | 5, 7 | eqeq12d 2637 |
. . . . 5
⊢ (𝑥 = 𝑦 → (((𝐴 ·𝑜 𝐵) ·𝑜
𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑥)) ↔ ((𝐴 ·𝑜
𝐵)
·𝑜 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)))) |
9 | | oveq2 6658 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → ((𝐴 ·𝑜 𝐵) ·𝑜
𝑥) = ((𝐴 ·𝑜 𝐵) ·𝑜
suc 𝑦)) |
10 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑥 = suc 𝑦 → (𝐵 ·𝑜 𝑥) = (𝐵 ·𝑜 suc 𝑦)) |
11 | 10 | oveq2d 6666 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → (𝐴 ·𝑜 (𝐵 ·𝑜
𝑥)) = (𝐴 ·𝑜 (𝐵 ·𝑜
suc 𝑦))) |
12 | 9, 11 | eqeq12d 2637 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → (((𝐴 ·𝑜 𝐵) ·𝑜
𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑥)) ↔ ((𝐴 ·𝑜
𝐵)
·𝑜 suc 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜
suc 𝑦)))) |
13 | | oveq2 6658 |
. . . . . 6
⊢ (𝑥 = 𝐶 → ((𝐴 ·𝑜 𝐵) ·𝑜
𝑥) = ((𝐴 ·𝑜 𝐵) ·𝑜
𝐶)) |
14 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑥 = 𝐶 → (𝐵 ·𝑜 𝑥) = (𝐵 ·𝑜 𝐶)) |
15 | 14 | oveq2d 6666 |
. . . . . 6
⊢ (𝑥 = 𝐶 → (𝐴 ·𝑜 (𝐵 ·𝑜
𝑥)) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝐶))) |
16 | 13, 15 | eqeq12d 2637 |
. . . . 5
⊢ (𝑥 = 𝐶 → (((𝐴 ·𝑜 𝐵) ·𝑜
𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑥)) ↔ ((𝐴 ·𝑜
𝐵)
·𝑜 𝐶) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝐶)))) |
17 | | omcl 7616 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·𝑜
𝐵) ∈
On) |
18 | | om0 7597 |
. . . . . . 7
⊢ ((𝐴 ·𝑜
𝐵) ∈ On → ((𝐴 ·𝑜
𝐵)
·𝑜 ∅) = ∅) |
19 | 17, 18 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·𝑜
𝐵)
·𝑜 ∅) = ∅) |
20 | | om0 7597 |
. . . . . . . 8
⊢ (𝐵 ∈ On → (𝐵 ·𝑜
∅) = ∅) |
21 | 20 | oveq2d 6666 |
. . . . . . 7
⊢ (𝐵 ∈ On → (𝐴 ·𝑜
(𝐵
·𝑜 ∅)) = (𝐴 ·𝑜
∅)) |
22 | | om0 7597 |
. . . . . . 7
⊢ (𝐴 ∈ On → (𝐴 ·𝑜
∅) = ∅) |
23 | 21, 22 | sylan9eqr 2678 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·𝑜
(𝐵
·𝑜 ∅)) = ∅) |
24 | 19, 23 | eqtr4d 2659 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·𝑜
𝐵)
·𝑜 ∅) = (𝐴 ·𝑜 (𝐵 ·𝑜
∅))) |
25 | | oveq1 6657 |
. . . . . . . . 9
⊢ (((𝐴 ·𝑜
𝐵)
·𝑜 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) → (((𝐴 ·𝑜
𝐵)
·𝑜 𝑦) +𝑜 (𝐴 ·𝑜 𝐵)) = ((𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) +𝑜
(𝐴
·𝑜 𝐵))) |
26 | | omsuc 7606 |
. . . . . . . . . . 11
⊢ (((𝐴 ·𝑜
𝐵) ∈ On ∧ 𝑦 ∈ On) → ((𝐴 ·𝑜
𝐵)
·𝑜 suc 𝑦) = (((𝐴 ·𝑜 𝐵) ·𝑜
𝑦) +𝑜
(𝐴
·𝑜 𝐵))) |
27 | 17, 26 | stoic3 1701 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → ((𝐴 ·𝑜
𝐵)
·𝑜 suc 𝑦) = (((𝐴 ·𝑜 𝐵) ·𝑜
𝑦) +𝑜
(𝐴
·𝑜 𝐵))) |
28 | | omsuc 7606 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ·𝑜
suc 𝑦) = ((𝐵 ·𝑜
𝑦) +𝑜
𝐵)) |
29 | 28 | 3adant1 1079 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ·𝑜
suc 𝑦) = ((𝐵 ·𝑜
𝑦) +𝑜
𝐵)) |
30 | 29 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·𝑜
(𝐵
·𝑜 suc 𝑦)) = (𝐴 ·𝑜 ((𝐵 ·𝑜
𝑦) +𝑜
𝐵))) |
31 | | omcl 7616 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ·𝑜
𝑦) ∈
On) |
32 | | odi 7659 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ On ∧ (𝐵 ·𝑜
𝑦) ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·𝑜
((𝐵
·𝑜 𝑦) +𝑜 𝐵)) = ((𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) +𝑜
(𝐴
·𝑜 𝐵))) |
33 | 31, 32 | syl3an2 1360 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝑦 ∈ On) ∧ 𝐵 ∈ On) → (𝐴 ·𝑜
((𝐵
·𝑜 𝑦) +𝑜 𝐵)) = ((𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) +𝑜
(𝐴
·𝑜 𝐵))) |
34 | 33 | 3exp 1264 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ On → ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ∈ On → (𝐴 ·𝑜
((𝐵
·𝑜 𝑦) +𝑜 𝐵)) = ((𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) +𝑜
(𝐴
·𝑜 𝐵))))) |
35 | 34 | expd 452 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ On → (𝐵 ∈ On → (𝑦 ∈ On → (𝐵 ∈ On → (𝐴 ·𝑜
((𝐵
·𝑜 𝑦) +𝑜 𝐵)) = ((𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) +𝑜
(𝐴
·𝑜 𝐵)))))) |
36 | 35 | com34 91 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ On → (𝐵 ∈ On → (𝐵 ∈ On → (𝑦 ∈ On → (𝐴 ·𝑜
((𝐵
·𝑜 𝑦) +𝑜 𝐵)) = ((𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) +𝑜
(𝐴
·𝑜 𝐵)))))) |
37 | 36 | pm2.43d 53 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ On → (𝐵 ∈ On → (𝑦 ∈ On → (𝐴 ·𝑜
((𝐵
·𝑜 𝑦) +𝑜 𝐵)) = ((𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) +𝑜
(𝐴
·𝑜 𝐵))))) |
38 | 37 | 3imp 1256 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·𝑜
((𝐵
·𝑜 𝑦) +𝑜 𝐵)) = ((𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) +𝑜
(𝐴
·𝑜 𝐵))) |
39 | 30, 38 | eqtrd 2656 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·𝑜
(𝐵
·𝑜 suc 𝑦)) = ((𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) +𝑜
(𝐴
·𝑜 𝐵))) |
40 | 27, 39 | eqeq12d 2637 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (((𝐴 ·𝑜
𝐵)
·𝑜 suc 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜
suc 𝑦)) ↔ (((𝐴 ·𝑜
𝐵)
·𝑜 𝑦) +𝑜 (𝐴 ·𝑜 𝐵)) = ((𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) +𝑜
(𝐴
·𝑜 𝐵)))) |
41 | 25, 40 | syl5ibr 236 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (((𝐴 ·𝑜
𝐵)
·𝑜 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) → ((𝐴 ·𝑜
𝐵)
·𝑜 suc 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜
suc 𝑦)))) |
42 | 41 | 3exp 1264 |
. . . . . . 7
⊢ (𝐴 ∈ On → (𝐵 ∈ On → (𝑦 ∈ On → (((𝐴 ·𝑜
𝐵)
·𝑜 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) → ((𝐴 ·𝑜
𝐵)
·𝑜 suc 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜
suc 𝑦)))))) |
43 | 42 | com3r 87 |
. . . . . 6
⊢ (𝑦 ∈ On → (𝐴 ∈ On → (𝐵 ∈ On → (((𝐴 ·𝑜
𝐵)
·𝑜 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) → ((𝐴 ·𝑜
𝐵)
·𝑜 suc 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜
suc 𝑦)))))) |
44 | 43 | impd 447 |
. . . . 5
⊢ (𝑦 ∈ On → ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (((𝐴 ·𝑜
𝐵)
·𝑜 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) → ((𝐴 ·𝑜
𝐵)
·𝑜 suc 𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜
suc 𝑦))))) |
45 | 17 | ancoms 469 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ On) → (𝐴 ·𝑜
𝐵) ∈
On) |
46 | | vex 3203 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V |
47 | | omlim 7613 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ·𝑜
𝐵) ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → ((𝐴 ·𝑜 𝐵) ·𝑜
𝑥) = ∪ 𝑦 ∈ 𝑥 ((𝐴 ·𝑜 𝐵) ·𝑜
𝑦)) |
48 | 46, 47 | mpanr1 719 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ·𝑜
𝐵) ∈ On ∧ Lim
𝑥) → ((𝐴 ·𝑜
𝐵)
·𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 ((𝐴 ·𝑜 𝐵) ·𝑜
𝑦)) |
49 | 45, 48 | sylan 488 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ On ∧ 𝐴 ∈ On) ∧ Lim 𝑥) → ((𝐴 ·𝑜 𝐵) ·𝑜
𝑥) = ∪ 𝑦 ∈ 𝑥 ((𝐴 ·𝑜 𝐵) ·𝑜
𝑦)) |
50 | 49 | an32s 846 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ On) → ((𝐴 ·𝑜 𝐵) ·𝑜
𝑥) = ∪ 𝑦 ∈ 𝑥 ((𝐴 ·𝑜 𝐵) ·𝑜
𝑦)) |
51 | 50 | ad2antrr 762 |
. . . . . . . . . . 11
⊢
(((((𝐵 ∈ On
∧ Lim 𝑥) ∧ 𝐴 ∈ On) ∧ ∅ ∈
𝐵) ∧ ∀𝑦 ∈ 𝑥 ((𝐴 ·𝑜 𝐵) ·𝑜
𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦))) → ((𝐴 ·𝑜
𝐵)
·𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 ((𝐴 ·𝑜 𝐵) ·𝑜
𝑦)) |
52 | | iuneq2 4537 |
. . . . . . . . . . . 12
⊢
(∀𝑦 ∈
𝑥 ((𝐴 ·𝑜 𝐵) ·𝑜
𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) → ∪ 𝑦 ∈ 𝑥 ((𝐴 ·𝑜 𝐵) ·𝑜
𝑦) = ∪ 𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦))) |
53 | | limelon 5788 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → 𝑥 ∈ On) |
54 | 46, 53 | mpan 706 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (Lim
𝑥 → 𝑥 ∈ On) |
55 | 54 | anim1i 592 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((Lim
𝑥 ∧ 𝐵 ∈ On) → (𝑥 ∈ On ∧ 𝐵 ∈ On)) |
56 | 55 | ancoms 469 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 ∈ On ∧ Lim 𝑥) → (𝑥 ∈ On ∧ 𝐵 ∈ On)) |
57 | | omordi 7646 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈
𝐵) → (𝑦 ∈ 𝑥 → (𝐵 ·𝑜 𝑦) ∈ (𝐵 ·𝑜 𝑥))) |
58 | 56, 57 | sylan 488 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐵 ∈ On ∧ Lim 𝑥) ∧ ∅ ∈ 𝐵) → (𝑦 ∈ 𝑥 → (𝐵 ·𝑜 𝑦) ∈ (𝐵 ·𝑜 𝑥))) |
59 | | ssid 3624 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ·𝑜
(𝐵
·𝑜 𝑦)) ⊆ (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) |
60 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = (𝐵 ·𝑜 𝑦) → (𝐴 ·𝑜 𝑧) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦))) |
61 | 60 | sseq2d 3633 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = (𝐵 ·𝑜 𝑦) → ((𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) ⊆ (𝐴 ·𝑜
𝑧) ↔ (𝐴 ·𝑜
(𝐵
·𝑜 𝑦)) ⊆ (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)))) |
62 | 61 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐵 ·𝑜
𝑦) ∈ (𝐵 ·𝑜
𝑥) ∧ (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) ⊆ (𝐴 ·𝑜
(𝐵
·𝑜 𝑦))) → ∃𝑧 ∈ (𝐵 ·𝑜 𝑥)(𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) ⊆ (𝐴 ·𝑜
𝑧)) |
63 | 59, 62 | mpan2 707 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ·𝑜
𝑦) ∈ (𝐵 ·𝑜
𝑥) → ∃𝑧 ∈ (𝐵 ·𝑜 𝑥)(𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) ⊆ (𝐴 ·𝑜
𝑧)) |
64 | 58, 63 | syl6 35 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐵 ∈ On ∧ Lim 𝑥) ∧ ∅ ∈ 𝐵) → (𝑦 ∈ 𝑥 → ∃𝑧 ∈ (𝐵 ·𝑜 𝑥)(𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) ⊆ (𝐴 ·𝑜
𝑧))) |
65 | 64 | ralrimiv 2965 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐵 ∈ On ∧ Lim 𝑥) ∧ ∅ ∈ 𝐵) → ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ (𝐵 ·𝑜 𝑥)(𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) ⊆ (𝐴 ·𝑜
𝑧)) |
66 | | iunss2 4565 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑦 ∈
𝑥 ∃𝑧 ∈ (𝐵 ·𝑜 𝑥)(𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) ⊆ (𝐴 ·𝑜
𝑧) → ∪ 𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) ⊆ ∪ 𝑧 ∈ (𝐵 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧)) |
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ∈ On ∧ Lim 𝑥) ∧ ∅ ∈ 𝐵) → ∪ 𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) ⊆ ∪ 𝑧 ∈ (𝐵 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧)) |
68 | 67 | adantlr 751 |
. . . . . . . . . . . . . 14
⊢ ((((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐵) → ∪ 𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) ⊆ ∪ 𝑧 ∈ (𝐵 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧)) |
69 | | omcl 7616 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On) → (𝐵 ·𝑜
𝑥) ∈
On) |
70 | 54, 69 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 ∈ On ∧ Lim 𝑥) → (𝐵 ·𝑜 𝑥) ∈ On) |
71 | | onelon 5748 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐵 ·𝑜
𝑥) ∈ On ∧ 𝑧 ∈ (𝐵 ·𝑜 𝑥)) → 𝑧 ∈ On) |
72 | 70, 71 | sylan 488 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝑧 ∈ (𝐵 ·𝑜 𝑥)) → 𝑧 ∈ On) |
73 | 72 | adantlr 751 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ On) ∧ 𝑧 ∈ (𝐵 ·𝑜 𝑥)) → 𝑧 ∈ On) |
74 | | omordlim 7657 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐵 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ 𝑧 ∈ (𝐵 ·𝑜 𝑥)) → ∃𝑦 ∈ 𝑥 𝑧 ∈ (𝐵 ·𝑜 𝑦)) |
75 | 74 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐵 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → (𝑧 ∈ (𝐵 ·𝑜 𝑥) → ∃𝑦 ∈ 𝑥 𝑧 ∈ (𝐵 ·𝑜 𝑦))) |
76 | 46, 75 | mpanr1 719 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐵 ∈ On ∧ Lim 𝑥) → (𝑧 ∈ (𝐵 ·𝑜 𝑥) → ∃𝑦 ∈ 𝑥 𝑧 ∈ (𝐵 ·𝑜 𝑦))) |
77 | 76 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑧 ∈ On ∧ (𝐵 ∈ On ∧ Lim 𝑥)) ∧ 𝐴 ∈ On) → (𝑧 ∈ (𝐵 ·𝑜 𝑥) → ∃𝑦 ∈ 𝑥 𝑧 ∈ (𝐵 ·𝑜 𝑦))) |
78 | | onelon 5748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On) |
79 | 54, 78 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((Lim
𝑥 ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On) |
80 | 79, 31 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐵 ∈ On ∧ (Lim 𝑥 ∧ 𝑦 ∈ 𝑥)) → (𝐵 ·𝑜 𝑦) ∈ On) |
81 | | onelss 5766 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐵 ·𝑜
𝑦) ∈ On → (𝑧 ∈ (𝐵 ·𝑜 𝑦) → 𝑧 ⊆ (𝐵 ·𝑜 𝑦))) |
82 | 81 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑧 ∈ On ∧ (𝐵 ·𝑜
𝑦) ∈ On ∧ 𝐴 ∈ On) → (𝑧 ∈ (𝐵 ·𝑜 𝑦) → 𝑧 ⊆ (𝐵 ·𝑜 𝑦))) |
83 | | omwordi 7651 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑧 ∈ On ∧ (𝐵 ·𝑜
𝑦) ∈ On ∧ 𝐴 ∈ On) → (𝑧 ⊆ (𝐵 ·𝑜 𝑦) → (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)))) |
84 | 82, 83 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑧 ∈ On ∧ (𝐵 ·𝑜
𝑦) ∈ On ∧ 𝐴 ∈ On) → (𝑧 ∈ (𝐵 ·𝑜 𝑦) → (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)))) |
85 | 84 | 3exp 1264 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑧 ∈ On → ((𝐵 ·𝑜
𝑦) ∈ On → (𝐴 ∈ On → (𝑧 ∈ (𝐵 ·𝑜 𝑦) → (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)))))) |
86 | 80, 85 | syl5 34 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 ∈ On → ((𝐵 ∈ On ∧ (Lim 𝑥 ∧ 𝑦 ∈ 𝑥)) → (𝐴 ∈ On → (𝑧 ∈ (𝐵 ·𝑜 𝑦) → (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)))))) |
87 | 86 | exp4d 637 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 ∈ On → (𝐵 ∈ On → (Lim 𝑥 → (𝑦 ∈ 𝑥 → (𝐴 ∈ On → (𝑧 ∈ (𝐵 ·𝑜 𝑦) → (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)))))))) |
88 | 87 | imp32 449 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑧 ∈ On ∧ (𝐵 ∈ On ∧ Lim 𝑥)) → (𝑦 ∈ 𝑥 → (𝐴 ∈ On → (𝑧 ∈ (𝐵 ·𝑜 𝑦) → (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)))))) |
89 | 88 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑧 ∈ On ∧ (𝐵 ∈ On ∧ Lim 𝑥)) → (𝐴 ∈ On → (𝑦 ∈ 𝑥 → (𝑧 ∈ (𝐵 ·𝑜 𝑦) → (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)))))) |
90 | 89 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑧 ∈ On ∧ (𝐵 ∈ On ∧ Lim 𝑥)) ∧ 𝐴 ∈ On) → (𝑦 ∈ 𝑥 → (𝑧 ∈ (𝐵 ·𝑜 𝑦) → (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦))))) |
91 | 90 | reximdvai 3015 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑧 ∈ On ∧ (𝐵 ∈ On ∧ Lim 𝑥)) ∧ 𝐴 ∈ On) → (∃𝑦 ∈ 𝑥 𝑧 ∈ (𝐵 ·𝑜 𝑦) → ∃𝑦 ∈ 𝑥 (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)))) |
92 | 77, 91 | syld 47 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑧 ∈ On ∧ (𝐵 ∈ On ∧ Lim 𝑥)) ∧ 𝐴 ∈ On) → (𝑧 ∈ (𝐵 ·𝑜 𝑥) → ∃𝑦 ∈ 𝑥 (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)))) |
93 | 92 | exp31 630 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ On → ((𝐵 ∈ On ∧ Lim 𝑥) → (𝐴 ∈ On → (𝑧 ∈ (𝐵 ·𝑜 𝑥) → ∃𝑦 ∈ 𝑥 (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)))))) |
94 | 93 | imp4c 617 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ On → ((((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ On) ∧ 𝑧 ∈ (𝐵 ·𝑜 𝑥)) → ∃𝑦 ∈ 𝑥 (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)))) |
95 | 73, 94 | mpcom 38 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ On) ∧ 𝑧 ∈ (𝐵 ·𝑜 𝑥)) → ∃𝑦 ∈ 𝑥 (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦))) |
96 | 95 | ralrimiva 2966 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ On) → ∀𝑧 ∈ (𝐵 ·𝑜 𝑥)∃𝑦 ∈ 𝑥 (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦))) |
97 | | iunss2 4565 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑧 ∈
(𝐵
·𝑜 𝑥)∃𝑦 ∈ 𝑥 (𝐴 ·𝑜 𝑧) ⊆ (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) → ∪ 𝑧 ∈ (𝐵 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧) ⊆ ∪ 𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦))) |
98 | 96, 97 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ On) → ∪ 𝑧 ∈ (𝐵 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧) ⊆ ∪ 𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦))) |
99 | 98 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐵) → ∪ 𝑧 ∈ (𝐵 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧) ⊆ ∪ 𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦))) |
100 | 68, 99 | eqssd 3620 |
. . . . . . . . . . . . 13
⊢ ((((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐵) → ∪ 𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) = ∪ 𝑧 ∈ (𝐵 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧)) |
101 | | omlimcl 7658 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐵 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ ∅ ∈ 𝐵) → Lim (𝐵 ·𝑜 𝑥)) |
102 | 46, 101 | mpanlr1 722 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐵 ∈ On ∧ Lim 𝑥) ∧ ∅ ∈ 𝐵) → Lim (𝐵 ·𝑜 𝑥)) |
103 | | ovex 6678 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐵 ·𝑜
𝑥) ∈
V |
104 | | omlim 7613 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ On ∧ ((𝐵 ·𝑜
𝑥) ∈ V ∧ Lim
(𝐵
·𝑜 𝑥))) → (𝐴 ·𝑜 (𝐵 ·𝑜
𝑥)) = ∪ 𝑧 ∈ (𝐵 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧)) |
105 | 103, 104 | mpanr1 719 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ On ∧ Lim (𝐵 ·𝑜
𝑥)) → (𝐴 ·𝑜
(𝐵
·𝑜 𝑥)) = ∪
𝑧 ∈ (𝐵 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧)) |
106 | 102, 105 | sylan2 491 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ On ∧ ((𝐵 ∈ On ∧ Lim 𝑥) ∧ ∅ ∈ 𝐵)) → (𝐴 ·𝑜 (𝐵 ·𝑜
𝑥)) = ∪ 𝑧 ∈ (𝐵 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧)) |
107 | 106 | ancoms 469 |
. . . . . . . . . . . . . 14
⊢ ((((𝐵 ∈ On ∧ Lim 𝑥) ∧ ∅ ∈ 𝐵) ∧ 𝐴 ∈ On) → (𝐴 ·𝑜 (𝐵 ·𝑜
𝑥)) = ∪ 𝑧 ∈ (𝐵 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧)) |
108 | 107 | an32s 846 |
. . . . . . . . . . . . 13
⊢ ((((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐵) → (𝐴 ·𝑜 (𝐵 ·𝑜
𝑥)) = ∪ 𝑧 ∈ (𝐵 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧)) |
109 | 100, 108 | eqtr4d 2659 |
. . . . . . . . . . . 12
⊢ ((((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐵) → ∪ 𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑥))) |
110 | 52, 109 | sylan9eqr 2678 |
. . . . . . . . . . 11
⊢
(((((𝐵 ∈ On
∧ Lim 𝑥) ∧ 𝐴 ∈ On) ∧ ∅ ∈
𝐵) ∧ ∀𝑦 ∈ 𝑥 ((𝐴 ·𝑜 𝐵) ·𝑜
𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦))) → ∪ 𝑦 ∈ 𝑥 ((𝐴 ·𝑜 𝐵) ·𝑜
𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑥))) |
111 | 51, 110 | eqtrd 2656 |
. . . . . . . . . 10
⊢
(((((𝐵 ∈ On
∧ Lim 𝑥) ∧ 𝐴 ∈ On) ∧ ∅ ∈
𝐵) ∧ ∀𝑦 ∈ 𝑥 ((𝐴 ·𝑜 𝐵) ·𝑜
𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦))) → ((𝐴 ·𝑜
𝐵)
·𝑜 𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑥))) |
112 | 111 | exp31 630 |
. . . . . . . . 9
⊢ (((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ On) → (∅ ∈ 𝐵 → (∀𝑦 ∈ 𝑥 ((𝐴 ·𝑜 𝐵) ·𝑜
𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) → ((𝐴 ·𝑜
𝐵)
·𝑜 𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑥))))) |
113 | | eloni 5733 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ On → Ord 𝐵) |
114 | | ord0eln0 5779 |
. . . . . . . . . . . . . 14
⊢ (Ord
𝐵 → (∅ ∈
𝐵 ↔ 𝐵 ≠ ∅)) |
115 | 114 | necon2bbid 2837 |
. . . . . . . . . . . . 13
⊢ (Ord
𝐵 → (𝐵 = ∅ ↔ ¬ ∅ ∈ 𝐵)) |
116 | 113, 115 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ On → (𝐵 = ∅ ↔ ¬ ∅
∈ 𝐵)) |
117 | 116 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ On) → (𝐵 = ∅ ↔ ¬ ∅ ∈ 𝐵)) |
118 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 = ∅ → (𝐴 ·𝑜
𝐵) = (𝐴 ·𝑜
∅)) |
119 | 118, 22 | sylan9eqr 2678 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ On ∧ 𝐵 = ∅) → (𝐴 ·𝑜
𝐵) =
∅) |
120 | 119 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ On ∧ 𝐵 = ∅) → ((𝐴 ·𝑜
𝐵)
·𝑜 𝑥) = (∅ ·𝑜
𝑥)) |
121 | | om0r 7619 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ On → (∅
·𝑜 𝑥) = ∅) |
122 | 120, 121 | sylan9eqr 2678 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ On ∧ (𝐴 ∈ On ∧ 𝐵 = ∅)) → ((𝐴 ·𝑜
𝐵)
·𝑜 𝑥) = ∅) |
123 | 122 | anassrs 680 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ On ∧ 𝐴 ∈ On) ∧ 𝐵 = ∅) → ((𝐴 ·𝑜
𝐵)
·𝑜 𝑥) = ∅) |
124 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 = ∅ → (𝐵 ·𝑜
𝑥) = (∅
·𝑜 𝑥)) |
125 | 124, 121 | sylan9eqr 2678 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ On ∧ 𝐵 = ∅) → (𝐵 ·𝑜
𝑥) =
∅) |
126 | 125 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ On ∧ 𝐵 = ∅) → (𝐴 ·𝑜
(𝐵
·𝑜 𝑥)) = (𝐴 ·𝑜
∅)) |
127 | 126, 22 | sylan9eq 2676 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ On ∧ 𝐵 = ∅) ∧ 𝐴 ∈ On) → (𝐴 ·𝑜
(𝐵
·𝑜 𝑥)) = ∅) |
128 | 127 | an32s 846 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ On ∧ 𝐴 ∈ On) ∧ 𝐵 = ∅) → (𝐴 ·𝑜
(𝐵
·𝑜 𝑥)) = ∅) |
129 | 123, 128 | eqtr4d 2659 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ On ∧ 𝐴 ∈ On) ∧ 𝐵 = ∅) → ((𝐴 ·𝑜
𝐵)
·𝑜 𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑥))) |
130 | 129 | ex 450 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ On ∧ 𝐴 ∈ On) → (𝐵 = ∅ → ((𝐴 ·𝑜
𝐵)
·𝑜 𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑥)))) |
131 | 54, 130 | sylan 488 |
. . . . . . . . . . . 12
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ On) → (𝐵 = ∅ → ((𝐴 ·𝑜 𝐵) ·𝑜
𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑥)))) |
132 | 131 | adantll 750 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ On) → (𝐵 = ∅ → ((𝐴 ·𝑜 𝐵) ·𝑜
𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑥)))) |
133 | 117, 132 | sylbird 250 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ On) → (¬ ∅ ∈
𝐵 → ((𝐴 ·𝑜
𝐵)
·𝑜 𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑥)))) |
134 | 133 | a1dd 50 |
. . . . . . . . 9
⊢ (((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ On) → (¬ ∅ ∈
𝐵 → (∀𝑦 ∈ 𝑥 ((𝐴 ·𝑜 𝐵) ·𝑜
𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) → ((𝐴 ·𝑜
𝐵)
·𝑜 𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑥))))) |
135 | 112, 134 | pm2.61d 170 |
. . . . . . . 8
⊢ (((𝐵 ∈ On ∧ Lim 𝑥) ∧ 𝐴 ∈ On) → (∀𝑦 ∈ 𝑥 ((𝐴 ·𝑜 𝐵) ·𝑜
𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) → ((𝐴 ·𝑜
𝐵)
·𝑜 𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑥)))) |
136 | 135 | exp31 630 |
. . . . . . 7
⊢ (𝐵 ∈ On → (Lim 𝑥 → (𝐴 ∈ On → (∀𝑦 ∈ 𝑥 ((𝐴 ·𝑜 𝐵) ·𝑜
𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) → ((𝐴 ·𝑜
𝐵)
·𝑜 𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑥)))))) |
137 | 136 | com3l 89 |
. . . . . 6
⊢ (Lim
𝑥 → (𝐴 ∈ On → (𝐵 ∈ On → (∀𝑦 ∈ 𝑥 ((𝐴 ·𝑜 𝐵) ·𝑜
𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) → ((𝐴 ·𝑜
𝐵)
·𝑜 𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑥)))))) |
138 | 137 | impd 447 |
. . . . 5
⊢ (Lim
𝑥 → ((𝐴 ∈ On ∧ 𝐵 ∈ On) →
(∀𝑦 ∈ 𝑥 ((𝐴 ·𝑜 𝐵) ·𝑜
𝑦) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑦)) → ((𝐴 ·𝑜
𝐵)
·𝑜 𝑥) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝑥))))) |
139 | 4, 8, 12, 16, 24, 44, 138 | tfinds3 7064 |
. . . 4
⊢ (𝐶 ∈ On → ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·𝑜
𝐵)
·𝑜 𝐶) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝐶)))) |
140 | 139 | expd 452 |
. . 3
⊢ (𝐶 ∈ On → (𝐴 ∈ On → (𝐵 ∈ On → ((𝐴 ·𝑜
𝐵)
·𝑜 𝐶) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝐶))))) |
141 | 140 | com3l 89 |
. 2
⊢ (𝐴 ∈ On → (𝐵 ∈ On → (𝐶 ∈ On → ((𝐴 ·𝑜
𝐵)
·𝑜 𝐶) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝐶))))) |
142 | 141 | 3imp 1256 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ·𝑜
𝐵)
·𝑜 𝐶) = (𝐴 ·𝑜 (𝐵 ·𝑜
𝐶))) |