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

Ref | Expression | ||
---|---|---|---|

Hypothesis | rnmptss.1 | ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) | |

Assertion | rnmptss | ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ran 𝐹 ⊆ 𝐶 ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | rnmptss.1 | ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) | |

2 | 1 | fmpt | ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ 𝐹 : 𝐴 ⟶ 𝐶 ) |

3 | frn | ⊢ ( 𝐹 : 𝐴 ⟶ 𝐶 → ran 𝐹 ⊆ 𝐶 ) | |

4 | 2 3 | sylbi | ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ran 𝐹 ⊆ 𝐶 ) |