This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ (A \in Fin \land B \subseteq A) \to \|B\| \leq \|A\|$

Proof

Step	Hyp	Ref	Expression
1		hashss	$⊢ (A \in Fin \land B \subseteq A) \to \|B\| \leq \|A\|$