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

Metamath Proof Explorer

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 )