This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rnmptssbi

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

Ref Expression
Hypotheses rnmptssbi.1 ⊢ Ⅎ 𝑥 𝜑
rnmptssbi.2 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
rnmptssbi.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
Assertion rnmptssbi ( 𝜑 → ( ran 𝐹 ⊆ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 rnmptssbi.1 ⊢ Ⅎ 𝑥 𝜑
2 rnmptssbi.2 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
3 rnmptssbi.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
4 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
5 2 4 nfcxfr ⊢ Ⅎ 𝑥 𝐹
6 5 nfrn ⊢ Ⅎ 𝑥 ran 𝐹
7 nfcv ⊢ Ⅎ 𝑥 𝐶
8 6 7 nfss ⊢ Ⅎ 𝑥 ran 𝐹 ⊆ 𝐶
9 1 8 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ ran 𝐹 ⊆ 𝐶 )
10 simplr ⊢ ( ( ( 𝜑 ∧ ran 𝐹 ⊆ 𝐶 ) ∧ 𝑥 ∈ 𝐴 ) → ran 𝐹 ⊆ 𝐶 )
11 simpr ⊢ ( ( ( 𝜑 ∧ ran 𝐹 ⊆ 𝐶 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
12 3 adantlr ⊢ ( ( ( 𝜑 ∧ ran 𝐹 ⊆ 𝐶 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
13 2 11 12 elrnmpt1d ⊢ ( ( ( 𝜑 ∧ ran 𝐹 ⊆ 𝐶 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ran 𝐹 )
14 10 13 sseldd ⊢ ( ( ( 𝜑 ∧ ran 𝐹 ⊆ 𝐶 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝐶 )
15 9 14 ralrimia ⊢ ( ( 𝜑 ∧ ran 𝐹 ⊆ 𝐶 ) → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 )
16 2 rnmptss ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ran 𝐹 ⊆ 𝐶 )
17 16 adantl ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ) → ran 𝐹 ⊆ 𝐶 )
18 15 17 impbida ⊢ ( 𝜑 → ( ran 𝐹 ⊆ 𝐶 ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ) )