Theorem hashsng

Description: The size of a singleton. (Contributed by Paul Chapman, 26-Oct-2012) (Proof shortened by Mario Carneiro, 13-Feb-2013)

	Ref	Expression
Assertion	hashsng	⊢ ( 𝐴 ∈ 𝑉 → ( ♯ ‘ { 𝐴 } ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		1z	⊢ 1 ∈ ℤ
2		en2sn	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 1 ∈ ℤ ) → { 𝐴 } ≈ { 1 } )
3	1 2	mpan2	⊢ ( 𝐴 ∈ 𝑉 → { 𝐴 } ≈ { 1 } )
4		snfi	⊢ { 𝐴 } ∈ Fin
5		snfi	⊢ { 1 } ∈ Fin
6		hashen	⊢ ( ( { 𝐴 } ∈ Fin ∧ { 1 } ∈ Fin ) → ( ( ♯ ‘ { 𝐴 } ) = ( ♯ ‘ { 1 } ) ↔ { 𝐴 } ≈ { 1 } ) )
7	4 5 6	mp2an	⊢ ( ( ♯ ‘ { 𝐴 } ) = ( ♯ ‘ { 1 } ) ↔ { 𝐴 } ≈ { 1 } )
8	3 7	sylibr	⊢ ( 𝐴 ∈ 𝑉 → ( ♯ ‘ { 𝐴 } ) = ( ♯ ‘ { 1 } ) )
9		fzsn	⊢ ( 1 ∈ ℤ → ( 1 ... 1 ) = { 1 } )
10	9	fveq2d	⊢ ( 1 ∈ ℤ → ( ♯ ‘ ( 1 ... 1 ) ) = ( ♯ ‘ { 1 } ) )
11		1nn0	⊢ 1 ∈ ℕ0
12		hashfz1	⊢ ( 1 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 1 ) ) = 1 )
13	11 12	ax-mp	⊢ ( ♯ ‘ ( 1 ... 1 ) ) = 1
14	10 13	eqtr3di	⊢ ( 1 ∈ ℤ → ( ♯ ‘ { 1 } ) = 1 )
15	1 14	ax-mp	⊢ ( ♯ ‘ { 1 } ) = 1
16	8 15	eqtrdi	⊢ ( 𝐴 ∈ 𝑉 → ( ♯ ‘ { 𝐴 } ) = 1 )