Step | Hyp | Ref
| Expression |
1 | | oveq2 6557 |
. . . 4
⊢ (𝑥 = ∅ → (𝐵 +𝑜 𝑥) = (𝐵 +𝑜
∅)) |
2 | 1 | oveq2d 6565 |
. . 3
⊢ (𝑥 = ∅ → (𝐴 ↑𝑜
(𝐵 +𝑜
𝑥)) = (𝐴 ↑𝑜 (𝐵 +𝑜
∅))) |
3 | | oveq2 6557 |
. . . 4
⊢ (𝑥 = ∅ → (𝐴 ↑𝑜
𝑥) = (𝐴 ↑𝑜
∅)) |
4 | 3 | oveq2d 6565 |
. . 3
⊢ (𝑥 = ∅ → ((𝐴 ↑𝑜
𝐵)
·𝑜 (𝐴 ↑𝑜 𝑥)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 ∅))) |
5 | 2, 4 | eqeq12d 2625 |
. 2
⊢ (𝑥 = ∅ → ((𝐴 ↑𝑜
(𝐵 +𝑜
𝑥)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝑥)) ↔ (𝐴 ↑𝑜 (𝐵 +𝑜 ∅))
= ((𝐴
↑𝑜 𝐵) ·𝑜 (𝐴 ↑𝑜
∅)))) |
6 | | oveq2 6557 |
. . . 4
⊢ (𝑥 = 𝑦 → (𝐵 +𝑜 𝑥) = (𝐵 +𝑜 𝑦)) |
7 | 6 | oveq2d 6565 |
. . 3
⊢ (𝑥 = 𝑦 → (𝐴 ↑𝑜 (𝐵 +𝑜 𝑥)) = (𝐴 ↑𝑜 (𝐵 +𝑜 𝑦))) |
8 | | oveq2 6557 |
. . . 4
⊢ (𝑥 = 𝑦 → (𝐴 ↑𝑜 𝑥) = (𝐴 ↑𝑜 𝑦)) |
9 | 8 | oveq2d 6565 |
. . 3
⊢ (𝑥 = 𝑦 → ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝑥)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝑦))) |
10 | 7, 9 | eqeq12d 2625 |
. 2
⊢ (𝑥 = 𝑦 → ((𝐴 ↑𝑜 (𝐵 +𝑜 𝑥)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝑥)) ↔ (𝐴 ↑𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝑦)))) |
11 | | oveq2 6557 |
. . . 4
⊢ (𝑥 = suc 𝑦 → (𝐵 +𝑜 𝑥) = (𝐵 +𝑜 suc 𝑦)) |
12 | 11 | oveq2d 6565 |
. . 3
⊢ (𝑥 = suc 𝑦 → (𝐴 ↑𝑜 (𝐵 +𝑜 𝑥)) = (𝐴 ↑𝑜 (𝐵 +𝑜 suc 𝑦))) |
13 | | oveq2 6557 |
. . . 4
⊢ (𝑥 = suc 𝑦 → (𝐴 ↑𝑜 𝑥) = (𝐴 ↑𝑜 suc 𝑦)) |
14 | 13 | oveq2d 6565 |
. . 3
⊢ (𝑥 = suc 𝑦 → ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝑥)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 suc 𝑦))) |
15 | 12, 14 | eqeq12d 2625 |
. 2
⊢ (𝑥 = suc 𝑦 → ((𝐴 ↑𝑜 (𝐵 +𝑜 𝑥)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝑥)) ↔ (𝐴 ↑𝑜 (𝐵 +𝑜 suc 𝑦)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 suc 𝑦)))) |
16 | | oveq2 6557 |
. . . 4
⊢ (𝑥 = 𝐶 → (𝐵 +𝑜 𝑥) = (𝐵 +𝑜 𝐶)) |
17 | 16 | oveq2d 6565 |
. . 3
⊢ (𝑥 = 𝐶 → (𝐴 ↑𝑜 (𝐵 +𝑜 𝑥)) = (𝐴 ↑𝑜 (𝐵 +𝑜 𝐶))) |
18 | | oveq2 6557 |
. . . 4
⊢ (𝑥 = 𝐶 → (𝐴 ↑𝑜 𝑥) = (𝐴 ↑𝑜 𝐶)) |
19 | 18 | oveq2d 6565 |
. . 3
⊢ (𝑥 = 𝐶 → ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝑥)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝐶))) |
20 | 17, 19 | eqeq12d 2625 |
. 2
⊢ (𝑥 = 𝐶 → ((𝐴 ↑𝑜 (𝐵 +𝑜 𝑥)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝑥)) ↔ (𝐴 ↑𝑜 (𝐵 +𝑜 𝐶)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝐶)))) |
21 | | oeoalem.1 |
. . . . 5
⊢ 𝐴 ∈ On |
22 | | oeoalem.3 |
. . . . 5
⊢ 𝐵 ∈ On |
23 | | oecl 7504 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑𝑜
𝐵) ∈
On) |
24 | 21, 22, 23 | mp2an 704 |
. . . 4
⊢ (𝐴 ↑𝑜
𝐵) ∈
On |
25 | | om1 7509 |
. . . 4
⊢ ((𝐴 ↑𝑜
𝐵) ∈ On → ((𝐴 ↑𝑜
𝐵)
·𝑜 1𝑜) = (𝐴 ↑𝑜 𝐵)) |
26 | 24, 25 | ax-mp 5 |
. . 3
⊢ ((𝐴 ↑𝑜
𝐵)
·𝑜 1𝑜) = (𝐴 ↑𝑜 𝐵) |
27 | | oe0 7489 |
. . . . 5
⊢ (𝐴 ∈ On → (𝐴 ↑𝑜
∅) = 1𝑜) |
28 | 21, 27 | ax-mp 5 |
. . . 4
⊢ (𝐴 ↑𝑜
∅) = 1𝑜 |
29 | 28 | oveq2i 6560 |
. . 3
⊢ ((𝐴 ↑𝑜
𝐵)
·𝑜 (𝐴 ↑𝑜 ∅)) =
((𝐴
↑𝑜 𝐵) ·𝑜
1𝑜) |
30 | | oa0 7483 |
. . . . 5
⊢ (𝐵 ∈ On → (𝐵 +𝑜 ∅)
= 𝐵) |
31 | 22, 30 | ax-mp 5 |
. . . 4
⊢ (𝐵 +𝑜 ∅)
= 𝐵 |
32 | 31 | oveq2i 6560 |
. . 3
⊢ (𝐴 ↑𝑜
(𝐵 +𝑜
∅)) = (𝐴
↑𝑜 𝐵) |
33 | 26, 29, 32 | 3eqtr4ri 2643 |
. 2
⊢ (𝐴 ↑𝑜
(𝐵 +𝑜
∅)) = ((𝐴
↑𝑜 𝐵) ·𝑜 (𝐴 ↑𝑜
∅)) |
34 | | oasuc 7491 |
. . . . . . . 8
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 +𝑜 suc 𝑦) = suc (𝐵 +𝑜 𝑦)) |
35 | 34 | oveq2d 6565 |
. . . . . . 7
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ↑𝑜
(𝐵 +𝑜
suc 𝑦)) = (𝐴 ↑𝑜 suc
(𝐵 +𝑜
𝑦))) |
36 | | oacl 7502 |
. . . . . . . 8
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 +𝑜 𝑦) ∈ On) |
37 | | oesuc 7494 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ (𝐵 +𝑜 𝑦) ∈ On) → (𝐴 ↑𝑜 suc
(𝐵 +𝑜
𝑦)) = ((𝐴 ↑𝑜 (𝐵 +𝑜 𝑦)) ·𝑜
𝐴)) |
38 | 21, 36, 37 | sylancr 694 |
. . . . . . 7
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ↑𝑜 suc
(𝐵 +𝑜
𝑦)) = ((𝐴 ↑𝑜 (𝐵 +𝑜 𝑦)) ·𝑜
𝐴)) |
39 | 35, 38 | eqtrd 2644 |
. . . . . 6
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ↑𝑜
(𝐵 +𝑜
suc 𝑦)) = ((𝐴 ↑𝑜
(𝐵 +𝑜
𝑦))
·𝑜 𝐴)) |
40 | 22, 39 | mpan 702 |
. . . . 5
⊢ (𝑦 ∈ On → (𝐴 ↑𝑜
(𝐵 +𝑜
suc 𝑦)) = ((𝐴 ↑𝑜
(𝐵 +𝑜
𝑦))
·𝑜 𝐴)) |
41 | | oveq1 6556 |
. . . . 5
⊢ ((𝐴 ↑𝑜
(𝐵 +𝑜
𝑦)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝑦)) → ((𝐴 ↑𝑜 (𝐵 +𝑜 𝑦)) ·𝑜
𝐴) = (((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝑦)) ·𝑜 𝐴)) |
42 | 40, 41 | sylan9eq 2664 |
. . . 4
⊢ ((𝑦 ∈ On ∧ (𝐴 ↑𝑜
(𝐵 +𝑜
𝑦)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝑦))) → (𝐴 ↑𝑜 (𝐵 +𝑜 suc 𝑦)) = (((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝑦)) ·𝑜 𝐴)) |
43 | | oecl 7504 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ↑𝑜
𝑦) ∈
On) |
44 | | omass 7547 |
. . . . . . . . 9
⊢ (((𝐴 ↑𝑜
𝐵) ∈ On ∧ (𝐴 ↑𝑜
𝑦) ∈ On ∧ 𝐴 ∈ On) → (((𝐴 ↑𝑜
𝐵)
·𝑜 (𝐴 ↑𝑜 𝑦)) ·𝑜
𝐴) = ((𝐴 ↑𝑜 𝐵) ·𝑜
((𝐴
↑𝑜 𝑦) ·𝑜 𝐴))) |
45 | 24, 21, 44 | mp3an13 1407 |
. . . . . . . 8
⊢ ((𝐴 ↑𝑜
𝑦) ∈ On →
(((𝐴
↑𝑜 𝐵) ·𝑜 (𝐴 ↑𝑜
𝑦))
·𝑜 𝐴) = ((𝐴 ↑𝑜 𝐵) ·𝑜
((𝐴
↑𝑜 𝑦) ·𝑜 𝐴))) |
46 | 43, 45 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (((𝐴 ↑𝑜
𝐵)
·𝑜 (𝐴 ↑𝑜 𝑦)) ·𝑜
𝐴) = ((𝐴 ↑𝑜 𝐵) ·𝑜
((𝐴
↑𝑜 𝑦) ·𝑜 𝐴))) |
47 | | oesuc 7494 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ↑𝑜 suc
𝑦) = ((𝐴 ↑𝑜 𝑦) ·𝑜
𝐴)) |
48 | 47 | oveq2d 6565 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → ((𝐴 ↑𝑜
𝐵)
·𝑜 (𝐴 ↑𝑜 suc 𝑦)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
((𝐴
↑𝑜 𝑦) ·𝑜 𝐴))) |
49 | 46, 48 | eqtr4d 2647 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (((𝐴 ↑𝑜
𝐵)
·𝑜 (𝐴 ↑𝑜 𝑦)) ·𝑜
𝐴) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 suc 𝑦))) |
50 | 21, 49 | mpan 702 |
. . . . 5
⊢ (𝑦 ∈ On → (((𝐴 ↑𝑜
𝐵)
·𝑜 (𝐴 ↑𝑜 𝑦)) ·𝑜
𝐴) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 suc 𝑦))) |
51 | 50 | adantr 480 |
. . . 4
⊢ ((𝑦 ∈ On ∧ (𝐴 ↑𝑜
(𝐵 +𝑜
𝑦)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝑦))) → (((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝑦)) ·𝑜 𝐴) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 suc 𝑦))) |
52 | 42, 51 | eqtrd 2644 |
. . 3
⊢ ((𝑦 ∈ On ∧ (𝐴 ↑𝑜
(𝐵 +𝑜
𝑦)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝑦))) → (𝐴 ↑𝑜 (𝐵 +𝑜 suc 𝑦)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 suc 𝑦))) |
53 | 52 | ex 449 |
. 2
⊢ (𝑦 ∈ On → ((𝐴 ↑𝑜
(𝐵 +𝑜
𝑦)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝑦)) → (𝐴 ↑𝑜 (𝐵 +𝑜 suc 𝑦)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 suc 𝑦)))) |
54 | | vex 3176 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
55 | | oalim 7499 |
. . . . . . . . 9
⊢ ((𝐵 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → (𝐵 +𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐵 +𝑜 𝑦)) |
56 | 22, 55 | mpan 702 |
. . . . . . . 8
⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → (𝐵 +𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐵 +𝑜 𝑦)) |
57 | 54, 56 | mpan 702 |
. . . . . . 7
⊢ (Lim
𝑥 → (𝐵 +𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐵 +𝑜 𝑦)) |
58 | 57 | oveq2d 6565 |
. . . . . 6
⊢ (Lim
𝑥 → (𝐴 ↑𝑜 (𝐵 +𝑜 𝑥)) = (𝐴 ↑𝑜 ∪ 𝑦 ∈ 𝑥 (𝐵 +𝑜 𝑦))) |
59 | 54 | a1i 11 |
. . . . . . 7
⊢ (Lim
𝑥 → 𝑥 ∈ V) |
60 | | limord 5701 |
. . . . . . . . . 10
⊢ (Lim
𝑥 → Ord 𝑥) |
61 | | ordelon 5664 |
. . . . . . . . . 10
⊢ ((Ord
𝑥 ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On) |
62 | 60, 61 | sylan 487 |
. . . . . . . . 9
⊢ ((Lim
𝑥 ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On) |
63 | 22, 62, 36 | sylancr 694 |
. . . . . . . 8
⊢ ((Lim
𝑥 ∧ 𝑦 ∈ 𝑥) → (𝐵 +𝑜 𝑦) ∈ On) |
64 | 63 | ralrimiva 2949 |
. . . . . . 7
⊢ (Lim
𝑥 → ∀𝑦 ∈ 𝑥 (𝐵 +𝑜 𝑦) ∈ On) |
65 | | 0ellim 5704 |
. . . . . . . 8
⊢ (Lim
𝑥 → ∅ ∈
𝑥) |
66 | | ne0i 3880 |
. . . . . . . 8
⊢ (∅
∈ 𝑥 → 𝑥 ≠ ∅) |
67 | 65, 66 | syl 17 |
. . . . . . 7
⊢ (Lim
𝑥 → 𝑥 ≠ ∅) |
68 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑤 ∈ V |
69 | | oeoalem.2 |
. . . . . . . . . . 11
⊢ ∅
∈ 𝐴 |
70 | | oelim 7501 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ On ∧ (𝑤 ∈ V ∧ Lim 𝑤)) ∧ ∅ ∈ 𝐴) → (𝐴 ↑𝑜 𝑤) = ∪ 𝑧 ∈ 𝑤 (𝐴 ↑𝑜 𝑧)) |
71 | 69, 70 | mpan2 703 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ (𝑤 ∈ V ∧ Lim 𝑤)) → (𝐴 ↑𝑜 𝑤) = ∪ 𝑧 ∈ 𝑤 (𝐴 ↑𝑜 𝑧)) |
72 | 21, 71 | mpan 702 |
. . . . . . . . 9
⊢ ((𝑤 ∈ V ∧ Lim 𝑤) → (𝐴 ↑𝑜 𝑤) = ∪ 𝑧 ∈ 𝑤 (𝐴 ↑𝑜 𝑧)) |
73 | 68, 72 | mpan 702 |
. . . . . . . 8
⊢ (Lim
𝑤 → (𝐴 ↑𝑜 𝑤) = ∪ 𝑧 ∈ 𝑤 (𝐴 ↑𝑜 𝑧)) |
74 | | oewordi 7558 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈
𝐴) → (𝑧 ⊆ 𝑤 → (𝐴 ↑𝑜 𝑧) ⊆ (𝐴 ↑𝑜 𝑤))) |
75 | 69, 74 | mpan2 703 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On ∧ 𝐴 ∈ On) → (𝑧 ⊆ 𝑤 → (𝐴 ↑𝑜 𝑧) ⊆ (𝐴 ↑𝑜 𝑤))) |
76 | 21, 75 | mp3an3 1405 |
. . . . . . . . 9
⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧 ⊆ 𝑤 → (𝐴 ↑𝑜 𝑧) ⊆ (𝐴 ↑𝑜 𝑤))) |
77 | 76 | 3impia 1253 |
. . . . . . . 8
⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On ∧ 𝑧 ⊆ 𝑤) → (𝐴 ↑𝑜 𝑧) ⊆ (𝐴 ↑𝑜 𝑤)) |
78 | 73, 77 | onoviun 7327 |
. . . . . . 7
⊢ ((𝑥 ∈ V ∧ ∀𝑦 ∈ 𝑥 (𝐵 +𝑜 𝑦) ∈ On ∧ 𝑥 ≠ ∅) → (𝐴 ↑𝑜 ∪ 𝑦 ∈ 𝑥 (𝐵 +𝑜 𝑦)) = ∪
𝑦 ∈ 𝑥 (𝐴 ↑𝑜 (𝐵 +𝑜 𝑦))) |
79 | 59, 64, 67, 78 | syl3anc 1318 |
. . . . . 6
⊢ (Lim
𝑥 → (𝐴 ↑𝑜 ∪ 𝑦 ∈ 𝑥 (𝐵 +𝑜 𝑦)) = ∪
𝑦 ∈ 𝑥 (𝐴 ↑𝑜 (𝐵 +𝑜 𝑦))) |
80 | 58, 79 | eqtrd 2644 |
. . . . 5
⊢ (Lim
𝑥 → (𝐴 ↑𝑜 (𝐵 +𝑜 𝑥)) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑𝑜 (𝐵 +𝑜 𝑦))) |
81 | | iuneq2 4473 |
. . . . 5
⊢
(∀𝑦 ∈
𝑥 (𝐴 ↑𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝑦)) → ∪
𝑦 ∈ 𝑥 (𝐴 ↑𝑜 (𝐵 +𝑜 𝑦)) = ∪ 𝑦 ∈ 𝑥 ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝑦))) |
82 | 80, 81 | sylan9eq 2664 |
. . . 4
⊢ ((Lim
𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ↑𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝑦))) → (𝐴 ↑𝑜 (𝐵 +𝑜 𝑥)) = ∪ 𝑦 ∈ 𝑥 ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝑦))) |
83 | | oelim 7501 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ ∅ ∈ 𝐴) → (𝐴 ↑𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑𝑜 𝑦)) |
84 | 69, 83 | mpan2 703 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → (𝐴 ↑𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑𝑜 𝑦)) |
85 | 21, 84 | mpan 702 |
. . . . . . . 8
⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → (𝐴 ↑𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑𝑜 𝑦)) |
86 | 54, 85 | mpan 702 |
. . . . . . 7
⊢ (Lim
𝑥 → (𝐴 ↑𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 (𝐴 ↑𝑜 𝑦)) |
87 | 86 | oveq2d 6565 |
. . . . . 6
⊢ (Lim
𝑥 → ((𝐴 ↑𝑜
𝐵)
·𝑜 (𝐴 ↑𝑜 𝑥)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
∪ 𝑦 ∈ 𝑥 (𝐴 ↑𝑜 𝑦))) |
88 | 21, 62, 43 | sylancr 694 |
. . . . . . . 8
⊢ ((Lim
𝑥 ∧ 𝑦 ∈ 𝑥) → (𝐴 ↑𝑜 𝑦) ∈ On) |
89 | 88 | ralrimiva 2949 |
. . . . . . 7
⊢ (Lim
𝑥 → ∀𝑦 ∈ 𝑥 (𝐴 ↑𝑜 𝑦) ∈ On) |
90 | | omlim 7500 |
. . . . . . . . . 10
⊢ (((𝐴 ↑𝑜
𝐵) ∈ On ∧ (𝑤 ∈ V ∧ Lim 𝑤)) → ((𝐴 ↑𝑜 𝐵) ·𝑜
𝑤) = ∪ 𝑧 ∈ 𝑤 ((𝐴 ↑𝑜 𝐵) ·𝑜
𝑧)) |
91 | 24, 90 | mpan 702 |
. . . . . . . . 9
⊢ ((𝑤 ∈ V ∧ Lim 𝑤) → ((𝐴 ↑𝑜 𝐵) ·𝑜
𝑤) = ∪ 𝑧 ∈ 𝑤 ((𝐴 ↑𝑜 𝐵) ·𝑜
𝑧)) |
92 | 68, 91 | mpan 702 |
. . . . . . . 8
⊢ (Lim
𝑤 → ((𝐴 ↑𝑜
𝐵)
·𝑜 𝑤) = ∪ 𝑧 ∈ 𝑤 ((𝐴 ↑𝑜 𝐵) ·𝑜
𝑧)) |
93 | | omwordi 7538 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On ∧ (𝐴 ↑𝑜
𝐵) ∈ On) → (𝑧 ⊆ 𝑤 → ((𝐴 ↑𝑜 𝐵) ·𝑜
𝑧) ⊆ ((𝐴 ↑𝑜
𝐵)
·𝑜 𝑤))) |
94 | 24, 93 | mp3an3 1405 |
. . . . . . . . 9
⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧 ⊆ 𝑤 → ((𝐴 ↑𝑜 𝐵) ·𝑜
𝑧) ⊆ ((𝐴 ↑𝑜
𝐵)
·𝑜 𝑤))) |
95 | 94 | 3impia 1253 |
. . . . . . . 8
⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On ∧ 𝑧 ⊆ 𝑤) → ((𝐴 ↑𝑜 𝐵) ·𝑜
𝑧) ⊆ ((𝐴 ↑𝑜
𝐵)
·𝑜 𝑤)) |
96 | 92, 95 | onoviun 7327 |
. . . . . . 7
⊢ ((𝑥 ∈ V ∧ ∀𝑦 ∈ 𝑥 (𝐴 ↑𝑜 𝑦) ∈ On ∧ 𝑥 ≠ ∅) → ((𝐴 ↑𝑜
𝐵)
·𝑜 ∪ 𝑦 ∈ 𝑥 (𝐴 ↑𝑜 𝑦)) = ∪ 𝑦 ∈ 𝑥 ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝑦))) |
97 | 59, 89, 67, 96 | syl3anc 1318 |
. . . . . 6
⊢ (Lim
𝑥 → ((𝐴 ↑𝑜
𝐵)
·𝑜 ∪ 𝑦 ∈ 𝑥 (𝐴 ↑𝑜 𝑦)) = ∪ 𝑦 ∈ 𝑥 ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝑦))) |
98 | 87, 97 | eqtrd 2644 |
. . . . 5
⊢ (Lim
𝑥 → ((𝐴 ↑𝑜
𝐵)
·𝑜 (𝐴 ↑𝑜 𝑥)) = ∪ 𝑦 ∈ 𝑥 ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝑦))) |
99 | 98 | adantr 480 |
. . . 4
⊢ ((Lim
𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ↑𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝑦))) → ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝑥)) = ∪
𝑦 ∈ 𝑥 ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝑦))) |
100 | 82, 99 | eqtr4d 2647 |
. . 3
⊢ ((Lim
𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ↑𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝑦))) → (𝐴 ↑𝑜 (𝐵 +𝑜 𝑥)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝑥))) |
101 | 100 | ex 449 |
. 2
⊢ (Lim
𝑥 → (∀𝑦 ∈ 𝑥 (𝐴 ↑𝑜 (𝐵 +𝑜 𝑦)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝑦)) → (𝐴 ↑𝑜 (𝐵 +𝑜 𝑥)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝑥)))) |
102 | 5, 10, 15, 20, 33, 53, 101 | tfinds 6951 |
1
⊢ (𝐶 ∈ On → (𝐴 ↑𝑜
(𝐵 +𝑜
𝐶)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝐶))) |