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 |
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 |