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