Theorem hashsnle1

Description: The size of a singleton is less than or equal to 1. (Contributed by AV, 23-Feb-2021)

	Ref	Expression
Assertion	hashsnle1	⊢ ( ♯ ‘ { 𝐴 } ) ≤ 1

Proof

Step	Hyp	Ref	Expression
1		hashsn01	⊢ ( ( ♯ ‘ { 𝐴 } ) = 0 ∨ ( ♯ ‘ { 𝐴 } ) = 1 )
2		0le1	⊢ 0 ≤ 1
3		breq1	⊢ ( ( ♯ ‘ { 𝐴 } ) = 0 → ( ( ♯ ‘ { 𝐴 } ) ≤ 1 ↔ 0 ≤ 1 ) )
4	2 3	mpbiri	⊢ ( ( ♯ ‘ { 𝐴 } ) = 0 → ( ♯ ‘ { 𝐴 } ) ≤ 1 )
5		1le1	⊢ 1 ≤ 1
6		breq1	⊢ ( ( ♯ ‘ { 𝐴 } ) = 1 → ( ( ♯ ‘ { 𝐴 } ) ≤ 1 ↔ 1 ≤ 1 ) )
7	5 6	mpbiri	⊢ ( ( ♯ ‘ { 𝐴 } ) = 1 → ( ♯ ‘ { 𝐴 } ) ≤ 1 )
8	4 7	jaoi	⊢ ( ( ( ♯ ‘ { 𝐴 } ) = 0 ∨ ( ♯ ‘ { 𝐴 } ) = 1 ) → ( ♯ ‘ { 𝐴 } ) ≤ 1 )
9	1 8	ax-mp	⊢ ( ♯ ‘ { 𝐴 } ) ≤ 1