Step | Hyp | Ref
| Expression |
1 | | oveq2 6658 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝐵 +𝑜 𝑥) = (𝐵 +𝑜
∅)) |
2 | 1 | oveq2d 6666 |
. . . . 5
⊢ (𝑥 = ∅ → (𝐴 ·𝑜
(𝐵 +𝑜
𝑥)) = (𝐴 ·𝑜 (𝐵 +𝑜
∅))) |
3 | | oveq2 6658 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝐴 ·𝑜
𝑥) = (𝐴 ·𝑜
∅)) |
4 | 3 | oveq2d 6666 |
. . . . 5
⊢ (𝑥 = ∅ → ((𝐴 ·𝑜
𝐵) +𝑜
(𝐴
·𝑜 𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
∅))) |
5 | 2, 4 | eqeq12d 2637 |
. . . 4
⊢ (𝑥 = ∅ → ((𝐴 ·𝑜
(𝐵 +𝑜
𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑥)) ↔ (𝐴 ·𝑜
(𝐵 +𝑜
∅)) = ((𝐴
·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
∅)))) |
6 | | oveq2 6658 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝐵 +𝑜 𝑥) = (𝐵 +𝑜 𝑦)) |
7 | 6 | oveq2d 6666 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = (𝐴 ·𝑜 (𝐵 +𝑜 𝑦))) |
8 | | oveq2 6658 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝐴 ·𝑜 𝑥) = (𝐴 ·𝑜 𝑦)) |
9 | 8 | oveq2d 6666 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦))) |
10 | 7, 9 | eqeq12d 2637 |
. . . 4
⊢ (𝑥 = 𝑦 → ((𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑥)) ↔ (𝐴 ·𝑜
(𝐵 +𝑜
𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)))) |
11 | | oveq2 6658 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → (𝐵 +𝑜 𝑥) = (𝐵 +𝑜 suc 𝑦)) |
12 | 11 | oveq2d 6666 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → (𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = (𝐴 ·𝑜 (𝐵 +𝑜 suc 𝑦))) |
13 | | oveq2 6658 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → (𝐴 ·𝑜 𝑥) = (𝐴 ·𝑜 suc 𝑦)) |
14 | 13 | oveq2d 6666 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
suc 𝑦))) |
15 | 12, 14 | eqeq12d 2637 |
. . . 4
⊢ (𝑥 = suc 𝑦 → ((𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑥)) ↔ (𝐴 ·𝑜
(𝐵 +𝑜
suc 𝑦)) = ((𝐴 ·𝑜
𝐵) +𝑜
(𝐴
·𝑜 suc 𝑦)))) |
16 | | oveq2 6658 |
. . . . . 6
⊢ (𝑥 = 𝐶 → (𝐵 +𝑜 𝑥) = (𝐵 +𝑜 𝐶)) |
17 | 16 | oveq2d 6666 |
. . . . 5
⊢ (𝑥 = 𝐶 → (𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = (𝐴 ·𝑜 (𝐵 +𝑜 𝐶))) |
18 | | oveq2 6658 |
. . . . . 6
⊢ (𝑥 = 𝐶 → (𝐴 ·𝑜 𝑥) = (𝐴 ·𝑜 𝐶)) |
19 | 18 | oveq2d 6666 |
. . . . 5
⊢ (𝑥 = 𝐶 → ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝐶))) |
20 | 17, 19 | eqeq12d 2637 |
. . . 4
⊢ (𝑥 = 𝐶 → ((𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑥)) ↔ (𝐴 ·𝑜
(𝐵 +𝑜
𝐶)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝐶)))) |
21 | | omcl 7616 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·𝑜
𝐵) ∈
On) |
22 | | oa0 7596 |
. . . . . 6
⊢ ((𝐴 ·𝑜
𝐵) ∈ On → ((𝐴 ·𝑜
𝐵) +𝑜
∅) = (𝐴
·𝑜 𝐵)) |
23 | 21, 22 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·𝑜
𝐵) +𝑜
∅) = (𝐴
·𝑜 𝐵)) |
24 | | om0 7597 |
. . . . . . 7
⊢ (𝐴 ∈ On → (𝐴 ·𝑜
∅) = ∅) |
25 | 24 | adantr 481 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·𝑜
∅) = ∅) |
26 | 25 | oveq2d 6666 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·𝑜
𝐵) +𝑜
(𝐴
·𝑜 ∅)) = ((𝐴 ·𝑜 𝐵) +𝑜
∅)) |
27 | | oa0 7596 |
. . . . . . 7
⊢ (𝐵 ∈ On → (𝐵 +𝑜 ∅)
= 𝐵) |
28 | 27 | adantl 482 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐵 +𝑜 ∅)
= 𝐵) |
29 | 28 | oveq2d 6666 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·𝑜
(𝐵 +𝑜
∅)) = (𝐴
·𝑜 𝐵)) |
30 | 23, 26, 29 | 3eqtr4rd 2667 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·𝑜
(𝐵 +𝑜
∅)) = ((𝐴
·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
∅))) |
31 | | oveq1 6657 |
. . . . . . . 8
⊢ ((𝐴 ·𝑜
(𝐵 +𝑜
𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)) → ((𝐴 ·𝑜
(𝐵 +𝑜
𝑦)) +𝑜
𝐴) = (((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)) +𝑜
𝐴)) |
32 | | oasuc 7604 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 +𝑜 suc 𝑦) = suc (𝐵 +𝑜 𝑦)) |
33 | 32 | 3adant1 1079 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 +𝑜 suc 𝑦) = suc (𝐵 +𝑜 𝑦)) |
34 | 33 | oveq2d 6666 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·𝑜
(𝐵 +𝑜
suc 𝑦)) = (𝐴 ·𝑜
suc (𝐵
+𝑜 𝑦))) |
35 | | oacl 7615 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 +𝑜 𝑦) ∈ On) |
36 | | omsuc 7606 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ (𝐵 +𝑜 𝑦) ∈ On) → (𝐴 ·𝑜
suc (𝐵
+𝑜 𝑦)) =
((𝐴
·𝑜 (𝐵 +𝑜 𝑦)) +𝑜 𝐴)) |
37 | 35, 36 | sylan2 491 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝑦 ∈ On)) → (𝐴 ·𝑜
suc (𝐵
+𝑜 𝑦)) =
((𝐴
·𝑜 (𝐵 +𝑜 𝑦)) +𝑜 𝐴)) |
38 | 37 | 3impb 1260 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·𝑜
suc (𝐵
+𝑜 𝑦)) =
((𝐴
·𝑜 (𝐵 +𝑜 𝑦)) +𝑜 𝐴)) |
39 | 34, 38 | eqtrd 2656 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·𝑜
(𝐵 +𝑜
suc 𝑦)) = ((𝐴 ·𝑜
(𝐵 +𝑜
𝑦)) +𝑜
𝐴)) |
40 | | omsuc 7606 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·𝑜
suc 𝑦) = ((𝐴 ·𝑜
𝑦) +𝑜
𝐴)) |
41 | 40 | 3adant2 1080 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·𝑜
suc 𝑦) = ((𝐴 ·𝑜
𝑦) +𝑜
𝐴)) |
42 | 41 | oveq2d 6666 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → ((𝐴 ·𝑜
𝐵) +𝑜
(𝐴
·𝑜 suc 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 ((𝐴 ·𝑜
𝑦) +𝑜
𝐴))) |
43 | | omcl 7616 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·𝑜
𝑦) ∈
On) |
44 | | oaass 7641 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ·𝑜
𝐵) ∈ On ∧ (𝐴 ·𝑜
𝑦) ∈ On ∧ 𝐴 ∈ On) → (((𝐴 ·𝑜
𝐵) +𝑜
(𝐴
·𝑜 𝑦)) +𝑜 𝐴) = ((𝐴 ·𝑜 𝐵) +𝑜 ((𝐴 ·𝑜
𝑦) +𝑜
𝐴))) |
45 | 21, 44 | syl3an1 1359 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 ·𝑜
𝑦) ∈ On ∧ 𝐴 ∈ On) → (((𝐴 ·𝑜
𝐵) +𝑜
(𝐴
·𝑜 𝑦)) +𝑜 𝐴) = ((𝐴 ·𝑜 𝐵) +𝑜 ((𝐴 ·𝑜
𝑦) +𝑜
𝐴))) |
46 | 43, 45 | syl3an2 1360 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 ∈ On ∧ 𝑦 ∈ On) ∧ 𝐴 ∈ On) → (((𝐴 ·𝑜
𝐵) +𝑜
(𝐴
·𝑜 𝑦)) +𝑜 𝐴) = ((𝐴 ·𝑜 𝐵) +𝑜 ((𝐴 ·𝑜
𝑦) +𝑜
𝐴))) |
47 | 46 | 3exp 1264 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ∈ On → (((𝐴 ·𝑜
𝐵) +𝑜
(𝐴
·𝑜 𝑦)) +𝑜 𝐴) = ((𝐴 ·𝑜 𝐵) +𝑜 ((𝐴 ·𝑜
𝑦) +𝑜
𝐴))))) |
48 | 47 | exp4b 632 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ On → (𝐵 ∈ On → (𝐴 ∈ On → (𝑦 ∈ On → (𝐴 ∈ On → (((𝐴 ·𝑜
𝐵) +𝑜
(𝐴
·𝑜 𝑦)) +𝑜 𝐴) = ((𝐴 ·𝑜 𝐵) +𝑜 ((𝐴 ·𝑜
𝑦) +𝑜
𝐴))))))) |
49 | 48 | pm2.43a 54 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ On → (𝐵 ∈ On → (𝑦 ∈ On → (𝐴 ∈ On → (((𝐴 ·𝑜
𝐵) +𝑜
(𝐴
·𝑜 𝑦)) +𝑜 𝐴) = ((𝐴 ·𝑜 𝐵) +𝑜 ((𝐴 ·𝑜
𝑦) +𝑜
𝐴)))))) |
50 | 49 | com4r 94 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ On → (𝐴 ∈ On → (𝐵 ∈ On → (𝑦 ∈ On → (((𝐴 ·𝑜
𝐵) +𝑜
(𝐴
·𝑜 𝑦)) +𝑜 𝐴) = ((𝐴 ·𝑜 𝐵) +𝑜 ((𝐴 ·𝑜
𝑦) +𝑜
𝐴)))))) |
51 | 50 | pm2.43i 52 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ On → (𝐵 ∈ On → (𝑦 ∈ On → (((𝐴 ·𝑜
𝐵) +𝑜
(𝐴
·𝑜 𝑦)) +𝑜 𝐴) = ((𝐴 ·𝑜 𝐵) +𝑜 ((𝐴 ·𝑜
𝑦) +𝑜
𝐴))))) |
52 | 51 | 3imp 1256 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (((𝐴 ·𝑜
𝐵) +𝑜
(𝐴
·𝑜 𝑦)) +𝑜 𝐴) = ((𝐴 ·𝑜 𝐵) +𝑜 ((𝐴 ·𝑜
𝑦) +𝑜
𝐴))) |
53 | 42, 52 | eqtr4d 2659 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → ((𝐴 ·𝑜
𝐵) +𝑜
(𝐴
·𝑜 suc 𝑦)) = (((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)) +𝑜
𝐴)) |
54 | 39, 53 | eqeq12d 2637 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → ((𝐴 ·𝑜
(𝐵 +𝑜
suc 𝑦)) = ((𝐴 ·𝑜
𝐵) +𝑜
(𝐴
·𝑜 suc 𝑦)) ↔ ((𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) +𝑜 𝐴) = (((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)) +𝑜
𝐴))) |
55 | 31, 54 | syl5ibr 236 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → ((𝐴 ·𝑜
(𝐵 +𝑜
𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)) → (𝐴 ·𝑜
(𝐵 +𝑜
suc 𝑦)) = ((𝐴 ·𝑜
𝐵) +𝑜
(𝐴
·𝑜 suc 𝑦)))) |
56 | 55 | 3exp 1264 |
. . . . . 6
⊢ (𝐴 ∈ On → (𝐵 ∈ On → (𝑦 ∈ On → ((𝐴 ·𝑜
(𝐵 +𝑜
𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)) → (𝐴 ·𝑜
(𝐵 +𝑜
suc 𝑦)) = ((𝐴 ·𝑜
𝐵) +𝑜
(𝐴
·𝑜 suc 𝑦)))))) |
57 | 56 | com3r 87 |
. . . . 5
⊢ (𝑦 ∈ On → (𝐴 ∈ On → (𝐵 ∈ On → ((𝐴 ·𝑜
(𝐵 +𝑜
𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)) → (𝐴 ·𝑜
(𝐵 +𝑜
suc 𝑦)) = ((𝐴 ·𝑜
𝐵) +𝑜
(𝐴
·𝑜 suc 𝑦)))))) |
58 | 57 | impd 447 |
. . . 4
⊢ (𝑦 ∈ On → ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·𝑜
(𝐵 +𝑜
𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)) → (𝐴 ·𝑜
(𝐵 +𝑜
suc 𝑦)) = ((𝐴 ·𝑜
𝐵) +𝑜
(𝐴
·𝑜 suc 𝑦))))) |
59 | | vex 3203 |
. . . . . . . . . . . . . 14
⊢ 𝑥 ∈ V |
60 | | limelon 5788 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → 𝑥 ∈ On) |
61 | 59, 60 | mpan 706 |
. . . . . . . . . . . . 13
⊢ (Lim
𝑥 → 𝑥 ∈ On) |
62 | | oacl 7615 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On) → (𝐵 +𝑜 𝑥) ∈ On) |
63 | | om0r 7619 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 +𝑜 𝑥) ∈ On → (∅
·𝑜 (𝐵 +𝑜 𝑥)) = ∅) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On) → (∅
·𝑜 (𝐵 +𝑜 𝑥)) = ∅) |
65 | | om0r 7619 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ On → (∅
·𝑜 𝐵) = ∅) |
66 | | om0r 7619 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ On → (∅
·𝑜 𝑥) = ∅) |
67 | 65, 66 | oveqan12d 6669 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On) → ((∅
·𝑜 𝐵) +𝑜 (∅
·𝑜 𝑥)) = (∅ +𝑜
∅)) |
68 | | 0elon 5778 |
. . . . . . . . . . . . . . . 16
⊢ ∅
∈ On |
69 | | oa0 7596 |
. . . . . . . . . . . . . . . 16
⊢ (∅
∈ On → (∅ +𝑜 ∅) =
∅) |
70 | 68, 69 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (∅
+𝑜 ∅) = ∅ |
71 | 67, 70 | syl6req 2673 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On) → ∅ =
((∅ ·𝑜 𝐵) +𝑜 (∅
·𝑜 𝑥))) |
72 | 64, 71 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On) → (∅
·𝑜 (𝐵 +𝑜 𝑥)) = ((∅ ·𝑜
𝐵) +𝑜
(∅ ·𝑜 𝑥))) |
73 | 61, 72 | sylan2 491 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ On ∧ Lim 𝑥) → (∅
·𝑜 (𝐵 +𝑜 𝑥)) = ((∅ ·𝑜
𝐵) +𝑜
(∅ ·𝑜 𝑥))) |
74 | 73 | ancoms 469 |
. . . . . . . . . . 11
⊢ ((Lim
𝑥 ∧ 𝐵 ∈ On) → (∅
·𝑜 (𝐵 +𝑜 𝑥)) = ((∅ ·𝑜
𝐵) +𝑜
(∅ ·𝑜 𝑥))) |
75 | | oveq1 6657 |
. . . . . . . . . . . 12
⊢ (𝐴 = ∅ → (𝐴 ·𝑜
(𝐵 +𝑜
𝑥)) = (∅
·𝑜 (𝐵 +𝑜 𝑥))) |
76 | | oveq1 6657 |
. . . . . . . . . . . . 13
⊢ (𝐴 = ∅ → (𝐴 ·𝑜
𝐵) = (∅
·𝑜 𝐵)) |
77 | | oveq1 6657 |
. . . . . . . . . . . . 13
⊢ (𝐴 = ∅ → (𝐴 ·𝑜
𝑥) = (∅
·𝑜 𝑥)) |
78 | 76, 77 | oveq12d 6668 |
. . . . . . . . . . . 12
⊢ (𝐴 = ∅ → ((𝐴 ·𝑜
𝐵) +𝑜
(𝐴
·𝑜 𝑥)) = ((∅ ·𝑜
𝐵) +𝑜
(∅ ·𝑜 𝑥))) |
79 | 75, 78 | eqeq12d 2637 |
. . . . . . . . . . 11
⊢ (𝐴 = ∅ → ((𝐴 ·𝑜
(𝐵 +𝑜
𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑥)) ↔ (∅
·𝑜 (𝐵 +𝑜 𝑥)) = ((∅ ·𝑜
𝐵) +𝑜
(∅ ·𝑜 𝑥)))) |
80 | 74, 79 | syl5ibr 236 |
. . . . . . . . . 10
⊢ (𝐴 = ∅ → ((Lim 𝑥 ∧ 𝐵 ∈ On) → (𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑥)))) |
81 | 80 | expd 452 |
. . . . . . . . 9
⊢ (𝐴 = ∅ → (Lim 𝑥 → (𝐵 ∈ On → (𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑥))))) |
82 | 81 | com3r 87 |
. . . . . . . 8
⊢ (𝐵 ∈ On → (𝐴 = ∅ → (Lim 𝑥 → (𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑥))))) |
83 | 82 | imp 445 |
. . . . . . 7
⊢ ((𝐵 ∈ On ∧ 𝐴 = ∅) → (Lim 𝑥 → (𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑥)))) |
84 | 83 | a1dd 50 |
. . . . . 6
⊢ ((𝐵 ∈ On ∧ 𝐴 = ∅) → (Lim 𝑥 → (∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)) → (𝐴 ·𝑜
(𝐵 +𝑜
𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑥))))) |
85 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → 𝐵 ∈ On) |
86 | 62 | ancoms 469 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝐵 +𝑜 𝑥) ∈ On) |
87 | | onelon 5748 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐵 +𝑜 𝑥) ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → 𝑧 ∈ On) |
88 | 86, 87 | sylan 488 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → 𝑧 ∈ On) |
89 | | ontri1 5757 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐵 ∈ On ∧ 𝑧 ∈ On) → (𝐵 ⊆ 𝑧 ↔ ¬ 𝑧 ∈ 𝐵)) |
90 | | oawordex 7637 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐵 ∈ On ∧ 𝑧 ∈ On) → (𝐵 ⊆ 𝑧 ↔ ∃𝑣 ∈ On (𝐵 +𝑜 𝑣) = 𝑧)) |
91 | 89, 90 | bitr3d 270 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 ∈ On ∧ 𝑧 ∈ On) → (¬ 𝑧 ∈ 𝐵 ↔ ∃𝑣 ∈ On (𝐵 +𝑜 𝑣) = 𝑧)) |
92 | 85, 88, 91 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → (¬ 𝑧 ∈ 𝐵 ↔ ∃𝑣 ∈ On (𝐵 +𝑜 𝑣) = 𝑧)) |
93 | | oaord 7627 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑣 ∈ On ∧ 𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑣 ∈ 𝑥 ↔ (𝐵 +𝑜 𝑣) ∈ (𝐵 +𝑜 𝑥))) |
94 | 93 | 3expb 1266 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑣 ∈ On ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → (𝑣 ∈ 𝑥 ↔ (𝐵 +𝑜 𝑣) ∈ (𝐵 +𝑜 𝑥))) |
95 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐵 +𝑜 𝑣) = 𝑧 → ((𝐵 +𝑜 𝑣) ∈ (𝐵 +𝑜 𝑥) ↔ 𝑧 ∈ (𝐵 +𝑜 𝑥))) |
96 | 94, 95 | sylan9bb 736 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑣 ∈ On ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ (𝐵 +𝑜 𝑣) = 𝑧) → (𝑣 ∈ 𝑥 ↔ 𝑧 ∈ (𝐵 +𝑜 𝑥))) |
97 | | iba 524 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐵 +𝑜 𝑣) = 𝑧 → (𝑣 ∈ 𝑥 ↔ (𝑣 ∈ 𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧))) |
98 | 97 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑣 ∈ On ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ (𝐵 +𝑜 𝑣) = 𝑧) → (𝑣 ∈ 𝑥 ↔ (𝑣 ∈ 𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧))) |
99 | 96, 98 | bitr3d 270 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑣 ∈ On ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ (𝐵 +𝑜 𝑣) = 𝑧) → (𝑧 ∈ (𝐵 +𝑜 𝑥) ↔ (𝑣 ∈ 𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧))) |
100 | 99 | an32s 846 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑣 ∈ On ∧ (𝐵 +𝑜 𝑣) = 𝑧) ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → (𝑧 ∈ (𝐵 +𝑜 𝑥) ↔ (𝑣 ∈ 𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧))) |
101 | 100 | biimpcd 239 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 ∈ (𝐵 +𝑜 𝑥) → (((𝑣 ∈ On ∧ (𝐵 +𝑜 𝑣) = 𝑧) ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → (𝑣 ∈ 𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧))) |
102 | 101 | exp4c 636 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ (𝐵 +𝑜 𝑥) → (𝑣 ∈ On → ((𝐵 +𝑜 𝑣) = 𝑧 → ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑣 ∈ 𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧))))) |
103 | 102 | com4r 94 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑧 ∈ (𝐵 +𝑜 𝑥) → (𝑣 ∈ On → ((𝐵 +𝑜 𝑣) = 𝑧 → (𝑣 ∈ 𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧))))) |
104 | 103 | imp 445 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → (𝑣 ∈ On → ((𝐵 +𝑜 𝑣) = 𝑧 → (𝑣 ∈ 𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧)))) |
105 | 104 | reximdvai 3015 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → (∃𝑣 ∈ On (𝐵 +𝑜 𝑣) = 𝑧 → ∃𝑣 ∈ On (𝑣 ∈ 𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧))) |
106 | 92, 105 | sylbid 230 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → (¬ 𝑧 ∈ 𝐵 → ∃𝑣 ∈ On (𝑣 ∈ 𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧))) |
107 | 106 | orrd 393 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → (𝑧 ∈ 𝐵 ∨ ∃𝑣 ∈ On (𝑣 ∈ 𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧))) |
108 | 61, 107 | sylanl1 682 |
. . . . . . . . . . . . . . . 16
⊢ (((Lim
𝑥 ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → (𝑧 ∈ 𝐵 ∨ ∃𝑣 ∈ On (𝑣 ∈ 𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧))) |
109 | 108 | adantlrl 756 |
. . . . . . . . . . . . . . 15
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → (𝑧 ∈ 𝐵 ∨ ∃𝑣 ∈ On (𝑣 ∈ 𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧))) |
110 | 109 | adantlr 751 |
. . . . . . . . . . . . . 14
⊢ ((((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)))) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → (𝑧 ∈ 𝐵 ∨ ∃𝑣 ∈ On (𝑣 ∈ 𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧))) |
111 | | 0ellim 5787 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (Lim
𝑥 → ∅ ∈
𝑥) |
112 | | om00el 7656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (∅
∈ (𝐴
·𝑜 𝑥) ↔ (∅ ∈ 𝐴 ∧ ∅ ∈ 𝑥))) |
113 | 112 | biimprd 238 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → ((∅
∈ 𝐴 ∧ ∅
∈ 𝑥) → ∅
∈ (𝐴
·𝑜 𝑥))) |
114 | 111, 113 | sylan2i 687 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → ((∅
∈ 𝐴 ∧ Lim 𝑥) → ∅ ∈ (𝐴 ·𝑜
𝑥))) |
115 | 61, 114 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ On ∧ Lim 𝑥) → ((∅ ∈ 𝐴 ∧ Lim 𝑥) → ∅ ∈ (𝐴 ·𝑜 𝑥))) |
116 | 115 | exp4b 632 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 ∈ On → (Lim 𝑥 → (∅ ∈ 𝐴 → (Lim 𝑥 → ∅ ∈ (𝐴 ·𝑜 𝑥))))) |
117 | 116 | com4r 94 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (Lim
𝑥 → (𝐴 ∈ On → (Lim 𝑥 → (∅ ∈ 𝐴 → ∅ ∈ (𝐴 ·𝑜 𝑥))))) |
118 | 117 | pm2.43a 54 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (Lim
𝑥 → (𝐴 ∈ On → (∅ ∈ 𝐴 → ∅ ∈ (𝐴 ·𝑜
𝑥)))) |
119 | 118 | imp31 448 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((Lim
𝑥 ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴 ·𝑜
𝑥)) |
120 | 119 | a1d 25 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((Lim
𝑥 ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (𝑧 ∈ 𝐵 → ∅ ∈ (𝐴 ·𝑜 𝑥))) |
121 | 120 | adantlrr 757 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∅ ∈ 𝐴) → (𝑧 ∈ 𝐵 → ∅ ∈ (𝐴 ·𝑜 𝑥))) |
122 | | omordi 7646 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐵 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈
𝐴) → (𝑧 ∈ 𝐵 → (𝐴 ·𝑜 𝑧) ∈ (𝐴 ·𝑜 𝐵))) |
123 | 122 | ancom1s 847 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈
𝐴) → (𝑧 ∈ 𝐵 → (𝐴 ·𝑜 𝑧) ∈ (𝐴 ·𝑜 𝐵))) |
124 | | onelss 5766 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ·𝑜
𝐵) ∈ On → ((𝐴 ·𝑜
𝑧) ∈ (𝐴 ·𝑜
𝐵) → (𝐴 ·𝑜
𝑧) ⊆ (𝐴 ·𝑜
𝐵))) |
125 | 22 | sseq2d 3633 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ·𝑜
𝐵) ∈ On → ((𝐴 ·𝑜
𝑧) ⊆ ((𝐴 ·𝑜
𝐵) +𝑜
∅) ↔ (𝐴
·𝑜 𝑧) ⊆ (𝐴 ·𝑜 𝐵))) |
126 | 124, 125 | sylibrd 249 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ·𝑜
𝐵) ∈ On → ((𝐴 ·𝑜
𝑧) ∈ (𝐴 ·𝑜
𝐵) → (𝐴 ·𝑜
𝑧) ⊆ ((𝐴 ·𝑜
𝐵) +𝑜
∅))) |
127 | 21, 126 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·𝑜
𝑧) ∈ (𝐴 ·𝑜
𝐵) → (𝐴 ·𝑜
𝑧) ⊆ ((𝐴 ·𝑜
𝐵) +𝑜
∅))) |
128 | 127 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈
𝐴) → ((𝐴 ·𝑜
𝑧) ∈ (𝐴 ·𝑜
𝐵) → (𝐴 ·𝑜
𝑧) ⊆ ((𝐴 ·𝑜
𝐵) +𝑜
∅))) |
129 | 123, 128 | syld 47 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈
𝐴) → (𝑧 ∈ 𝐵 → (𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜
∅))) |
130 | 129 | adantll 750 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∅ ∈ 𝐴) → (𝑧 ∈ 𝐵 → (𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜
∅))) |
131 | 121, 130 | jcad 555 |
. . . . . . . . . . . . . . . . . 18
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∅ ∈ 𝐴) → (𝑧 ∈ 𝐵 → (∅ ∈ (𝐴 ·𝑜 𝑥) ∧ (𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜
∅)))) |
132 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = ∅ → ((𝐴 ·𝑜
𝐵) +𝑜
𝑤) = ((𝐴 ·𝑜 𝐵) +𝑜
∅)) |
133 | 132 | sseq2d 3633 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = ∅ → ((𝐴 ·𝑜
𝑧) ⊆ ((𝐴 ·𝑜
𝐵) +𝑜
𝑤) ↔ (𝐴 ·𝑜
𝑧) ⊆ ((𝐴 ·𝑜
𝐵) +𝑜
∅))) |
134 | 133 | rspcev 3309 |
. . . . . . . . . . . . . . . . . 18
⊢ ((∅
∈ (𝐴
·𝑜 𝑥) ∧ (𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜
∅)) → ∃𝑤
∈ (𝐴
·𝑜 𝑥)(𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 𝑤)) |
135 | 131, 134 | syl6 35 |
. . . . . . . . . . . . . . . . 17
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∅ ∈ 𝐴) → (𝑧 ∈ 𝐵 → ∃𝑤 ∈ (𝐴 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 𝑤))) |
136 | 135 | adantrr 753 |
. . . . . . . . . . . . . . . 16
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)))) → (𝑧 ∈ 𝐵 → ∃𝑤 ∈ (𝐴 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 𝑤))) |
137 | | omordi 7646 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈
𝐴) → (𝑣 ∈ 𝑥 → (𝐴 ·𝑜 𝑣) ∈ (𝐴 ·𝑜 𝑥))) |
138 | 61, 137 | sylanl1 682 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((Lim
𝑥 ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (𝑣 ∈ 𝑥 → (𝐴 ·𝑜 𝑣) ∈ (𝐴 ·𝑜 𝑥))) |
139 | 138 | adantrd 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((Lim
𝑥 ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → ((𝑣 ∈ 𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧) → (𝐴 ·𝑜 𝑣) ∈ (𝐴 ·𝑜 𝑥))) |
140 | 139 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((Lim
𝑥 ∧ 𝐴 ∈ On) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)))) → ((𝑣 ∈ 𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧) → (𝐴 ·𝑜 𝑣) ∈ (𝐴 ·𝑜 𝑥))) |
141 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 = 𝑣 → (𝐵 +𝑜 𝑦) = (𝐵 +𝑜 𝑣)) |
142 | 141 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 = 𝑣 → (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = (𝐴 ·𝑜 (𝐵 +𝑜 𝑣))) |
143 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 = 𝑣 → (𝐴 ·𝑜 𝑦) = (𝐴 ·𝑜 𝑣)) |
144 | 143 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 = 𝑣 → ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑣))) |
145 | 142, 144 | eqeq12d 2637 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = 𝑣 → ((𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)) ↔ (𝐴 ·𝑜
(𝐵 +𝑜
𝑣)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑣)))) |
146 | 145 | rspccv 3306 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∀𝑦 ∈
𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)) → (𝑣 ∈ 𝑥 → (𝐴 ·𝑜 (𝐵 +𝑜 𝑣)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑣)))) |
147 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐵 +𝑜 𝑣) = 𝑧 → (𝐴 ·𝑜 (𝐵 +𝑜 𝑣)) = (𝐴 ·𝑜 𝑧)) |
148 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 ·𝑜
(𝐵 +𝑜
𝑣)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑣)) → ((𝐴 ·𝑜
(𝐵 +𝑜
𝑣)) = (𝐴 ·𝑜 𝑧) ↔ ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑣)) = (𝐴 ·𝑜 𝑧))) |
149 | 147, 148 | syl5ib 234 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ·𝑜
(𝐵 +𝑜
𝑣)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑣)) → ((𝐵 +𝑜 𝑣) = 𝑧 → ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑣)) = (𝐴 ·𝑜 𝑧))) |
150 | | eqimss2 3658 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐴 ·𝑜
𝐵) +𝑜
(𝐴
·𝑜 𝑣)) = (𝐴 ·𝑜 𝑧) → (𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑣))) |
151 | 149, 150 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ·𝑜
(𝐵 +𝑜
𝑣)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑣)) → ((𝐵 +𝑜 𝑣) = 𝑧 → (𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑣)))) |
152 | 151 | imim2i 16 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑣 ∈ 𝑥 → (𝐴 ·𝑜 (𝐵 +𝑜 𝑣)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑣))) → (𝑣 ∈ 𝑥 → ((𝐵 +𝑜 𝑣) = 𝑧 → (𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑣))))) |
153 | 152 | impd 447 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑣 ∈ 𝑥 → (𝐴 ·𝑜 (𝐵 +𝑜 𝑣)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑣))) → ((𝑣 ∈ 𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧) → (𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑣)))) |
154 | 146, 153 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑦 ∈
𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)) → ((𝑣 ∈ 𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧) → (𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑣)))) |
155 | 154 | ad2antll 765 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((Lim
𝑥 ∧ 𝐴 ∈ On) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)))) → ((𝑣 ∈ 𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧) → (𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑣)))) |
156 | 140, 155 | jcad 555 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((Lim
𝑥 ∧ 𝐴 ∈ On) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)))) → ((𝑣 ∈ 𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧) → ((𝐴 ·𝑜 𝑣) ∈ (𝐴 ·𝑜 𝑥) ∧ (𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑣))))) |
157 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = (𝐴 ·𝑜 𝑣) → ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑣))) |
158 | 157 | sseq2d 3633 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = (𝐴 ·𝑜 𝑣) → ((𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ↔ (𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑣)))) |
159 | 158 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ·𝑜
𝑣) ∈ (𝐴 ·𝑜
𝑥) ∧ (𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑣))) → ∃𝑤 ∈ (𝐴 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 𝑤)) |
160 | 156, 159 | syl6 35 |
. . . . . . . . . . . . . . . . . 18
⊢ (((Lim
𝑥 ∧ 𝐴 ∈ On) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)))) → ((𝑣 ∈ 𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧) → ∃𝑤 ∈ (𝐴 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 𝑤))) |
161 | 160 | rexlimdvw 3034 |
. . . . . . . . . . . . . . . . 17
⊢ (((Lim
𝑥 ∧ 𝐴 ∈ On) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)))) → (∃𝑣 ∈ On (𝑣 ∈ 𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧) → ∃𝑤 ∈ (𝐴 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 𝑤))) |
162 | 161 | adantlrr 757 |
. . . . . . . . . . . . . . . 16
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)))) → (∃𝑣 ∈ On (𝑣 ∈ 𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧) → ∃𝑤 ∈ (𝐴 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 𝑤))) |
163 | 136, 162 | jaod 395 |
. . . . . . . . . . . . . . 15
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)))) → ((𝑧 ∈ 𝐵 ∨ ∃𝑣 ∈ On (𝑣 ∈ 𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧)) → ∃𝑤 ∈ (𝐴 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 𝑤))) |
164 | 163 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)))) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → ((𝑧 ∈ 𝐵 ∨ ∃𝑣 ∈ On (𝑣 ∈ 𝑥 ∧ (𝐵 +𝑜 𝑣) = 𝑧)) → ∃𝑤 ∈ (𝐴 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 𝑤))) |
165 | 110, 164 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)))) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → ∃𝑤 ∈ (𝐴 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 𝑤)) |
166 | 165 | ralrimiva 2966 |
. . . . . . . . . . . 12
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)))) → ∀𝑧 ∈ (𝐵 +𝑜 𝑥)∃𝑤 ∈ (𝐴 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 𝑤)) |
167 | | iunss2 4565 |
. . . . . . . . . . . 12
⊢
(∀𝑧 ∈
(𝐵 +𝑜
𝑥)∃𝑤 ∈ (𝐴 ·𝑜 𝑥)(𝐴 ·𝑜 𝑧) ⊆ ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) → ∪ 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 ·𝑜 𝑧) ⊆ ∪ 𝑤 ∈ (𝐴 ·𝑜 𝑥)((𝐴 ·𝑜 𝐵) +𝑜 𝑤)) |
168 | 166, 167 | syl 17 |
. . . . . . . . . . 11
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)))) → ∪ 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 ·𝑜 𝑧) ⊆ ∪ 𝑤 ∈ (𝐴 ·𝑜 𝑥)((𝐴 ·𝑜 𝐵) +𝑜 𝑤)) |
169 | | omordlim 7657 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ 𝑤 ∈ (𝐴 ·𝑜 𝑥)) → ∃𝑣 ∈ 𝑥 𝑤 ∈ (𝐴 ·𝑜 𝑣)) |
170 | 169 | ex 450 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → (𝑤 ∈ (𝐴 ·𝑜 𝑥) → ∃𝑣 ∈ 𝑥 𝑤 ∈ (𝐴 ·𝑜 𝑣))) |
171 | 59, 170 | mpanr1 719 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ On ∧ Lim 𝑥) → (𝑤 ∈ (𝐴 ·𝑜 𝑥) → ∃𝑣 ∈ 𝑥 𝑤 ∈ (𝐴 ·𝑜 𝑣))) |
172 | 171 | ancoms 469 |
. . . . . . . . . . . . . . . . . 18
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ On) → (𝑤 ∈ (𝐴 ·𝑜 𝑥) → ∃𝑣 ∈ 𝑥 𝑤 ∈ (𝐴 ·𝑜 𝑣))) |
173 | 172 | imp 445 |
. . . . . . . . . . . . . . . . 17
⊢ (((Lim
𝑥 ∧ 𝐴 ∈ On) ∧ 𝑤 ∈ (𝐴 ·𝑜 𝑥)) → ∃𝑣 ∈ 𝑥 𝑤 ∈ (𝐴 ·𝑜 𝑣)) |
174 | 173 | adantlrr 757 |
. . . . . . . . . . . . . . . 16
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑤 ∈ (𝐴 ·𝑜 𝑥)) → ∃𝑣 ∈ 𝑥 𝑤 ∈ (𝐴 ·𝑜 𝑣)) |
175 | 174 | adantlr 751 |
. . . . . . . . . . . . . . 15
⊢ ((((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦))) ∧ 𝑤 ∈ (𝐴 ·𝑜 𝑥)) → ∃𝑣 ∈ 𝑥 𝑤 ∈ (𝐴 ·𝑜 𝑣)) |
176 | | oaordi 7626 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑣 ∈ 𝑥 → (𝐵 +𝑜 𝑣) ∈ (𝐵 +𝑜 𝑥))) |
177 | 61, 176 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((Lim
𝑥 ∧ 𝐵 ∈ On) → (𝑣 ∈ 𝑥 → (𝐵 +𝑜 𝑣) ∈ (𝐵 +𝑜 𝑥))) |
178 | 177 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((Lim
𝑥 ∧ 𝐵 ∈ On) ∧ 𝑣 ∈ 𝑥) → (𝐵 +𝑜 𝑣) ∈ (𝐵 +𝑜 𝑥)) |
179 | 178 | adantlrl 756 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑣 ∈ 𝑥) → (𝐵 +𝑜 𝑣) ∈ (𝐵 +𝑜 𝑥)) |
180 | 179 | a1d 25 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑣 ∈ 𝑥) → (𝑤 ∈ (𝐴 ·𝑜 𝑣) → (𝐵 +𝑜 𝑣) ∈ (𝐵 +𝑜 𝑥))) |
181 | 180 | adantlr 751 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦))) ∧ 𝑣 ∈ 𝑥) → (𝑤 ∈ (𝐴 ·𝑜 𝑣) → (𝐵 +𝑜 𝑣) ∈ (𝐵 +𝑜 𝑥))) |
182 | | limord 5784 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (Lim
𝑥 → Ord 𝑥) |
183 | | ordelon 5747 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((Ord
𝑥 ∧ 𝑣 ∈ 𝑥) → 𝑣 ∈ On) |
184 | 182, 183 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((Lim
𝑥 ∧ 𝑣 ∈ 𝑥) → 𝑣 ∈ On) |
185 | | omcl 7616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐴 ∈ On ∧ 𝑣 ∈ On) → (𝐴 ·𝑜
𝑣) ∈
On) |
186 | 185 | ancoms 469 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑣 ∈ On ∧ 𝐴 ∈ On) → (𝐴 ·𝑜
𝑣) ∈
On) |
187 | 186 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑣 ∈ On ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·𝑜
𝑣) ∈
On) |
188 | 21 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑣 ∈ On ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·𝑜
𝐵) ∈
On) |
189 | | oaordi 7626 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐴 ·𝑜
𝑣) ∈ On ∧ (𝐴 ·𝑜
𝐵) ∈ On) → (𝑤 ∈ (𝐴 ·𝑜 𝑣) → ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ∈ ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑣)))) |
190 | 187, 188,
189 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑣 ∈ On ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → (𝑤 ∈ (𝐴 ·𝑜 𝑣) → ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ∈ ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑣)))) |
191 | 184, 190 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((Lim
𝑥 ∧ 𝑣 ∈ 𝑥) ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → (𝑤 ∈ (𝐴 ·𝑜 𝑣) → ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ∈ ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑣)))) |
192 | 191 | an32s 846 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑣 ∈ 𝑥) → (𝑤 ∈ (𝐴 ·𝑜 𝑣) → ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ∈ ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑣)))) |
193 | 192 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦))) ∧ 𝑣 ∈ 𝑥) → (𝑤 ∈ (𝐴 ·𝑜 𝑣) → ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ∈ ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑣)))) |
194 | 145 | rspccva 3308 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((∀𝑦 ∈
𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)) ∧ 𝑣 ∈ 𝑥) → (𝐴 ·𝑜 (𝐵 +𝑜 𝑣)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑣))) |
195 | 194 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((∀𝑦 ∈
𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)) ∧ 𝑣 ∈ 𝑥) → (((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ∈ (𝐴 ·𝑜 (𝐵 +𝑜 𝑣)) ↔ ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ∈ ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑣)))) |
196 | 195 | adantll 750 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦))) ∧ 𝑣 ∈ 𝑥) → (((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ∈ (𝐴 ·𝑜 (𝐵 +𝑜 𝑣)) ↔ ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ∈ ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑣)))) |
197 | 193, 196 | sylibrd 249 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦))) ∧ 𝑣 ∈ 𝑥) → (𝑤 ∈ (𝐴 ·𝑜 𝑣) → ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ∈ (𝐴 ·𝑜 (𝐵 +𝑜 𝑣)))) |
198 | | oacl 7615 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐵 ∈ On ∧ 𝑣 ∈ On) → (𝐵 +𝑜 𝑣) ∈ On) |
199 | 198 | ancoms 469 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑣 ∈ On ∧ 𝐵 ∈ On) → (𝐵 +𝑜 𝑣) ∈ On) |
200 | | omcl 7616 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 ∈ On ∧ (𝐵 +𝑜 𝑣) ∈ On) → (𝐴 ·𝑜
(𝐵 +𝑜
𝑣)) ∈
On) |
201 | 199, 200 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ On ∧ (𝑣 ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·𝑜
(𝐵 +𝑜
𝑣)) ∈
On) |
202 | 201 | an12s 843 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑣 ∈ On ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·𝑜
(𝐵 +𝑜
𝑣)) ∈
On) |
203 | 184, 202 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((Lim
𝑥 ∧ 𝑣 ∈ 𝑥) ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·𝑜 (𝐵 +𝑜 𝑣)) ∈ On) |
204 | 203 | an32s 846 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑣 ∈ 𝑥) → (𝐴 ·𝑜 (𝐵 +𝑜 𝑣)) ∈ On) |
205 | | onelss 5766 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ·𝑜
(𝐵 +𝑜
𝑣)) ∈ On →
(((𝐴
·𝑜 𝐵) +𝑜 𝑤) ∈ (𝐴 ·𝑜 (𝐵 +𝑜 𝑣)) → ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ⊆ (𝐴 ·𝑜 (𝐵 +𝑜 𝑣)))) |
206 | 204, 205 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑣 ∈ 𝑥) → (((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ∈ (𝐴 ·𝑜 (𝐵 +𝑜 𝑣)) → ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ⊆ (𝐴 ·𝑜 (𝐵 +𝑜 𝑣)))) |
207 | 206 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦))) ∧ 𝑣 ∈ 𝑥) → (((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ∈ (𝐴 ·𝑜 (𝐵 +𝑜 𝑣)) → ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ⊆ (𝐴 ·𝑜 (𝐵 +𝑜 𝑣)))) |
208 | 197, 207 | syld 47 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦))) ∧ 𝑣 ∈ 𝑥) → (𝑤 ∈ (𝐴 ·𝑜 𝑣) → ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ⊆ (𝐴 ·𝑜 (𝐵 +𝑜 𝑣)))) |
209 | 181, 208 | jcad 555 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦))) ∧ 𝑣 ∈ 𝑥) → (𝑤 ∈ (𝐴 ·𝑜 𝑣) → ((𝐵 +𝑜 𝑣) ∈ (𝐵 +𝑜 𝑥) ∧ ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ⊆ (𝐴 ·𝑜 (𝐵 +𝑜 𝑣))))) |
210 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = (𝐵 +𝑜 𝑣) → (𝐴 ·𝑜 𝑧) = (𝐴 ·𝑜 (𝐵 +𝑜 𝑣))) |
211 | 210 | sseq2d 3633 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = (𝐵 +𝑜 𝑣) → (((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ⊆ (𝐴 ·𝑜 𝑧) ↔ ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ⊆ (𝐴 ·𝑜 (𝐵 +𝑜 𝑣)))) |
212 | 211 | rspcev 3309 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐵 +𝑜 𝑣) ∈ (𝐵 +𝑜 𝑥) ∧ ((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ⊆ (𝐴 ·𝑜 (𝐵 +𝑜 𝑣))) → ∃𝑧 ∈ (𝐵 +𝑜 𝑥)((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ⊆ (𝐴 ·𝑜 𝑧)) |
213 | 209, 212 | syl6 35 |
. . . . . . . . . . . . . . . . 17
⊢ ((((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦))) ∧ 𝑣 ∈ 𝑥) → (𝑤 ∈ (𝐴 ·𝑜 𝑣) → ∃𝑧 ∈ (𝐵 +𝑜 𝑥)((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ⊆ (𝐴 ·𝑜 𝑧))) |
214 | 213 | rexlimdva 3031 |
. . . . . . . . . . . . . . . 16
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦))) → (∃𝑣 ∈ 𝑥 𝑤 ∈ (𝐴 ·𝑜 𝑣) → ∃𝑧 ∈ (𝐵 +𝑜 𝑥)((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ⊆ (𝐴 ·𝑜 𝑧))) |
215 | 214 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦))) ∧ 𝑤 ∈ (𝐴 ·𝑜 𝑥)) → (∃𝑣 ∈ 𝑥 𝑤 ∈ (𝐴 ·𝑜 𝑣) → ∃𝑧 ∈ (𝐵 +𝑜 𝑥)((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ⊆ (𝐴 ·𝑜 𝑧))) |
216 | 175, 215 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ ((((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦))) ∧ 𝑤 ∈ (𝐴 ·𝑜 𝑥)) → ∃𝑧 ∈ (𝐵 +𝑜 𝑥)((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ⊆ (𝐴 ·𝑜 𝑧)) |
217 | 216 | ralrimiva 2966 |
. . . . . . . . . . . . 13
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦))) → ∀𝑤 ∈ (𝐴 ·𝑜 𝑥)∃𝑧 ∈ (𝐵 +𝑜 𝑥)((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ⊆ (𝐴 ·𝑜 𝑧)) |
218 | | iunss2 4565 |
. . . . . . . . . . . . 13
⊢
(∀𝑤 ∈
(𝐴
·𝑜 𝑥)∃𝑧 ∈ (𝐵 +𝑜 𝑥)((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ⊆ (𝐴 ·𝑜 𝑧) → ∪ 𝑤 ∈ (𝐴 ·𝑜 𝑥)((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ⊆ ∪ 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 ·𝑜 𝑧)) |
219 | 217, 218 | syl 17 |
. . . . . . . . . . . 12
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦))) → ∪ 𝑤 ∈ (𝐴 ·𝑜 𝑥)((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ⊆ ∪ 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 ·𝑜 𝑧)) |
220 | 219 | adantrl 752 |
. . . . . . . . . . 11
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)))) → ∪ 𝑤 ∈ (𝐴 ·𝑜 𝑥)((𝐴 ·𝑜 𝐵) +𝑜 𝑤) ⊆ ∪ 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 ·𝑜 𝑧)) |
221 | 168, 220 | eqssd 3620 |
. . . . . . . . . 10
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)))) → ∪ 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 ·𝑜 𝑧) = ∪ 𝑤 ∈ (𝐴 ·𝑜 𝑥)((𝐴 ·𝑜 𝐵) +𝑜 𝑤)) |
222 | | oalimcl 7640 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → Lim (𝐵 +𝑜 𝑥)) |
223 | 59, 222 | mpanr1 719 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ On ∧ Lim 𝑥) → Lim (𝐵 +𝑜 𝑥)) |
224 | 223 | ancoms 469 |
. . . . . . . . . . . . . 14
⊢ ((Lim
𝑥 ∧ 𝐵 ∈ On) → Lim (𝐵 +𝑜 𝑥)) |
225 | 224 | anim2i 593 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ On ∧ (Lim 𝑥 ∧ 𝐵 ∈ On)) → (𝐴 ∈ On ∧ Lim (𝐵 +𝑜 𝑥))) |
226 | 225 | an12s 843 |
. . . . . . . . . . . 12
⊢ ((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ∈ On ∧ Lim (𝐵 +𝑜 𝑥))) |
227 | | ovex 6678 |
. . . . . . . . . . . . 13
⊢ (𝐵 +𝑜 𝑥) ∈ V |
228 | | omlim 7613 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ On ∧ ((𝐵 +𝑜 𝑥) ∈ V ∧ Lim (𝐵 +𝑜 𝑥))) → (𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = ∪ 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 ·𝑜 𝑧)) |
229 | 227, 228 | mpanr1 719 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ Lim (𝐵 +𝑜 𝑥)) → (𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = ∪ 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 ·𝑜 𝑧)) |
230 | 226, 229 | syl 17 |
. . . . . . . . . . 11
⊢ ((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·𝑜 (𝐵 +𝑜 𝑥)) = ∪ 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 ·𝑜 𝑧)) |
231 | 230 | adantr 481 |
. . . . . . . . . 10
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)))) → (𝐴 ·𝑜
(𝐵 +𝑜
𝑥)) = ∪ 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 ·𝑜 𝑧)) |
232 | 21 | ad2antlr 763 |
. . . . . . . . . . . 12
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∅ ∈ 𝐴) → (𝐴 ·𝑜 𝐵) ∈ On) |
233 | 59 | jctl 564 |
. . . . . . . . . . . . . . . . 17
⊢ (Lim
𝑥 → (𝑥 ∈ V ∧ Lim 𝑥)) |
234 | 233 | anim2i 593 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ On ∧ Lim 𝑥) → (𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥))) |
235 | 234 | ancoms 469 |
. . . . . . . . . . . . . . 15
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ On) → (𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥))) |
236 | | omlimcl 7658 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ ∅ ∈ 𝐴) → Lim (𝐴 ·𝑜 𝑥)) |
237 | 235, 236 | sylan 488 |
. . . . . . . . . . . . . 14
⊢ (((Lim
𝑥 ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → Lim (𝐴 ·𝑜 𝑥)) |
238 | 237 | adantlrr 757 |
. . . . . . . . . . . . 13
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∅ ∈ 𝐴) → Lim (𝐴 ·𝑜 𝑥)) |
239 | | ovex 6678 |
. . . . . . . . . . . . 13
⊢ (𝐴 ·𝑜
𝑥) ∈
V |
240 | 238, 239 | jctil 560 |
. . . . . . . . . . . 12
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∅ ∈ 𝐴) → ((𝐴 ·𝑜 𝑥) ∈ V ∧ Lim (𝐴 ·𝑜
𝑥))) |
241 | | oalim 7612 |
. . . . . . . . . . . 12
⊢ (((𝐴 ·𝑜
𝐵) ∈ On ∧ ((𝐴 ·𝑜
𝑥) ∈ V ∧ Lim
(𝐴
·𝑜 𝑥))) → ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑥)) = ∪ 𝑤 ∈ (𝐴 ·𝑜 𝑥)((𝐴 ·𝑜 𝐵) +𝑜 𝑤)) |
242 | 232, 240,
241 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∅ ∈ 𝐴) → ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑥)) = ∪ 𝑤 ∈ (𝐴 ·𝑜 𝑥)((𝐴 ·𝑜 𝐵) +𝑜 𝑤)) |
243 | 242 | adantrr 753 |
. . . . . . . . . 10
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)))) → ((𝐴 ·𝑜
𝐵) +𝑜
(𝐴
·𝑜 𝑥)) = ∪
𝑤 ∈ (𝐴 ·𝑜 𝑥)((𝐴 ·𝑜 𝐵) +𝑜 𝑤)) |
244 | 221, 231,
243 | 3eqtr4d 2666 |
. . . . . . . . 9
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)))) → (𝐴 ·𝑜
(𝐵 +𝑜
𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑥))) |
245 | 244 | exp43 640 |
. . . . . . . 8
⊢ (Lim
𝑥 → ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∅
∈ 𝐴 →
(∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)) → (𝐴 ·𝑜
(𝐵 +𝑜
𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑥)))))) |
246 | 245 | com3l 89 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∅
∈ 𝐴 → (Lim 𝑥 → (∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)) → (𝐴 ·𝑜
(𝐵 +𝑜
𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑥)))))) |
247 | 246 | imp 445 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈
𝐴) → (Lim 𝑥 → (∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)) → (𝐴 ·𝑜
(𝐵 +𝑜
𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑥))))) |
248 | 84, 247 | oe0lem 7593 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (Lim 𝑥 → (∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)) → (𝐴 ·𝑜
(𝐵 +𝑜
𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑥))))) |
249 | 248 | com12 32 |
. . . 4
⊢ (Lim
𝑥 → ((𝐴 ∈ On ∧ 𝐵 ∈ On) →
(∀𝑦 ∈ 𝑥 (𝐴 ·𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑦)) → (𝐴 ·𝑜
(𝐵 +𝑜
𝑥)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝑥))))) |
250 | 5, 10, 15, 20, 30, 58, 249 | tfinds3 7064 |
. . 3
⊢ (𝐶 ∈ On → ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·𝑜
(𝐵 +𝑜
𝐶)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝐶)))) |
251 | 250 | expdcom 455 |
. 2
⊢ (𝐴 ∈ On → (𝐵 ∈ On → (𝐶 ∈ On → (𝐴 ·𝑜
(𝐵 +𝑜
𝐶)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝐶))))) |
252 | 251 | 3imp 1256 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ·𝑜
(𝐵 +𝑜
𝐶)) = ((𝐴 ·𝑜 𝐵) +𝑜 (𝐴 ·𝑜
𝐶))) |