Step | Hyp | Ref
| Expression |
1 | | df-rex 3072 |
. . . 4
⊢
(∃𝑦 ∈ ran
(𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ∈ 𝐶 ↔ ∃𝑦(𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ 𝑧 ∈ 𝐶)) |
2 | | iunrnmptss.2 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
3 | 2 | ralrimiva 3110 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) |
4 | | eqid 2740 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
5 | 4 | elrnmptg 5867 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝑉 → (𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵)) |
6 | 3, 5 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵)) |
7 | 6 | anbi1d 630 |
. . . . . 6
⊢ (𝜑 → ((𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ 𝑧 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝐶))) |
8 | 7 | exbidv 1928 |
. . . . 5
⊢ (𝜑 → (∃𝑦(𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ 𝑧 ∈ 𝐶) ↔ ∃𝑦(∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝐶))) |
9 | | r19.41v 3276 |
. . . . . . 7
⊢
(∃𝑥 ∈
𝐴 (𝑦 = 𝐵 ∧ 𝑧 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝐶)) |
10 | | iunrnmptss.1 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐵 → 𝐶 = 𝐷) |
11 | 10 | eleq2d 2826 |
. . . . . . . . 9
⊢ (𝑦 = 𝐵 → (𝑧 ∈ 𝐶 ↔ 𝑧 ∈ 𝐷)) |
12 | 11 | biimpa 477 |
. . . . . . . 8
⊢ ((𝑦 = 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝑧 ∈ 𝐷) |
13 | 12 | reximi 3177 |
. . . . . . 7
⊢
(∃𝑥 ∈
𝐴 (𝑦 = 𝐵 ∧ 𝑧 ∈ 𝐶) → ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐷) |
14 | 9, 13 | sylbir 234 |
. . . . . 6
⊢
((∃𝑥 ∈
𝐴 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝐶) → ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐷) |
15 | 14 | exlimiv 1937 |
. . . . 5
⊢
(∃𝑦(∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝐶) → ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐷) |
16 | 8, 15 | syl6bi 252 |
. . . 4
⊢ (𝜑 → (∃𝑦(𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ 𝑧 ∈ 𝐶) → ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐷)) |
17 | 1, 16 | syl5bi 241 |
. . 3
⊢ (𝜑 → (∃𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ∈ 𝐶 → ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐷)) |
18 | 17 | ss2abdv 4002 |
. 2
⊢ (𝜑 → {𝑧 ∣ ∃𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ∈ 𝐶} ⊆ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐷}) |
19 | | df-iun 4932 |
. 2
⊢ ∪ 𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝐶 = {𝑧 ∣ ∃𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ∈ 𝐶} |
20 | | df-iun 4932 |
. 2
⊢ ∪ 𝑥 ∈ 𝐴 𝐷 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐷} |
21 | 18, 19, 20 | 3sstr4g 3971 |
1
⊢ (𝜑 → ∪ 𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝐶 ⊆ ∪
𝑥 ∈ 𝐴 𝐷) |