Metamath Proof Explorer

Theorem hashfn

Description: A function is equinumerous to its domain. (Contributed by Mario Carneiro, 12-Mar-2015)

Ref Expression
Assertion hashfn ⊢ F Fn A → F = A

Proof

Step Hyp Ref Expression
1 fndmeng ⊢ F Fn A ∧ A ∈ V → A ≈ F
2 ensym ⊢ A ≈ F → F ≈ A
3 hasheni ⊢ F ≈ A → F = A
4 1 2 3 3syl ⊢ F Fn A ∧ A ∈ V → F = A
5 dmexg ⊢ F ∈ V → dom ⁡ F ∈ V
6 fndm ⊢ F Fn A → dom ⁡ F = A
7 6 eleq1d ⊢ F Fn A → dom ⁡ F ∈ V ↔ A ∈ V
8 5 7 imbitrid ⊢ F Fn A → F ∈ V → A ∈ V
9 8 con3dimp ⊢ F Fn A ∧ ¬ A ∈ V → ¬ F ∈ V
10 fvprc ⊢ ¬ F ∈ V → F = ∅
11 9 10 syl ⊢ F Fn A ∧ ¬ A ∈ V → F = ∅
12 fvprc ⊢ ¬ A ∈ V → A = ∅
13 12 adantl ⊢ F Fn A ∧ ¬ A ∈ V → A = ∅
14 11 13 eqtr4d ⊢ F Fn A ∧ ¬ A ∈ V → F = A
15 4 14 pm2.61dan ⊢ F Fn A → F = A