Theorem infdiffi

Description: Removing a finite set from an infinite set does not change the cardinality of the set. (Contributed by Mario Carneiro, 30-Apr-2015)

	Ref	Expression
Assertion	infdiffi	$$⊢\left(\mathrm{\omega }\preccurlyeq A\wedge B\in \mathrm{Fin}\right)\to \left(A\setminus B\right)\approx A$$

Proof

Step	Hyp	Ref	Expression
1		difeq2	$$⊢x=\varnothing \to A\setminus x=A\setminus \varnothing$$
2		dif0	$$⊢A\setminus \varnothing =A$$
3	1 2	eqtrdi	$$⊢x=\varnothing \to A\setminus x=A$$
4	3	breq1d	$$⊢x=\varnothing \to \left(\left(A\setminus x\right)\approx A\leftrightarrow A\approx A\right)$$
5	4	imbi2d	$$⊢x=\varnothing \to \left(\left(\mathrm{\omega }\preccurlyeq A\to \left(A\setminus x\right)\approx A\right)\leftrightarrow \left(\mathrm{\omega }\preccurlyeq A\to A\approx A\right)\right)$$
6		difeq2	$$⊢x=y\to A\setminus x=A\setminus y$$
7	6	breq1d	$$⊢x=y\to \left(\left(A\setminus x\right)\approx A\leftrightarrow \left(A\setminus y\right)\approx A\right)$$
8	7	imbi2d	$$⊢x=y\to \left(\left(\mathrm{\omega }\preccurlyeq A\to \left(A\setminus x\right)\approx A\right)\leftrightarrow \left(\mathrm{\omega }\preccurlyeq A\to \left(A\setminus y\right)\approx A\right)\right)$$
9		difeq2	$$⊢x=y\cup \left\{z\right\}\to A\setminus x=A\setminus \left(y\cup \left\{z\right\}\right)$$
10		difun1	$$⊢A\setminus \left(y\cup \left\{z\right\}\right)=\left(A\setminus y\right)\setminus \left\{z\right\}$$
11	9 10	eqtrdi	$$⊢x=y\cup \left\{z\right\}\to A\setminus x=\left(A\setminus y\right)\setminus \left\{z\right\}$$
12	11	breq1d	$$⊢x=y\cup \left\{z\right\}\to \left(\left(A\setminus x\right)\approx A\leftrightarrow \left(\left(A\setminus y\right)\setminus \left\{z\right\}\right)\approx A\right)$$
13	12	imbi2d	$$⊢x=y\cup \left\{z\right\}\to \left(\left(\mathrm{\omega }\preccurlyeq A\to \left(A\setminus x\right)\approx A\right)\leftrightarrow \left(\mathrm{\omega }\preccurlyeq A\to \left(\left(A\setminus y\right)\setminus \left\{z\right\}\right)\approx A\right)\right)$$
14		difeq2	$$⊢x=B\to A\setminus x=A\setminus B$$
15	14	breq1d	$$⊢x=B\to \left(\left(A\setminus x\right)\approx A\leftrightarrow \left(A\setminus B\right)\approx A\right)$$
16	15	imbi2d	$$⊢x=B\to \left(\left(\mathrm{\omega }\preccurlyeq A\to \left(A\setminus x\right)\approx A\right)\leftrightarrow \left(\mathrm{\omega }\preccurlyeq A\to \left(A\setminus B\right)\approx A\right)\right)$$
17		reldom	$$⊢\mathrm{Rel}\preccurlyeq$$
18	17	brrelex2i	$$⊢\mathrm{\omega }\preccurlyeq A\to A\in \mathrm{V}$$
19		enrefg	$$⊢A\in \mathrm{V}\to A\approx A$$
20	18 19	syl	$$⊢\mathrm{\omega }\preccurlyeq A\to A\approx A$$
21		domen2	$$⊢\left(A\setminus y\right)\approx A\to \left(\mathrm{\omega }\preccurlyeq \left(A\setminus y\right)\leftrightarrow \mathrm{\omega }\preccurlyeq A\right)$$
22	21	biimparc	$$⊢\left(\mathrm{\omega }\preccurlyeq A\wedge \left(A\setminus y\right)\approx A\right)\to \mathrm{\omega }\preccurlyeq \left(A\setminus y\right)$$
23		infdifsn	$$⊢\mathrm{\omega }\preccurlyeq \left(A\setminus y\right)\to \left(\left(A\setminus y\right)\setminus \left\{z\right\}\right)\approx \left(A\setminus y\right)$$
24	22 23	syl	$$⊢\left(\mathrm{\omega }\preccurlyeq A\wedge \left(A\setminus y\right)\approx A\right)\to \left(\left(A\setminus y\right)\setminus \left\{z\right\}\right)\approx \left(A\setminus y\right)$$
25		entr	$$⊢\left(\left(\left(A\setminus y\right)\setminus \left\{z\right\}\right)\approx \left(A\setminus y\right)\wedge \left(A\setminus y\right)\approx A\right)\to \left(\left(A\setminus y\right)\setminus \left\{z\right\}\right)\approx A$$
26	24 25	sylancom	$$⊢\left(\mathrm{\omega }\preccurlyeq A\wedge \left(A\setminus y\right)\approx A\right)\to \left(\left(A\setminus y\right)\setminus \left\{z\right\}\right)\approx A$$
27	26	ex	$$⊢\mathrm{\omega }\preccurlyeq A\to \left(\left(A\setminus y\right)\approx A\to \left(\left(A\setminus y\right)\setminus \left\{z\right\}\right)\approx A\right)$$
28	27	a2i	$$⊢\left(\mathrm{\omega }\preccurlyeq A\to \left(A\setminus y\right)\approx A\right)\to \left(\mathrm{\omega }\preccurlyeq A\to \left(\left(A\setminus y\right)\setminus \left\{z\right\}\right)\approx A\right)$$
29	28	a1i	$$⊢y\in \mathrm{Fin}\to \left(\left(\mathrm{\omega }\preccurlyeq A\to \left(A\setminus y\right)\approx A\right)\to \left(\mathrm{\omega }\preccurlyeq A\to \left(\left(A\setminus y\right)\setminus \left\{z\right\}\right)\approx A\right)\right)$$
30	5 8 13 16 20 29	findcard2	$$⊢B\in \mathrm{Fin}\to \left(\mathrm{\omega }\preccurlyeq A\to \left(A\setminus B\right)\approx A\right)$$
31	30	impcom	$$⊢\left(\mathrm{\omega }\preccurlyeq A\wedge B\in \mathrm{Fin}\right)\to \left(A\setminus B\right)\approx A$$