Metamath Proof Explorer

Theorem iunrnmptss

Description: A subset relation for an indexed union over the range of function expressed as a mapping. (Contributed by Thierry Arnoux, 27-Mar-2018)

Ref Expression
Hypotheses iunrnmptss.1 ⊢ y = B → C = D
iunrnmptss.2 ⊢ φ ∧ x ∈ A → B ∈ V
Assertion iunrnmptss ⊢ φ → ⋃ y ∈ ran ⁡ x ∈ A ⟼ B C ⊆ ⋃ x ∈ A D

Proof

Step Hyp Ref Expression
1 iunrnmptss.1 ⊢ y = B → C = D
2 iunrnmptss.2 ⊢ φ ∧ x ∈ A → B ∈ V
3 df-rex ⊢ ∃ y ∈ ran ⁡ x ∈ A ⟼ B z ∈ C ↔ ∃ y y ∈ ran ⁡ x ∈ A ⟼ B ∧ z ∈ C
4 2 ralrimiva ⊢ φ → ∀ x ∈ A B ∈ V
5 eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
6 5 elrnmptg ⊢ ∀ x ∈ A B ∈ V → y ∈ ran ⁡ x ∈ A ⟼ B ↔ ∃ x ∈ A y = B
7 4 6 syl ⊢ φ → y ∈ ran ⁡ x ∈ A ⟼ B ↔ ∃ x ∈ A y = B
8 7 anbi1d ⊢ φ → y ∈ ran ⁡ x ∈ A ⟼ B ∧ z ∈ C ↔ ∃ x ∈ A y = B ∧ z ∈ C
9 8 exbidv ⊢ φ → ∃ y y ∈ ran ⁡ x ∈ A ⟼ B ∧ z ∈ C ↔ ∃ y ∃ x ∈ A y = B ∧ z ∈ C
10 r19.41v ⊢ ∃ x ∈ A y = B ∧ z ∈ C ↔ ∃ x ∈ A y = B ∧ z ∈ C
11 1 eleq2d ⊢ y = B → z ∈ C ↔ z ∈ D
12 11 biimpa ⊢ y = B ∧ z ∈ C → z ∈ D
13 12 reximi ⊢ ∃ x ∈ A y = B ∧ z ∈ C → ∃ x ∈ A z ∈ D
14 10 13 sylbir ⊢ ∃ x ∈ A y = B ∧ z ∈ C → ∃ x ∈ A z ∈ D
15 14 exlimiv ⊢ ∃ y ∃ x ∈ A y = B ∧ z ∈ C → ∃ x ∈ A z ∈ D
16 9 15 syl6bi ⊢ φ → ∃ y y ∈ ran ⁡ x ∈ A ⟼ B ∧ z ∈ C → ∃ x ∈ A z ∈ D
17 3 16 syl5bi ⊢ φ → ∃ y ∈ ran ⁡ x ∈ A ⟼ B z ∈ C → ∃ x ∈ A z ∈ D
18 17 ss2abdv ⊢ φ → z | ∃ y ∈ ran ⁡ x ∈ A ⟼ B z ∈ C ⊆ z | ∃ x ∈ A z ∈ D
19 df-iun ⊢ ⋃ y ∈ ran ⁡ x ∈ A ⟼ B C = z | ∃ y ∈ ran ⁡ x ∈ A ⟼ B z ∈ C
20 df-iun ⊢ ⋃ x ∈ A D = z | ∃ x ∈ A z ∈ D
21 18 19 20 3sstr4g ⊢ φ → ⋃ y ∈ ran ⁡ x ∈ A ⟼ B C ⊆ ⋃ x ∈ A D