| Step | Hyp | Ref
| Expression |
| 1 | | oveq2 7439 |
. . . 4
⊢ (𝑧 = ∅ → (𝐴 +o 𝑧) = (𝐴 +o ∅)) |
| 2 | | mpteq1 5235 |
. . . . . . . 8
⊢ (𝑧 = ∅ → (𝑥 ∈ 𝑧 ↦ (𝐴 +o 𝑥)) = (𝑥 ∈ ∅ ↦ (𝐴 +o 𝑥))) |
| 3 | | mpt0 6710 |
. . . . . . . 8
⊢ (𝑥 ∈ ∅ ↦ (𝐴 +o 𝑥)) = ∅ |
| 4 | 2, 3 | eqtrdi 2793 |
. . . . . . 7
⊢ (𝑧 = ∅ → (𝑥 ∈ 𝑧 ↦ (𝐴 +o 𝑥)) = ∅) |
| 5 | 4 | rneqd 5949 |
. . . . . 6
⊢ (𝑧 = ∅ → ran (𝑥 ∈ 𝑧 ↦ (𝐴 +o 𝑥)) = ran ∅) |
| 6 | | rn0 5936 |
. . . . . 6
⊢ ran
∅ = ∅ |
| 7 | 5, 6 | eqtrdi 2793 |
. . . . 5
⊢ (𝑧 = ∅ → ran (𝑥 ∈ 𝑧 ↦ (𝐴 +o 𝑥)) = ∅) |
| 8 | 7 | uneq2d 4168 |
. . . 4
⊢ (𝑧 = ∅ → (𝐴 ∪ ran (𝑥 ∈ 𝑧 ↦ (𝐴 +o 𝑥))) = (𝐴 ∪ ∅)) |
| 9 | 1, 8 | eqeq12d 2753 |
. . 3
⊢ (𝑧 = ∅ → ((𝐴 +o 𝑧) = (𝐴 ∪ ran (𝑥 ∈ 𝑧 ↦ (𝐴 +o 𝑥))) ↔ (𝐴 +o ∅) = (𝐴 ∪ ∅))) |
| 10 | | oveq2 7439 |
. . . 4
⊢ (𝑧 = 𝑤 → (𝐴 +o 𝑧) = (𝐴 +o 𝑤)) |
| 11 | | mpteq1 5235 |
. . . . . 6
⊢ (𝑧 = 𝑤 → (𝑥 ∈ 𝑧 ↦ (𝐴 +o 𝑥)) = (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥))) |
| 12 | 11 | rneqd 5949 |
. . . . 5
⊢ (𝑧 = 𝑤 → ran (𝑥 ∈ 𝑧 ↦ (𝐴 +o 𝑥)) = ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥))) |
| 13 | 12 | uneq2d 4168 |
. . . 4
⊢ (𝑧 = 𝑤 → (𝐴 ∪ ran (𝑥 ∈ 𝑧 ↦ (𝐴 +o 𝑥))) = (𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥)))) |
| 14 | 10, 13 | eqeq12d 2753 |
. . 3
⊢ (𝑧 = 𝑤 → ((𝐴 +o 𝑧) = (𝐴 ∪ ran (𝑥 ∈ 𝑧 ↦ (𝐴 +o 𝑥))) ↔ (𝐴 +o 𝑤) = (𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥))))) |
| 15 | | oveq2 7439 |
. . . 4
⊢ (𝑧 = suc 𝑤 → (𝐴 +o 𝑧) = (𝐴 +o suc 𝑤)) |
| 16 | | mpteq1 5235 |
. . . . . 6
⊢ (𝑧 = suc 𝑤 → (𝑥 ∈ 𝑧 ↦ (𝐴 +o 𝑥)) = (𝑥 ∈ suc 𝑤 ↦ (𝐴 +o 𝑥))) |
| 17 | 16 | rneqd 5949 |
. . . . 5
⊢ (𝑧 = suc 𝑤 → ran (𝑥 ∈ 𝑧 ↦ (𝐴 +o 𝑥)) = ran (𝑥 ∈ suc 𝑤 ↦ (𝐴 +o 𝑥))) |
| 18 | 17 | uneq2d 4168 |
. . . 4
⊢ (𝑧 = suc 𝑤 → (𝐴 ∪ ran (𝑥 ∈ 𝑧 ↦ (𝐴 +o 𝑥))) = (𝐴 ∪ ran (𝑥 ∈ suc 𝑤 ↦ (𝐴 +o 𝑥)))) |
| 19 | 15, 18 | eqeq12d 2753 |
. . 3
⊢ (𝑧 = suc 𝑤 → ((𝐴 +o 𝑧) = (𝐴 ∪ ran (𝑥 ∈ 𝑧 ↦ (𝐴 +o 𝑥))) ↔ (𝐴 +o suc 𝑤) = (𝐴 ∪ ran (𝑥 ∈ suc 𝑤 ↦ (𝐴 +o 𝑥))))) |
| 20 | | oveq2 7439 |
. . . 4
⊢ (𝑧 = 𝐵 → (𝐴 +o 𝑧) = (𝐴 +o 𝐵)) |
| 21 | | mpteq1 5235 |
. . . . . 6
⊢ (𝑧 = 𝐵 → (𝑥 ∈ 𝑧 ↦ (𝐴 +o 𝑥)) = (𝑥 ∈ 𝐵 ↦ (𝐴 +o 𝑥))) |
| 22 | 21 | rneqd 5949 |
. . . . 5
⊢ (𝑧 = 𝐵 → ran (𝑥 ∈ 𝑧 ↦ (𝐴 +o 𝑥)) = ran (𝑥 ∈ 𝐵 ↦ (𝐴 +o 𝑥))) |
| 23 | 22 | uneq2d 4168 |
. . . 4
⊢ (𝑧 = 𝐵 → (𝐴 ∪ ran (𝑥 ∈ 𝑧 ↦ (𝐴 +o 𝑥))) = (𝐴 ∪ ran (𝑥 ∈ 𝐵 ↦ (𝐴 +o 𝑥)))) |
| 24 | 20, 23 | eqeq12d 2753 |
. . 3
⊢ (𝑧 = 𝐵 → ((𝐴 +o 𝑧) = (𝐴 ∪ ran (𝑥 ∈ 𝑧 ↦ (𝐴 +o 𝑥))) ↔ (𝐴 +o 𝐵) = (𝐴 ∪ ran (𝑥 ∈ 𝐵 ↦ (𝐴 +o 𝑥))))) |
| 25 | | oa0 8554 |
. . . 4
⊢ (𝐴 ∈ On → (𝐴 +o ∅) = 𝐴) |
| 26 | | un0 4394 |
. . . 4
⊢ (𝐴 ∪ ∅) = 𝐴 |
| 27 | 25, 26 | eqtr4di 2795 |
. . 3
⊢ (𝐴 ∈ On → (𝐴 +o ∅) = (𝐴 ∪
∅)) |
| 28 | | uneq1 4161 |
. . . . . 6
⊢ ((𝐴 +o 𝑤) = (𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥))) → ((𝐴 +o 𝑤) ∪ {(𝐴 +o 𝑤)}) = ((𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥))) ∪ {(𝐴 +o 𝑤)})) |
| 29 | | unass 4172 |
. . . . . . 7
⊢ ((𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥))) ∪ {(𝐴 +o 𝑤)}) = (𝐴 ∪ (ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥)) ∪ {(𝐴 +o 𝑤)})) |
| 30 | | rexun 4196 |
. . . . . . . . . . 11
⊢
(∃𝑥 ∈
(𝑤 ∪ {𝑤})𝑦 = (𝐴 +o 𝑥) ↔ (∃𝑥 ∈ 𝑤 𝑦 = (𝐴 +o 𝑥) ∨ ∃𝑥 ∈ {𝑤}𝑦 = (𝐴 +o 𝑥))) |
| 31 | | df-suc 6390 |
. . . . . . . . . . . 12
⊢ suc 𝑤 = (𝑤 ∪ {𝑤}) |
| 32 | 31 | rexeqi 3325 |
. . . . . . . . . . 11
⊢
(∃𝑥 ∈ suc
𝑤𝑦 = (𝐴 +o 𝑥) ↔ ∃𝑥 ∈ (𝑤 ∪ {𝑤})𝑦 = (𝐴 +o 𝑥)) |
| 33 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥)) = (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥)) |
| 34 | 33 | elrnmpt 5969 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ V → (𝑦 ∈ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥)) ↔ ∃𝑥 ∈ 𝑤 𝑦 = (𝐴 +o 𝑥))) |
| 35 | 34 | elv 3485 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥)) ↔ ∃𝑥 ∈ 𝑤 𝑦 = (𝐴 +o 𝑥)) |
| 36 | | velsn 4642 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ {(𝐴 +o 𝑤)} ↔ 𝑦 = (𝐴 +o 𝑤)) |
| 37 | | vex 3484 |
. . . . . . . . . . . . . 14
⊢ 𝑤 ∈ V |
| 38 | | oveq2 7439 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑤 → (𝐴 +o 𝑥) = (𝐴 +o 𝑤)) |
| 39 | 38 | eqeq2d 2748 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑤 → (𝑦 = (𝐴 +o 𝑥) ↔ 𝑦 = (𝐴 +o 𝑤))) |
| 40 | 37, 39 | rexsn 4682 |
. . . . . . . . . . . . 13
⊢
(∃𝑥 ∈
{𝑤}𝑦 = (𝐴 +o 𝑥) ↔ 𝑦 = (𝐴 +o 𝑤)) |
| 41 | 36, 40 | bitr4i 278 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ {(𝐴 +o 𝑤)} ↔ ∃𝑥 ∈ {𝑤}𝑦 = (𝐴 +o 𝑥)) |
| 42 | 35, 41 | orbi12i 915 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥)) ∨ 𝑦 ∈ {(𝐴 +o 𝑤)}) ↔ (∃𝑥 ∈ 𝑤 𝑦 = (𝐴 +o 𝑥) ∨ ∃𝑥 ∈ {𝑤}𝑦 = (𝐴 +o 𝑥))) |
| 43 | 30, 32, 42 | 3bitr4i 303 |
. . . . . . . . . 10
⊢
(∃𝑥 ∈ suc
𝑤𝑦 = (𝐴 +o 𝑥) ↔ (𝑦 ∈ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥)) ∨ 𝑦 ∈ {(𝐴 +o 𝑤)})) |
| 44 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ suc 𝑤 ↦ (𝐴 +o 𝑥)) = (𝑥 ∈ suc 𝑤 ↦ (𝐴 +o 𝑥)) |
| 45 | | ovex 7464 |
. . . . . . . . . . 11
⊢ (𝐴 +o 𝑥) ∈ V |
| 46 | 44, 45 | elrnmpti 5973 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ran (𝑥 ∈ suc 𝑤 ↦ (𝐴 +o 𝑥)) ↔ ∃𝑥 ∈ suc 𝑤𝑦 = (𝐴 +o 𝑥)) |
| 47 | | elun 4153 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥)) ∪ {(𝐴 +o 𝑤)}) ↔ (𝑦 ∈ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥)) ∨ 𝑦 ∈ {(𝐴 +o 𝑤)})) |
| 48 | 43, 46, 47 | 3bitr4i 303 |
. . . . . . . . 9
⊢ (𝑦 ∈ ran (𝑥 ∈ suc 𝑤 ↦ (𝐴 +o 𝑥)) ↔ 𝑦 ∈ (ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥)) ∪ {(𝐴 +o 𝑤)})) |
| 49 | 48 | eqriv 2734 |
. . . . . . . 8
⊢ ran
(𝑥 ∈ suc 𝑤 ↦ (𝐴 +o 𝑥)) = (ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥)) ∪ {(𝐴 +o 𝑤)}) |
| 50 | 49 | uneq2i 4165 |
. . . . . . 7
⊢ (𝐴 ∪ ran (𝑥 ∈ suc 𝑤 ↦ (𝐴 +o 𝑥))) = (𝐴 ∪ (ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥)) ∪ {(𝐴 +o 𝑤)})) |
| 51 | 29, 50 | eqtr4i 2768 |
. . . . . 6
⊢ ((𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥))) ∪ {(𝐴 +o 𝑤)}) = (𝐴 ∪ ran (𝑥 ∈ suc 𝑤 ↦ (𝐴 +o 𝑥))) |
| 52 | 28, 51 | eqtrdi 2793 |
. . . . 5
⊢ ((𝐴 +o 𝑤) = (𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥))) → ((𝐴 +o 𝑤) ∪ {(𝐴 +o 𝑤)}) = (𝐴 ∪ ran (𝑥 ∈ suc 𝑤 ↦ (𝐴 +o 𝑥)))) |
| 53 | | oasuc 8562 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝑤 ∈ On) → (𝐴 +o suc 𝑤) = suc (𝐴 +o 𝑤)) |
| 54 | | df-suc 6390 |
. . . . . . 7
⊢ suc
(𝐴 +o 𝑤) = ((𝐴 +o 𝑤) ∪ {(𝐴 +o 𝑤)}) |
| 55 | 53, 54 | eqtrdi 2793 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝑤 ∈ On) → (𝐴 +o suc 𝑤) = ((𝐴 +o 𝑤) ∪ {(𝐴 +o 𝑤)})) |
| 56 | 55 | eqeq1d 2739 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝑤 ∈ On) → ((𝐴 +o suc 𝑤) = (𝐴 ∪ ran (𝑥 ∈ suc 𝑤 ↦ (𝐴 +o 𝑥))) ↔ ((𝐴 +o 𝑤) ∪ {(𝐴 +o 𝑤)}) = (𝐴 ∪ ran (𝑥 ∈ suc 𝑤 ↦ (𝐴 +o 𝑥))))) |
| 57 | 52, 56 | imbitrrid 246 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝑤 ∈ On) → ((𝐴 +o 𝑤) = (𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥))) → (𝐴 +o suc 𝑤) = (𝐴 ∪ ran (𝑥 ∈ suc 𝑤 ↦ (𝐴 +o 𝑥))))) |
| 58 | 57 | expcom 413 |
. . 3
⊢ (𝑤 ∈ On → (𝐴 ∈ On → ((𝐴 +o 𝑤) = (𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥))) → (𝐴 +o suc 𝑤) = (𝐴 ∪ ran (𝑥 ∈ suc 𝑤 ↦ (𝐴 +o 𝑥)))))) |
| 59 | | vex 3484 |
. . . . . . . 8
⊢ 𝑧 ∈ V |
| 60 | | oalim 8570 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ (𝑧 ∈ V ∧ Lim 𝑧)) → (𝐴 +o 𝑧) = ∪ 𝑤 ∈ 𝑧 (𝐴 +o 𝑤)) |
| 61 | 59, 60 | mpanr1 703 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ Lim 𝑧) → (𝐴 +o 𝑧) = ∪ 𝑤 ∈ 𝑧 (𝐴 +o 𝑤)) |
| 62 | 61 | ancoms 458 |
. . . . . 6
⊢ ((Lim
𝑧 ∧ 𝐴 ∈ On) → (𝐴 +o 𝑧) = ∪ 𝑤 ∈ 𝑧 (𝐴 +o 𝑤)) |
| 63 | 62 | adantr 480 |
. . . . 5
⊢ (((Lim
𝑧 ∧ 𝐴 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝐴 +o 𝑤) = (𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥)))) → (𝐴 +o 𝑧) = ∪ 𝑤 ∈ 𝑧 (𝐴 +o 𝑤)) |
| 64 | | iuneq2 5011 |
. . . . . 6
⊢
(∀𝑤 ∈
𝑧 (𝐴 +o 𝑤) = (𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥))) → ∪ 𝑤 ∈ 𝑧 (𝐴 +o 𝑤) = ∪ 𝑤 ∈ 𝑧 (𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥)))) |
| 65 | 64 | adantl 481 |
. . . . 5
⊢ (((Lim
𝑧 ∧ 𝐴 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝐴 +o 𝑤) = (𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥)))) → ∪ 𝑤 ∈ 𝑧 (𝐴 +o 𝑤) = ∪ 𝑤 ∈ 𝑧 (𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥)))) |
| 66 | | iunun 5093 |
. . . . . . 7
⊢ ∪ 𝑤 ∈ 𝑧 (𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥))) = (∪
𝑤 ∈ 𝑧 𝐴 ∪ ∪
𝑤 ∈ 𝑧 ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥))) |
| 67 | | 0ellim 6447 |
. . . . . . . . 9
⊢ (Lim
𝑧 → ∅ ∈
𝑧) |
| 68 | | ne0i 4341 |
. . . . . . . . 9
⊢ (∅
∈ 𝑧 → 𝑧 ≠ ∅) |
| 69 | | iunconst 5001 |
. . . . . . . . 9
⊢ (𝑧 ≠ ∅ → ∪ 𝑤 ∈ 𝑧 𝐴 = 𝐴) |
| 70 | 67, 68, 69 | 3syl 18 |
. . . . . . . 8
⊢ (Lim
𝑧 → ∪ 𝑤 ∈ 𝑧 𝐴 = 𝐴) |
| 71 | | df-rex 3071 |
. . . . . . . . . . . . . 14
⊢
(∃𝑥 ∈
𝑤 𝑦 = (𝐴 +o 𝑥) ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝑦 = (𝐴 +o 𝑥))) |
| 72 | 35, 71 | bitri 275 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥)) ↔ ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝑦 = (𝐴 +o 𝑥))) |
| 73 | 72 | rexbii 3094 |
. . . . . . . . . . . 12
⊢
(∃𝑤 ∈
𝑧 𝑦 ∈ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥)) ↔ ∃𝑤 ∈ 𝑧 ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝑦 = (𝐴 +o 𝑥))) |
| 74 | | eluni2 4911 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ∪ 𝑧
↔ ∃𝑤 ∈
𝑧 𝑥 ∈ 𝑤) |
| 75 | 74 | anbi1i 624 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ∪ 𝑧
∧ 𝑦 = (𝐴 +o 𝑥)) ↔ (∃𝑤 ∈ 𝑧 𝑥 ∈ 𝑤 ∧ 𝑦 = (𝐴 +o 𝑥))) |
| 76 | | r19.41v 3189 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑤 ∈
𝑧 (𝑥 ∈ 𝑤 ∧ 𝑦 = (𝐴 +o 𝑥)) ↔ (∃𝑤 ∈ 𝑧 𝑥 ∈ 𝑤 ∧ 𝑦 = (𝐴 +o 𝑥))) |
| 77 | 75, 76 | bitr4i 278 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ∪ 𝑧
∧ 𝑦 = (𝐴 +o 𝑥)) ↔ ∃𝑤 ∈ 𝑧 (𝑥 ∈ 𝑤 ∧ 𝑦 = (𝐴 +o 𝑥))) |
| 78 | 77 | exbii 1848 |
. . . . . . . . . . . . 13
⊢
(∃𝑥(𝑥 ∈ ∪ 𝑧
∧ 𝑦 = (𝐴 +o 𝑥)) ↔ ∃𝑥∃𝑤 ∈ 𝑧 (𝑥 ∈ 𝑤 ∧ 𝑦 = (𝐴 +o 𝑥))) |
| 79 | | df-rex 3071 |
. . . . . . . . . . . . 13
⊢
(∃𝑥 ∈
∪ 𝑧𝑦 = (𝐴 +o 𝑥) ↔ ∃𝑥(𝑥 ∈ ∪ 𝑧 ∧ 𝑦 = (𝐴 +o 𝑥))) |
| 80 | | rexcom4 3288 |
. . . . . . . . . . . . 13
⊢
(∃𝑤 ∈
𝑧 ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝑦 = (𝐴 +o 𝑥)) ↔ ∃𝑥∃𝑤 ∈ 𝑧 (𝑥 ∈ 𝑤 ∧ 𝑦 = (𝐴 +o 𝑥))) |
| 81 | 78, 79, 80 | 3bitr4i 303 |
. . . . . . . . . . . 12
⊢
(∃𝑥 ∈
∪ 𝑧𝑦 = (𝐴 +o 𝑥) ↔ ∃𝑤 ∈ 𝑧 ∃𝑥(𝑥 ∈ 𝑤 ∧ 𝑦 = (𝐴 +o 𝑥))) |
| 82 | 73, 81 | bitr4i 278 |
. . . . . . . . . . 11
⊢
(∃𝑤 ∈
𝑧 𝑦 ∈ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥)) ↔ ∃𝑥 ∈ ∪ 𝑧𝑦 = (𝐴 +o 𝑥)) |
| 83 | | limuni 6445 |
. . . . . . . . . . . 12
⊢ (Lim
𝑧 → 𝑧 = ∪ 𝑧) |
| 84 | 83 | rexeqdv 3327 |
. . . . . . . . . . 11
⊢ (Lim
𝑧 → (∃𝑥 ∈ 𝑧 𝑦 = (𝐴 +o 𝑥) ↔ ∃𝑥 ∈ ∪ 𝑧𝑦 = (𝐴 +o 𝑥))) |
| 85 | 82, 84 | bitr4id 290 |
. . . . . . . . . 10
⊢ (Lim
𝑧 → (∃𝑤 ∈ 𝑧 𝑦 ∈ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥)) ↔ ∃𝑥 ∈ 𝑧 𝑦 = (𝐴 +o 𝑥))) |
| 86 | | eliun 4995 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ∪ 𝑤 ∈ 𝑧 ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥)) ↔ ∃𝑤 ∈ 𝑧 𝑦 ∈ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥))) |
| 87 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝑧 ↦ (𝐴 +o 𝑥)) = (𝑥 ∈ 𝑧 ↦ (𝐴 +o 𝑥)) |
| 88 | 87, 45 | elrnmpti 5973 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ran (𝑥 ∈ 𝑧 ↦ (𝐴 +o 𝑥)) ↔ ∃𝑥 ∈ 𝑧 𝑦 = (𝐴 +o 𝑥)) |
| 89 | 85, 86, 88 | 3bitr4g 314 |
. . . . . . . . 9
⊢ (Lim
𝑧 → (𝑦 ∈ ∪ 𝑤 ∈ 𝑧 ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥)) ↔ 𝑦 ∈ ran (𝑥 ∈ 𝑧 ↦ (𝐴 +o 𝑥)))) |
| 90 | 89 | eqrdv 2735 |
. . . . . . . 8
⊢ (Lim
𝑧 → ∪ 𝑤 ∈ 𝑧 ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥)) = ran (𝑥 ∈ 𝑧 ↦ (𝐴 +o 𝑥))) |
| 91 | 70, 90 | uneq12d 4169 |
. . . . . . 7
⊢ (Lim
𝑧 → (∪ 𝑤 ∈ 𝑧 𝐴 ∪ ∪
𝑤 ∈ 𝑧 ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥))) = (𝐴 ∪ ran (𝑥 ∈ 𝑧 ↦ (𝐴 +o 𝑥)))) |
| 92 | 66, 91 | eqtrid 2789 |
. . . . . 6
⊢ (Lim
𝑧 → ∪ 𝑤 ∈ 𝑧 (𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥))) = (𝐴 ∪ ran (𝑥 ∈ 𝑧 ↦ (𝐴 +o 𝑥)))) |
| 93 | 92 | ad2antrr 726 |
. . . . 5
⊢ (((Lim
𝑧 ∧ 𝐴 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝐴 +o 𝑤) = (𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥)))) → ∪ 𝑤 ∈ 𝑧 (𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥))) = (𝐴 ∪ ran (𝑥 ∈ 𝑧 ↦ (𝐴 +o 𝑥)))) |
| 94 | 63, 65, 93 | 3eqtrd 2781 |
. . . 4
⊢ (((Lim
𝑧 ∧ 𝐴 ∈ On) ∧ ∀𝑤 ∈ 𝑧 (𝐴 +o 𝑤) = (𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥)))) → (𝐴 +o 𝑧) = (𝐴 ∪ ran (𝑥 ∈ 𝑧 ↦ (𝐴 +o 𝑥)))) |
| 95 | 94 | exp31 419 |
. . 3
⊢ (Lim
𝑧 → (𝐴 ∈ On → (∀𝑤 ∈ 𝑧 (𝐴 +o 𝑤) = (𝐴 ∪ ran (𝑥 ∈ 𝑤 ↦ (𝐴 +o 𝑥))) → (𝐴 +o 𝑧) = (𝐴 ∪ ran (𝑥 ∈ 𝑧 ↦ (𝐴 +o 𝑥)))))) |
| 96 | 9, 14, 19, 24, 27, 58, 95 | tfinds3 7886 |
. 2
⊢ (𝐵 ∈ On → (𝐴 ∈ On → (𝐴 +o 𝐵) = (𝐴 ∪ ran (𝑥 ∈ 𝐵 ↦ (𝐴 +o 𝑥))))) |
| 97 | 96 | impcom 407 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o 𝐵) = (𝐴 ∪ ran (𝑥 ∈ 𝐵 ↦ (𝐴 +o 𝑥)))) |