Metamath Proof Explorer

Theorem rnmposs

Description: The range of an operation given by the maps-to notation as a subset. (Contributed by Thierry Arnoux, 23-May-2017)

Ref Expression
Hypothesis rnmposs.1 ⊢ F = x ∈ A , y ∈ B ⟼ C
Assertion rnmposs ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ D → ran ⁡ F ⊆ D

Proof

Step Hyp Ref Expression
1 rnmposs.1 ⊢ F = x ∈ A , y ∈ B ⟼ C
2 1 rnmpo ⊢ ran ⁡ F = z | ∃ x ∈ A ∃ y ∈ B z = C
3 2 eqabri ⊢ z ∈ ran ⁡ F ↔ ∃ x ∈ A ∃ y ∈ B z = C
4 2r19.29 ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ D ∧ ∃ x ∈ A ∃ y ∈ B z = C → ∃ x ∈ A ∃ y ∈ B C ∈ D ∧ z = C
5 eleq1 ⊢ z = C → z ∈ D ↔ C ∈ D
6 5 biimparc ⊢ C ∈ D ∧ z = C → z ∈ D
7 6 a1i ⊢ x ∈ A ∧ y ∈ B → C ∈ D ∧ z = C → z ∈ D
8 7 rexlimivv ⊢ ∃ x ∈ A ∃ y ∈ B C ∈ D ∧ z = C → z ∈ D
9 4 8 syl ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ D ∧ ∃ x ∈ A ∃ y ∈ B z = C → z ∈ D
10 9 ex ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ D → ∃ x ∈ A ∃ y ∈ B z = C → z ∈ D
11 3 10 biimtrid ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ D → z ∈ ran ⁡ F → z ∈ D
12 11 ssrdv ⊢ ∀ x ∈ A ∀ y ∈ B C ∈ D → ran ⁡ F ⊆ D