Theorem hashssle

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	$$⊢\left(A\in \mathrm{Fin}\wedge B\subseteq A\right)\to \left|B\right|\le \left|A\right|$$

Proof

Step	Hyp	Ref	Expression
1		hashss	$$⊢\left(A\in \mathrm{Fin}\wedge B\subseteq A\right)\to \left|B\right|\le \left|A\right|$$