| Step | Hyp | Ref
| Expression |
| 1 | | df-rex 3071 |
. . . 4
⊢
(∃𝑦 ∈ ran
(𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ∈ 𝐶 ↔ ∃𝑦(𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ 𝑧 ∈ 𝐶)) |
| 2 | | iunrnmptss.2 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
| 3 | 2 | ralrimiva 3146 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) |
| 4 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
| 5 | 4 | elrnmptg 5972 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝑉 → (𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵)) |
| 6 | 3, 5 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵)) |
| 7 | 6 | anbi1d 631 |
. . . . . 6
⊢ (𝜑 → ((𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ 𝑧 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝐶))) |
| 8 | 7 | exbidv 1921 |
. . . . 5
⊢ (𝜑 → (∃𝑦(𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ 𝑧 ∈ 𝐶) ↔ ∃𝑦(∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝐶))) |
| 9 | | r19.41v 3189 |
. . . . . . 7
⊢
(∃𝑥 ∈
𝐴 (𝑦 = 𝐵 ∧ 𝑧 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝐶)) |
| 10 | | iunrnmptss.1 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐵 → 𝐶 = 𝐷) |
| 11 | 10 | eleq2d 2827 |
. . . . . . . . 9
⊢ (𝑦 = 𝐵 → (𝑧 ∈ 𝐶 ↔ 𝑧 ∈ 𝐷)) |
| 12 | 11 | biimpa 476 |
. . . . . . . 8
⊢ ((𝑦 = 𝐵 ∧ 𝑧 ∈ 𝐶) → 𝑧 ∈ 𝐷) |
| 13 | 12 | reximi 3084 |
. . . . . . 7
⊢
(∃𝑥 ∈
𝐴 (𝑦 = 𝐵 ∧ 𝑧 ∈ 𝐶) → ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐷) |
| 14 | 9, 13 | sylbir 235 |
. . . . . 6
⊢
((∃𝑥 ∈
𝐴 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝐶) → ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐷) |
| 15 | 14 | exlimiv 1930 |
. . . . 5
⊢
(∃𝑦(∃𝑥 ∈ 𝐴 𝑦 = 𝐵 ∧ 𝑧 ∈ 𝐶) → ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐷) |
| 16 | 8, 15 | biimtrdi 253 |
. . . 4
⊢ (𝜑 → (∃𝑦(𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ 𝑧 ∈ 𝐶) → ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐷)) |
| 17 | 1, 16 | biimtrid 242 |
. . 3
⊢ (𝜑 → (∃𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ∈ 𝐶 → ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐷)) |
| 18 | 17 | ss2abdv 4066 |
. 2
⊢ (𝜑 → {𝑧 ∣ ∃𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ∈ 𝐶} ⊆ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐷}) |
| 19 | | df-iun 4993 |
. 2
⊢ ∪ 𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝐶 = {𝑧 ∣ ∃𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝑧 ∈ 𝐶} |
| 20 | | df-iun 4993 |
. 2
⊢ ∪ 𝑥 ∈ 𝐴 𝐷 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐷} |
| 21 | 18, 19, 20 | 3sstr4g 4037 |
1
⊢ (𝜑 → ∪ 𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)𝐶 ⊆ ∪
𝑥 ∈ 𝐴 𝐷) |