Theorem hashsn01

Description: The size of a singleton is either 0 or 1. (Contributed by AV, 23-Feb-2021)

	Ref	Expression
Assertion	hashsn01	⊢ ( ( ♯ ‘ { 𝐴 } ) = 0 ∨ ( ♯ ‘ { 𝐴 } ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		hashsng	⊢ ( 𝐴 ∈ V → ( ♯ ‘ { 𝐴 } ) = 1 )
2	1	olcd	⊢ ( 𝐴 ∈ V → ( ( ♯ ‘ { 𝐴 } ) = 0 ∨ ( ♯ ‘ { 𝐴 } ) = 1 ) )
3		snprc	⊢ ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
4	3	biimpi	⊢ ( ¬ 𝐴 ∈ V → { 𝐴 } = ∅ )
5	4	fveq2d	⊢ ( ¬ 𝐴 ∈ V → ( ♯ ‘ { 𝐴 } ) = ( ♯ ‘ ∅ ) )
6		hash0	⊢ ( ♯ ‘ ∅ ) = 0
7	5 6	eqtrdi	⊢ ( ¬ 𝐴 ∈ V → ( ♯ ‘ { 𝐴 } ) = 0 )
8	7	orcd	⊢ ( ¬ 𝐴 ∈ V → ( ( ♯ ‘ { 𝐴 } ) = 0 ∨ ( ♯ ‘ { 𝐴 } ) = 1 ) )
9	2 8	pm2.61i	⊢ ( ( ♯ ‘ { 𝐴 } ) = 0 ∨ ( ♯ ‘ { 𝐴 } ) = 1 )