Theorem hashin

Description: The size of the intersection of a set and a class is less than or equal to the size of the set. (Contributed by AV, 4-Jan-2021)

	Ref	Expression
Assertion	hashin	⊢ ( 𝐴 ∈ 𝑉 → ( ♯ ‘ ( 𝐴 ∩ 𝐵 ) ) ≤ ( ♯ ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		inss1	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
2		hashss	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ) → ( ♯ ‘ ( 𝐴 ∩ 𝐵 ) ) ≤ ( ♯ ‘ 𝐴 ) )
3	1 2	mpan2	⊢ ( 𝐴 ∈ 𝑉 → ( ♯ ‘ ( 𝐴 ∩ 𝐵 ) ) ≤ ( ♯ ‘ 𝐴 ) )