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→ 𝐵 → ( 𝐹 “ 𝐴 ) = 𝐵 ) |