Description: The size of a subset of a finite set is less than the size of the containing set. (Contributed by Glauco Siliprandi, 11-Dec-2019) TODO (NM): usage (2 times) should be replaced by hashss , and hashssle should be deleted afterwards.
| Ref | Expression | ||
|---|---|---|---|
| Assertion | hashssle | |- ( ( A e. Fin /\ B C_ A ) -> ( # ` B ) <_ ( # ` A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hashss | |- ( ( A e. Fin /\ B C_ A ) -> ( # ` B ) <_ ( # ` A ) ) |