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	|- ( # ` { A } ) <_ 1

Proof

Step	Hyp	Ref	Expression
1		hashsn01	|- ( ( # ` { A } ) = 0 \/ ( # ` { A } ) = 1 )
2		0le1	|- 0 <_ 1
3		breq1	|- ( ( # ` { A } ) = 0 -> ( ( # ` { A } ) <_ 1 <-> 0 <_ 1 ) )
4	2 3	mpbiri	|- ( ( # ` { A } ) = 0 -> ( # ` { A } ) <_ 1 )
5		1le1	|- 1 <_ 1
6		breq1	|- ( ( # ` { A } ) = 1 -> ( ( # ` { A } ) <_ 1 <-> 1 <_ 1 ) )
7	5 6	mpbiri	|- ( ( # ` { A } ) = 1 -> ( # ` { A } ) <_ 1 )
8	4 7	jaoi	|- ( ( ( # ` { A } ) = 0 \/ ( # ` { A } ) = 1 ) -> ( # ` { A } ) <_ 1 )
9	1 8	ax-mp	|- ( # ` { A } ) <_ 1