Description: Get an upper bound on a concretely specified finite set. Base case: singleton set. (Contributed by Mario Carneiro, 11-Feb-2015) (Proof shortened by AV, 23-Feb-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | hashsnlei | |- ( { A } e. Fin /\ ( # ` { A } ) <_ 1 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | snfi | |- { A } e. Fin |
|
| 2 | hashsnle1 | |- ( # ` { A } ) <_ 1 |
|
| 3 | 1 2 | pm3.2i | |- ( { A } e. Fin /\ ( # ` { A } ) <_ 1 ) |