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

Metamath Proof Explorer

Theorem rnmptssff

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

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

Proof

Step Hyp Ref Expression
1 rnmptssff.1 ⊢ Ⅎ 𝑥 𝐴
2 rnmptssff.2 ⊢ Ⅎ 𝑥 𝐶
3 rnmptssff.3 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
4 1 2 3 fmptff ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ 𝐹 : 𝐴 ⟶ 𝐶 )
5 frn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐶 → ran 𝐹 ⊆ 𝐶 )
6 4 5 sylbi ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ran 𝐹 ⊆ 𝐶 )