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