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 𝐴 → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ 𝐴 ) )