Theorem difinf

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

	Ref	Expression
Assertion	difinf	$$⊢\left(\neg A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \neg A\setminus B\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		unfi	$$⊢\left(A\setminus B\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left(A\setminus B\right)\cup B\in \mathrm{Fin}$$
2		undif1	$$⊢\left(A\setminus B\right)\cup B=A\cup B$$
3	2	eleq1i	$$⊢\left(A\setminus B\right)\cup B\in \mathrm{Fin}\leftrightarrow A\cup B\in \mathrm{Fin}$$
4		unfir	$$⊢A\cup B\in \mathrm{Fin}\to \left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)$$
5	4	simpld	$$⊢A\cup B\in \mathrm{Fin}\to A\in \mathrm{Fin}$$
6	3 5	sylbi	$$⊢\left(A\setminus B\right)\cup B\in \mathrm{Fin}\to A\in \mathrm{Fin}$$
7	1 6	syl	$$⊢\left(A\setminus B\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to A\in \mathrm{Fin}$$
8	7	expcom	$$⊢B\in \mathrm{Fin}\to \left(A\setminus B\in \mathrm{Fin}\to A\in \mathrm{Fin}\right)$$
9	8	con3d	$$⊢B\in \mathrm{Fin}\to \left(\neg A\in \mathrm{Fin}\to \neg A\setminus B\in \mathrm{Fin}\right)$$
10	9	impcom	$$⊢\left(\neg A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \neg A\setminus B\in \mathrm{Fin}$$