**Description:** The image of the domain of an onto function. (Contributed by NM, 29-Nov-2002)

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

Assertion | foima | ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( 𝐹 “ 𝐴 ) = 𝐵 ) |

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

1 | imadmrn | ⊢ ( 𝐹 “ dom 𝐹 ) = ran 𝐹 | |

2 | fof | ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 ) | |

3 | 2 | fdmd | ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → dom 𝐹 = 𝐴 ) |

4 | 3 | imaeq2d | ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( 𝐹 “ dom 𝐹 ) = ( 𝐹 “ 𝐴 ) ) |

5 | forn | ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ran 𝐹 = 𝐵 ) | |

6 | 1 4 5 | 3eqtr3a | ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( 𝐹 “ 𝐴 ) = 𝐵 ) |