Theorem nfile

Description: The size of any infinite set is always greater than or equal to the size of any set. (Contributed by AV, 13-Nov-2020)

	Ref	Expression
Assertion	nfile	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ¬ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		hashxrcl	⊢ ( 𝐴 ∈ 𝑉 → ( ♯ ‘ 𝐴 ) ∈ ℝ* )
2		pnfge	⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℝ* → ( ♯ ‘ 𝐴 ) ≤ +∞ )
3	1 2	syl	⊢ ( 𝐴 ∈ 𝑉 → ( ♯ ‘ 𝐴 ) ≤ +∞ )
4	3	3ad2ant1	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ¬ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐴 ) ≤ +∞ )
5		hashinf	⊢ ( ( 𝐵 ∈ 𝑊 ∧ ¬ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐵 ) = +∞ )
6	5	3adant1	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ¬ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐵 ) = +∞ )
7	4 6	breqtrrd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ ¬ 𝐵 ∈ Fin ) → ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) )