Metamath Proof Explorer

Theorem fdmrn

Description: A different way to write F is a function. (Contributed by Thierry Arnoux, 7-Dec-2016)

Ref Expression
Assertion fdmrn ⊢ Fun ⁡ F ↔ F : dom ⁡ F ⟶ ran ⁡ F

Proof

Step Hyp Ref Expression
1 ssid ⊢ ran ⁡ F ⊆ ran ⁡ F
2 df-f ⊢ F : dom ⁡ F ⟶ ran ⁡ F ↔ F Fn dom ⁡ F ∧ ran ⁡ F ⊆ ran ⁡ F
3 1 2 mpbiran2 ⊢ F : dom ⁡ F ⟶ ran ⁡ F ↔ F Fn dom ⁡ F
4 eqid ⊢ dom ⁡ F = dom ⁡ F
5 df-fn ⊢ F Fn dom ⁡ F ↔ Fun ⁡ F ∧ dom ⁡ F = dom ⁡ F
6 4 5 mpbiran2 ⊢ F Fn dom ⁡ F ↔ Fun ⁡ F
7 3 6 bitr2i ⊢ Fun ⁡ F ↔ F : dom ⁡ F ⟶ ran ⁡ F