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	|- ( ( A e. V /\ B e. W /\ -. B e. Fin ) -> ( # ` A ) <_ ( # ` B ) )

Proof

Step	Hyp	Ref	Expression
1		hashxrcl	|- ( A e. V -> ( # ` A ) e. RR* )
2		pnfge	|- ( ( # ` A ) e. RR* -> ( # ` A ) <_ +oo )
3	1 2	syl	|- ( A e. V -> ( # ` A ) <_ +oo )
4	3	3ad2ant1	|- ( ( A e. V /\ B e. W /\ -. B e. Fin ) -> ( # ` A ) <_ +oo )
5		hashinf	|- ( ( B e. W /\ -. B e. Fin ) -> ( # ` B ) = +oo )
6	5	3adant1	|- ( ( A e. V /\ B e. W /\ -. B e. Fin ) -> ( # ` B ) = +oo )
7	4 6	breqtrrd	|- ( ( A e. V /\ B e. W /\ -. B e. Fin ) -> ( # ` A ) <_ ( # ` B ) )