Step | Hyp | Ref
| Expression |
1 | | oveq2 6658 |
. . . 4
⊢ (𝑧 = ∅ → (𝐴 +𝑜 𝑧) = (𝐴 +𝑜
∅)) |
2 | | mpteq1 4737 |
. . . . . . . 8
⊢ (𝑧 = ∅ → (𝑥 ∈ 𝑧 ↦ (𝐴 +𝑜 𝑥)) = (𝑥 ∈ ∅ ↦ (𝐴 +𝑜 𝑥))) |
3 | | mpt0 6021 |
. . . . . . . 8
⊢ (𝑥 ∈ ∅ ↦ (𝐴 +𝑜 𝑥)) = ∅ |
4 | 2, 3 | syl6eq 2672 |
. . . . . . 7
⊢ (𝑧 = ∅ → (𝑥 ∈ 𝑧 ↦ (𝐴 +𝑜 𝑥)) = ∅) |
5 | 4 | rneqd 5353 |
. . . . . 6
⊢ (𝑧 = ∅ → ran (𝑥 ∈ 𝑧 ↦ (𝐴 +𝑜 𝑥)) = ran ∅) |
6 | | rn0 5377 |
. . . . . 6
⊢ ran
∅ = ∅ |
7 | 5, 6 | syl6eq 2672 |
. . . . 5
⊢ (𝑧 = ∅ → ran (𝑥 ∈ 𝑧 ↦ (𝐴 +𝑜 𝑥)) = ∅) |
8 | 7 | uneq2d 3767 |
. . . 4
⊢ (𝑧 = ∅ → (𝐴 ∪ ran (𝑥 ∈ 𝑧 ↦ (𝐴 +𝑜 𝑥))) = (𝐴 ∪ ∅)) |
9 | 1, 8 | eqeq12d 2637 |
. . 3
⊢ (𝑧 = ∅ → ((𝐴 +𝑜 𝑧) = (𝐴 ∪ ran (𝑥 ∈ 𝑧 ↦ (𝐴 +𝑜 𝑥))) ↔ (𝐴 +𝑜 ∅) = (𝐴 ∪
∅))) |
10 | | oveq2 6658 |
. . . 4
⊢ (𝑧 = 𝑤 → (𝐴 +𝑜 𝑧) = (𝐴 +𝑜 𝑤)) |
11 | | mpteq1 4737 |
. . . . . 6
⊢ (𝑧 = 𝑤 → (𝑥 ∈ 𝑧 ↦ (𝐴 +𝑜 𝑥)) = (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥))) |
12 | 11 | rneqd 5353 |
. . . . 5
⊢ (𝑧 = 𝑤 → ran (𝑥 ∈ 𝑧 ↦ (𝐴 +𝑜 𝑥)) = ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥))) |
13 | 12 | uneq2d 3767 |
. . . 4
⊢ (𝑧 = 𝑤 → (𝐴 ∪ ran (𝑥 ∈ 𝑧 ↦ (𝐴 +𝑜 𝑥))) = (𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥)))) |
14 | 10, 13 | eqeq12d 2637 |
. . 3
⊢ (𝑧 = 𝑤 → ((𝐴 +𝑜 𝑧) = (𝐴 ∪ ran (𝑥 ∈ 𝑧 ↦ (𝐴 +𝑜 𝑥))) ↔ (𝐴 +𝑜 𝑤) = (𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥))))) |
15 | | oveq2 6658 |
. . . 4
⊢ (𝑧 = suc 𝑤 → (𝐴 +𝑜 𝑧) = (𝐴 +𝑜 suc 𝑤)) |
16 | | mpteq1 4737 |
. . . . . 6
⊢ (𝑧 = suc 𝑤 → (𝑥 ∈ 𝑧 ↦ (𝐴 +𝑜 𝑥)) = (𝑥 ∈ suc 𝑤 ↦ (𝐴 +𝑜 𝑥))) |
17 | 16 | rneqd 5353 |
. . . . 5
⊢ (𝑧 = suc 𝑤 → ran (𝑥 ∈ 𝑧 ↦ (𝐴 +𝑜 𝑥)) = ran (𝑥 ∈ suc 𝑤 ↦ (𝐴 +𝑜 𝑥))) |
18 | 17 | uneq2d 3767 |
. . . 4
⊢ (𝑧 = suc 𝑤 → (𝐴 ∪ ran (𝑥 ∈ 𝑧 ↦ (𝐴 +𝑜 𝑥))) = (𝐴 ∪ ran (𝑥 ∈ suc 𝑤 ↦ (𝐴 +𝑜 𝑥)))) |
19 | 15, 18 | eqeq12d 2637 |
. . 3
⊢ (𝑧 = suc 𝑤 → ((𝐴 +𝑜 𝑧) = (𝐴 ∪ ran (𝑥 ∈ 𝑧 ↦ (𝐴 +𝑜 𝑥))) ↔ (𝐴 +𝑜 suc 𝑤) = (𝐴 ∪ ran (𝑥 ∈ suc 𝑤 ↦ (𝐴 +𝑜 𝑥))))) |
20 | | oveq2 6658 |
. . . 4
⊢ (𝑧 = 𝐵 → (𝐴 +𝑜 𝑧) = (𝐴 +𝑜 𝐵)) |
21 | | mpteq1 4737 |
. . . . . 6
⊢ (𝑧 = 𝐵 → (𝑥 ∈ 𝑧 ↦ (𝐴 +𝑜 𝑥)) = (𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥))) |
22 | 21 | rneqd 5353 |
. . . . 5
⊢ (𝑧 = 𝐵 → ran (𝑥 ∈ 𝑧 ↦ (𝐴 +𝑜 𝑥)) = ran (𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥))) |
23 | 22 | uneq2d 3767 |
. . . 4
⊢ (𝑧 = 𝐵 → (𝐴 ∪ ran (𝑥 ∈ 𝑧 ↦ (𝐴 +𝑜 𝑥))) = (𝐴 ∪ ran (𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥)))) |
24 | 20, 23 | eqeq12d 2637 |
. . 3
⊢ (𝑧 = 𝐵 → ((𝐴 +𝑜 𝑧) = (𝐴 ∪ ran (𝑥 ∈ 𝑧 ↦ (𝐴 +𝑜 𝑥))) ↔ (𝐴 +𝑜 𝐵) = (𝐴 ∪ ran (𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥))))) |
25 | | oa0 7596 |
. . . 4
⊢ (𝐴 ∈ On → (𝐴 +𝑜 ∅)
= 𝐴) |
26 | | un0 3967 |
. . . 4
⊢ (𝐴 ∪ ∅) = 𝐴 |
27 | 25, 26 | syl6eqr 2674 |
. . 3
⊢ (𝐴 ∈ On → (𝐴 +𝑜 ∅)
= (𝐴 ∪
∅)) |
28 | | uneq1 3760 |
. . . . . 6
⊢ ((𝐴 +𝑜 𝑤) = (𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥))) → ((𝐴 +𝑜 𝑤) ∪ {(𝐴 +𝑜 𝑤)}) = ((𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥))) ∪ {(𝐴 +𝑜 𝑤)})) |
29 | | unass 3770 |
. . . . . . 7
⊢ ((𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥))) ∪ {(𝐴 +𝑜 𝑤)}) = (𝐴 ∪ (ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥)) ∪ {(𝐴 +𝑜 𝑤)})) |
30 | | rexun 3793 |
. . . . . . . . . . 11
⊢
(∃𝑥 ∈
(𝑤 ∪ {𝑤})𝑦 = (𝐴 +𝑜 𝑥) ↔ (∃𝑥 ∈ 𝑤 𝑦 = (𝐴 +𝑜 𝑥) ∨ ∃𝑥 ∈ {𝑤}𝑦 = (𝐴 +𝑜 𝑥))) |
31 | | df-suc 5729 |
. . . . . . . . . . . 12
⊢ suc 𝑤 = (𝑤 ∪ {𝑤}) |
32 | 31 | rexeqi 3143 |
. . . . . . . . . . 11
⊢
(∃𝑥 ∈ suc
𝑤𝑦 = (𝐴 +𝑜 𝑥) ↔ ∃𝑥 ∈ (𝑤 ∪ {𝑤})𝑦 = (𝐴 +𝑜 𝑥)) |
33 | | vex 3203 |
. . . . . . . . . . . . 13
⊢ 𝑦 ∈ V |
34 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥)) = (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥)) |
35 | 34 | elrnmpt 5372 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ V → (𝑦 ∈ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥)) ↔ ∃𝑥 ∈ 𝑤 𝑦 = (𝐴 +𝑜 𝑥))) |
36 | 33, 35 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥)) ↔ ∃𝑥 ∈ 𝑤 𝑦 = (𝐴 +𝑜 𝑥)) |
37 | | velsn 4193 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ {(𝐴 +𝑜 𝑤)} ↔ 𝑦 = (𝐴 +𝑜 𝑤)) |
38 | | vex 3203 |
. . . . . . . . . . . . . 14
⊢ 𝑤 ∈ V |
39 | | oveq2 6658 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑤 → (𝐴 +𝑜 𝑥) = (𝐴 +𝑜 𝑤)) |
40 | 39 | eqeq2d 2632 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑤 → (𝑦 = (𝐴 +𝑜 𝑥) ↔ 𝑦 = (𝐴 +𝑜 𝑤))) |
41 | 38, 40 | rexsn 4223 |
. . . . . . . . . . . . 13
⊢
(∃𝑥 ∈
{𝑤}𝑦 = (𝐴 +𝑜 𝑥) ↔ 𝑦 = (𝐴 +𝑜 𝑤)) |
42 | 37, 41 | bitr4i 267 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ {(𝐴 +𝑜 𝑤)} ↔ ∃𝑥 ∈ {𝑤}𝑦 = (𝐴 +𝑜 𝑥)) |
43 | 36, 42 | orbi12i 543 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥)) ∨ 𝑦 ∈ {(𝐴 +𝑜 𝑤)}) ↔ (∃𝑥 ∈ 𝑤 𝑦 = (𝐴 +𝑜 𝑥) ∨ ∃𝑥 ∈ {𝑤}𝑦 = (𝐴 +𝑜 𝑥))) |
44 | 30, 32, 43 | 3bitr4i 292 |
. . . . . . . . . 10
⊢
(∃𝑥 ∈ suc
𝑤𝑦 = (𝐴 +𝑜 𝑥) ↔ (𝑦 ∈ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥)) ∨ 𝑦 ∈ {(𝐴 +𝑜 𝑤)})) |
45 | | eqid 2622 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ suc 𝑤 ↦ (𝐴 +𝑜 𝑥)) = (𝑥 ∈ suc 𝑤 ↦ (𝐴 +𝑜 𝑥)) |
46 | | ovex 6678 |
. . . . . . . . . . 11
⊢ (𝐴 +𝑜 𝑥) ∈ V |
47 | 45, 46 | elrnmpti 5376 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ran (𝑥 ∈ suc 𝑤 ↦ (𝐴 +𝑜 𝑥)) ↔ ∃𝑥 ∈ suc 𝑤𝑦 = (𝐴 +𝑜 𝑥)) |
48 | | elun 3753 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥)) ∪ {(𝐴 +𝑜 𝑤)}) ↔ (𝑦 ∈ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥)) ∨ 𝑦 ∈ {(𝐴 +𝑜 𝑤)})) |
49 | 44, 47, 48 | 3bitr4i 292 |
. . . . . . . . 9
⊢ (𝑦 ∈ ran (𝑥 ∈ suc 𝑤 ↦ (𝐴 +𝑜 𝑥)) ↔ 𝑦 ∈ (ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥)) ∪ {(𝐴 +𝑜 𝑤)})) |
50 | 49 | eqriv 2619 |
. . . . . . . 8
⊢ ran
(𝑥 ∈ suc 𝑤 ↦ (𝐴 +𝑜 𝑥)) = (ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥)) ∪ {(𝐴 +𝑜 𝑤)}) |
51 | 50 | uneq2i 3764 |
. . . . . . 7
⊢ (𝐴 ∪ ran (𝑥 ∈ suc 𝑤 ↦ (𝐴 +𝑜 𝑥))) = (𝐴 ∪ (ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥)) ∪ {(𝐴 +𝑜 𝑤)})) |
52 | 29, 51 | eqtr4i 2647 |
. . . . . 6
⊢ ((𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥))) ∪ {(𝐴 +𝑜 𝑤)}) = (𝐴 ∪ ran (𝑥 ∈ suc 𝑤 ↦ (𝐴 +𝑜 𝑥))) |
53 | 28, 52 | syl6eq 2672 |
. . . . 5
⊢ ((𝐴 +𝑜 𝑤) = (𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥))) → ((𝐴 +𝑜 𝑤) ∪ {(𝐴 +𝑜 𝑤)}) = (𝐴 ∪ ran (𝑥 ∈ suc 𝑤 ↦ (𝐴 +𝑜 𝑥)))) |
54 | | oasuc 7604 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝑤 ∈ On) → (𝐴 +𝑜 suc 𝑤) = suc (𝐴 +𝑜 𝑤)) |
55 | | df-suc 5729 |
. . . . . . 7
⊢ suc
(𝐴 +𝑜
𝑤) = ((𝐴 +𝑜 𝑤) ∪ {(𝐴 +𝑜 𝑤)}) |
56 | 54, 55 | syl6eq 2672 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝑤 ∈ On) → (𝐴 +𝑜 suc 𝑤) = ((𝐴 +𝑜 𝑤) ∪ {(𝐴 +𝑜 𝑤)})) |
57 | 56 | eqeq1d 2624 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝑤 ∈ On) → ((𝐴 +𝑜 suc 𝑤) = (𝐴 ∪ ran (𝑥 ∈ suc 𝑤 ↦ (𝐴 +𝑜 𝑥))) ↔ ((𝐴 +𝑜 𝑤) ∪ {(𝐴 +𝑜 𝑤)}) = (𝐴 ∪ ran (𝑥 ∈ suc 𝑤 ↦ (𝐴 +𝑜 𝑥))))) |
58 | 53, 57 | syl5ibr 236 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝑤 ∈ On) → ((𝐴 +𝑜 𝑤) = (𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥))) → (𝐴 +𝑜 suc 𝑤) = (𝐴 ∪ ran (𝑥 ∈ suc 𝑤 ↦ (𝐴 +𝑜 𝑥))))) |
59 | 58 | expcom 451 |
. . 3
⊢ (𝑤 ∈ On → (𝐴 ∈ On → ((𝐴 +𝑜 𝑤) = (𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥))) → (𝐴 +𝑜 suc 𝑤) = (𝐴 ∪ ran (𝑥 ∈ suc 𝑤 ↦ (𝐴 +𝑜 𝑥)))))) |
60 | | vex 3203 |
. . . . . . . 8
⊢ 𝑧 ∈ V |
61 | | oalim 7612 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ (𝑧 ∈ V ∧ Lim 𝑧)) → (𝐴 +𝑜 𝑧) = ∪ 𝑤 ∈ 𝑧 (𝐴 +𝑜 𝑤)) |
62 | 60, 61 | mpanr1 719 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ Lim 𝑧) → (𝐴 +𝑜 𝑧) = ∪ 𝑤 ∈ 𝑧 (𝐴 +𝑜 𝑤)) |
63 | 62 | ancoms 469 |
. . . . . 6
⊢ ((Lim
𝑧 ∧ 𝐴 ∈ On) → (𝐴 +𝑜 𝑧) = ∪ 𝑤 ∈ 𝑧 (𝐴 +𝑜 𝑤)) |
64 | 63 | adantr 481 |
. . . . 5
⊢ (((Lim
𝑧 ∧ 𝐴 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝐴 +𝑜 𝑤) = (𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥)))) → (𝐴 +𝑜 𝑧) = ∪ 𝑤 ∈ 𝑧 (𝐴 +𝑜 𝑤)) |
65 | | iuneq2 4537 |
. . . . . 6
⊢
(∀𝑤 ∈
𝑧 (𝐴 +𝑜 𝑤) = (𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥))) → ∪ 𝑤 ∈ 𝑧 (𝐴 +𝑜 𝑤) = ∪ 𝑤 ∈ 𝑧 (𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥)))) |
66 | 65 | adantl 482 |
. . . . 5
⊢ (((Lim
𝑧 ∧ 𝐴 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝐴 +𝑜 𝑤) = (𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥)))) → ∪ 𝑤 ∈ 𝑧 (𝐴 +𝑜 𝑤) = ∪ 𝑤 ∈ 𝑧 (𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥)))) |
67 | | iunun 4604 |
. . . . . . 7
⊢ ∪ 𝑤 ∈ 𝑧 (𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥))) = (∪
𝑤 ∈ 𝑧 𝐴 ∪ ∪
𝑤 ∈ 𝑧 ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥))) |
68 | | 0ellim 5787 |
. . . . . . . . 9
⊢ (Lim
𝑧 → ∅ ∈
𝑧) |
69 | | ne0i 3921 |
. . . . . . . . 9
⊢ (∅
∈ 𝑧 → 𝑧 ≠ ∅) |
70 | | iunconst 4529 |
. . . . . . . . 9
⊢ (𝑧 ≠ ∅ → ∪ 𝑤 ∈ 𝑧 𝐴 = 𝐴) |
71 | 68, 69, 70 | 3syl 18 |
. . . . . . . 8
⊢ (Lim
𝑧 → ∪ 𝑤 ∈ 𝑧 𝐴 = 𝐴) |
72 | | limuni 5785 |
. . . . . . . . . . . 12
⊢ (Lim
𝑧 → 𝑧 = ∪ 𝑧) |
73 | 72 | rexeqdv 3145 |
. . . . . . . . . . 11
⊢ (Lim
𝑧 → (∃𝑥 ∈ 𝑧 𝑦 = (𝐴 +𝑜 𝑥) ↔ ∃𝑥 ∈ ∪ 𝑧𝑦 = (𝐴 +𝑜 𝑥))) |
74 | | df-rex 2918 |
. . . . . . . . . . . . . 14
⊢
(∃𝑥 ∈
𝑤 𝑦 = (𝐴 +𝑜 𝑥) ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝑦 = (𝐴 +𝑜 𝑥))) |
75 | 36, 74 | bitri 264 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥)) ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝑦 = (𝐴 +𝑜 𝑥))) |
76 | 75 | rexbii 3041 |
. . . . . . . . . . . 12
⊢
(∃𝑤 ∈
𝑧 𝑦 ∈ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥)) ↔ ∃𝑤 ∈ 𝑧 ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝑦 = (𝐴 +𝑜 𝑥))) |
77 | | eluni2 4440 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ∪ 𝑧
↔ ∃𝑤 ∈
𝑧 𝑥 ∈ 𝑤) |
78 | 77 | anbi1i 731 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ∪ 𝑧
∧ 𝑦 = (𝐴 +𝑜 𝑥)) ↔ (∃𝑤 ∈ 𝑧 𝑥 ∈ 𝑤 ∧ 𝑦 = (𝐴 +𝑜 𝑥))) |
79 | | r19.41v 3089 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑤 ∈
𝑧 (𝑥 ∈ 𝑤 ∧ 𝑦 = (𝐴 +𝑜 𝑥)) ↔ (∃𝑤 ∈ 𝑧 𝑥 ∈ 𝑤 ∧ 𝑦 = (𝐴 +𝑜 𝑥))) |
80 | 78, 79 | bitr4i 267 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ∪ 𝑧
∧ 𝑦 = (𝐴 +𝑜 𝑥)) ↔ ∃𝑤 ∈ 𝑧 (𝑥 ∈ 𝑤 ∧ 𝑦 = (𝐴 +𝑜 𝑥))) |
81 | 80 | exbii 1774 |
. . . . . . . . . . . . 13
⊢
(∃𝑥(𝑥 ∈ ∪ 𝑧
∧ 𝑦 = (𝐴 +𝑜 𝑥)) ↔ ∃𝑥∃𝑤 ∈ 𝑧 (𝑥 ∈ 𝑤 ∧ 𝑦 = (𝐴 +𝑜 𝑥))) |
82 | | df-rex 2918 |
. . . . . . . . . . . . 13
⊢
(∃𝑥 ∈
∪ 𝑧𝑦 = (𝐴 +𝑜 𝑥) ↔ ∃𝑥(𝑥 ∈ ∪ 𝑧 ∧ 𝑦 = (𝐴 +𝑜 𝑥))) |
83 | | rexcom4 3225 |
. . . . . . . . . . . . 13
⊢
(∃𝑤 ∈
𝑧 ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝑦 = (𝐴 +𝑜 𝑥)) ↔ ∃𝑥∃𝑤 ∈ 𝑧 (𝑥 ∈ 𝑤 ∧ 𝑦 = (𝐴 +𝑜 𝑥))) |
84 | 81, 82, 83 | 3bitr4i 292 |
. . . . . . . . . . . 12
⊢
(∃𝑥 ∈
∪ 𝑧𝑦 = (𝐴 +𝑜 𝑥) ↔ ∃𝑤 ∈ 𝑧 ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝑦 = (𝐴 +𝑜 𝑥))) |
85 | 76, 84 | bitr4i 267 |
. . . . . . . . . . 11
⊢
(∃𝑤 ∈
𝑧 𝑦 ∈ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥)) ↔ ∃𝑥 ∈ ∪ 𝑧𝑦 = (𝐴 +𝑜 𝑥)) |
86 | 73, 85 | syl6rbbr 279 |
. . . . . . . . . 10
⊢ (Lim
𝑧 → (∃𝑤 ∈ 𝑧 𝑦 ∈ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥)) ↔ ∃𝑥 ∈ 𝑧 𝑦 = (𝐴 +𝑜 𝑥))) |
87 | | eliun 4524 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ∪ 𝑤 ∈ 𝑧 ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥)) ↔ ∃𝑤 ∈ 𝑧 𝑦 ∈ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥))) |
88 | | eqid 2622 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝑧 ↦ (𝐴 +𝑜 𝑥)) = (𝑥 ∈ 𝑧 ↦ (𝐴 +𝑜 𝑥)) |
89 | 88, 46 | elrnmpti 5376 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ran (𝑥 ∈ 𝑧 ↦ (𝐴 +𝑜 𝑥)) ↔ ∃𝑥 ∈ 𝑧 𝑦 = (𝐴 +𝑜 𝑥)) |
90 | 86, 87, 89 | 3bitr4g 303 |
. . . . . . . . 9
⊢ (Lim
𝑧 → (𝑦 ∈ ∪ 𝑤 ∈ 𝑧 ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥)) ↔ 𝑦 ∈ ran (𝑥 ∈ 𝑧 ↦ (𝐴 +𝑜 𝑥)))) |
91 | 90 | eqrdv 2620 |
. . . . . . . 8
⊢ (Lim
𝑧 → ∪ 𝑤 ∈ 𝑧 ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥)) = ran (𝑥 ∈ 𝑧 ↦ (𝐴 +𝑜 𝑥))) |
92 | 71, 91 | uneq12d 3768 |
. . . . . . 7
⊢ (Lim
𝑧 → (∪ 𝑤 ∈ 𝑧 𝐴 ∪ ∪
𝑤 ∈ 𝑧 ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥))) = (𝐴 ∪ ran (𝑥 ∈ 𝑧 ↦ (𝐴 +𝑜 𝑥)))) |
93 | 67, 92 | syl5eq 2668 |
. . . . . 6
⊢ (Lim
𝑧 → ∪ 𝑤 ∈ 𝑧 (𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥))) = (𝐴 ∪ ran (𝑥 ∈ 𝑧 ↦ (𝐴 +𝑜 𝑥)))) |
94 | 93 | ad2antrr 762 |
. . . . 5
⊢ (((Lim
𝑧 ∧ 𝐴 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝐴 +𝑜 𝑤) = (𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥)))) → ∪ 𝑤 ∈ 𝑧 (𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥))) = (𝐴 ∪ ran (𝑥 ∈ 𝑧 ↦ (𝐴 +𝑜 𝑥)))) |
95 | 64, 66, 94 | 3eqtrd 2660 |
. . . 4
⊢ (((Lim
𝑧 ∧ 𝐴 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝐴 +𝑜 𝑤) = (𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥)))) → (𝐴 +𝑜 𝑧) = (𝐴 ∪ ran (𝑥 ∈ 𝑧 ↦ (𝐴 +𝑜 𝑥)))) |
96 | 95 | exp31 630 |
. . 3
⊢ (Lim
𝑧 → (𝐴 ∈ On → (∀𝑤 ∈ 𝑧 (𝐴 +𝑜 𝑤) = (𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +𝑜 𝑥))) → (𝐴 +𝑜 𝑧) = (𝐴 ∪ ran (𝑥 ∈ 𝑧 ↦ (𝐴 +𝑜 𝑥)))))) |
97 | 9, 14, 19, 24, 27, 59, 96 | tfinds3 7064 |
. 2
⊢ (𝐵 ∈ On → (𝐴 ∈ On → (𝐴 +𝑜 𝐵) = (𝐴 ∪ ran (𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥))))) |
98 | 97 | impcom 446 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +𝑜 𝐵) = (𝐴 ∪ ran (𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥)))) |