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	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴 ) → ( ♯ ‘ 𝐵 ) ≤ ( ♯ ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		hashss	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴 ) → ( ♯ ‘ 𝐵 ) ≤ ( ♯ ‘ 𝐴 ) )