Metamath Proof Explorer


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