This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hashfn

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

Ref Expression
Assertion hashfn ( 𝐹 Fn 𝐴 → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ 𝐴 ) )

Proof

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