Metamath Proof Explorer

Theorem rnmptssbi

Description: The range of an operation given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses rnmptssbi.1 ⊢ Ⅎ x φ
rnmptssbi.2 ⊢ F = x ∈ A ⟼ B
rnmptssbi.3 ⊢ φ ∧ x ∈ A → B ∈ V
Assertion rnmptssbi ⊢ φ → ran ⁡ F ⊆ C ↔ ∀ x ∈ A B ∈ C

Proof

Step Hyp Ref Expression
1 rnmptssbi.1 ⊢ Ⅎ x φ
2 rnmptssbi.2 ⊢ F = x ∈ A ⟼ B
3 rnmptssbi.3 ⊢ φ ∧ x ∈ A → B ∈ V
4 nfmpt1 ⊢ Ⅎ _ x x ∈ A ⟼ B
5 2 4 nfcxfr ⊢ Ⅎ _ x F
6 5 nfrn ⊢ Ⅎ _ x ran ⁡ F
7 nfcv ⊢ Ⅎ _ x C
8 6 7 nfss ⊢ Ⅎ x ran ⁡ F ⊆ C
9 1 8 nfan ⊢ Ⅎ x φ ∧ ran ⁡ F ⊆ C
10 simplr ⊢ φ ∧ ran ⁡ F ⊆ C ∧ x ∈ A → ran ⁡ F ⊆ C
11 simpr ⊢ φ ∧ ran ⁡ F ⊆ C ∧ x ∈ A → x ∈ A
12 3 adantlr ⊢ φ ∧ ran ⁡ F ⊆ C ∧ x ∈ A → B ∈ V
13 2 11 12 elrnmpt1d ⊢ φ ∧ ran ⁡ F ⊆ C ∧ x ∈ A → B ∈ ran ⁡ F
14 10 13 sseldd ⊢ φ ∧ ran ⁡ F ⊆ C ∧ x ∈ A → B ∈ C
15 9 14 ralrimia ⊢ φ ∧ ran ⁡ F ⊆ C → ∀ x ∈ A B ∈ C
16 2 rnmptss ⊢ ∀ x ∈ A B ∈ C → ran ⁡ F ⊆ C
17 16 adantl ⊢ φ ∧ ∀ x ∈ A B ∈ C → ran ⁡ F ⊆ C
18 15 17 impbida ⊢ φ → ran ⁡ F ⊆ C ↔ ∀ x ∈ A B ∈ C