Theorem difinf

Description: An infinite set A minus a finite set is infinite. (Contributed by FL, 3-Aug-2009)

	Ref	Expression
Assertion	difinf	|- ( ( -. A e. Fin /\ B e. Fin ) -> -. ( A \ B ) e. Fin )

Proof

Step	Hyp	Ref	Expression
1		unfi	|- ( ( ( A \ B ) e. Fin /\ B e. Fin ) -> ( ( A \ B ) u. B ) e. Fin )
2		undif1	|- ( ( A \ B ) u. B ) = ( A u. B )
3	2	eleq1i	|- ( ( ( A \ B ) u. B ) e. Fin <-> ( A u. B ) e. Fin )
4		unfir	|- ( ( A u. B ) e. Fin -> ( A e. Fin /\ B e. Fin ) )
5	4	simpld	|- ( ( A u. B ) e. Fin -> A e. Fin )
6	3 5	sylbi	|- ( ( ( A \ B ) u. B ) e. Fin -> A e. Fin )
7	1 6	syl	|- ( ( ( A \ B ) e. Fin /\ B e. Fin ) -> A e. Fin )
8	7	expcom	|- ( B e. Fin -> ( ( A \ B ) e. Fin -> A e. Fin ) )
9	8	con3d	|- ( B e. Fin -> ( -. A e. Fin -> -. ( A \ B ) e. Fin ) )
10	9	impcom	|- ( ( -. A e. Fin /\ B e. Fin ) -> -. ( A \ B ) e. Fin )