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	$$⊢\left(A\in V\wedge B\in W\wedge \neg B\in \mathrm{Fin}\right)\to \left|A\right|\le \left|B\right|$$

Proof

Step	Hyp	Ref	Expression
1		hashxrcl	$$⊢A\in V\to \left|A\right|\in {ℝ}^{*}$$
2		pnfge	$$⊢\left|A\right|\in {ℝ}^{*}\to \left|A\right|\le \mathrm{+\infty }$$
3	1 2	syl	$$⊢A\in V\to \left|A\right|\le \mathrm{+\infty }$$
4	3	3ad2ant1	$$⊢\left(A\in V\wedge B\in W\wedge \neg B\in \mathrm{Fin}\right)\to \left|A\right|\le \mathrm{+\infty }$$
5		hashinf	$$⊢\left(B\in W\wedge \neg B\in \mathrm{Fin}\right)\to \left|B\right|=\mathrm{+\infty }$$
6	5	3adant1	$$⊢\left(A\in V\wedge B\in W\wedge \neg B\in \mathrm{Fin}\right)\to \left|B\right|=\mathrm{+\infty }$$
7	4 6	breqtrrd	$$⊢\left(A\in V\wedge B\in W\wedge \neg B\in \mathrm{Fin}\right)\to \left|A\right|\le \left|B\right|$$