Theorem topdifinfeq

Description: Two different ways of defining the collection from Exercise 3 of Munkres p. 83. (Contributed by ML, 18-Jul-2020)

	Ref	Expression
Assertion	topdifinfeq	$$⊢\left\{x\in 𝒫A|\left(\neg A\setminus x\in \mathrm{Fin}\vee \left(A\setminus x=\varnothing \vee A\setminus x=A\right)\right)\right\}=\left\{x\in 𝒫A|\left(\neg A\setminus x\in \mathrm{Fin}\vee \left(x=\varnothing \vee x=A\right)\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		velpw	$$⊢x\in 𝒫A\leftrightarrow x\subseteq A$$
2		sseqin2	$$⊢x\subseteq A\leftrightarrow A\cap x=x$$
3	1 2	bitri	$$⊢x\in 𝒫A\leftrightarrow A\cap x=x$$
4		eqeq1	$$⊢A\cap x=x\to \left(A\cap x=\varnothing \leftrightarrow x=\varnothing \right)$$
5	3 4	sylbi	$$⊢x\in 𝒫A\to \left(A\cap x=\varnothing \leftrightarrow x=\varnothing \right)$$
6		disj3	$$⊢A\cap x=\varnothing \leftrightarrow A=A\setminus x$$
7		eqcom	$$⊢A=A\setminus x\leftrightarrow A\setminus x=A$$
8	6 7	bitri	$$⊢A\cap x=\varnothing \leftrightarrow A\setminus x=A$$
9	5 8	bitr3di	$$⊢x\in 𝒫A\to \left(x=\varnothing \leftrightarrow A\setminus x=A\right)$$
10		eqss	$$⊢x=A\leftrightarrow \left(x\subseteq A\wedge A\subseteq x\right)$$
11		ssdif0	$$⊢A\subseteq x\leftrightarrow A\setminus x=\varnothing$$
12	11	bicomi	$$⊢A\setminus x=\varnothing \leftrightarrow A\subseteq x$$
13	1 12	anbi12i	$$⊢\left(x\in 𝒫A\wedge A\setminus x=\varnothing \right)\leftrightarrow \left(x\subseteq A\wedge A\subseteq x\right)$$
14	10 13	bitr4i	$$⊢x=A\leftrightarrow \left(x\in 𝒫A\wedge A\setminus x=\varnothing \right)$$
15	14	baib	$$⊢x\in 𝒫A\to \left(x=A\leftrightarrow A\setminus x=\varnothing \right)$$
16	9 15	orbi12d	$$⊢x\in 𝒫A\to \left(\left(x=\varnothing \vee x=A\right)\leftrightarrow \left(A\setminus x=A\vee A\setminus x=\varnothing \right)\right)$$
17		orcom	$$⊢\left(A\setminus x=A\vee A\setminus x=\varnothing \right)\leftrightarrow \left(A\setminus x=\varnothing \vee A\setminus x=A\right)$$
18	16 17	bitrdi	$$⊢x\in 𝒫A\to \left(\left(x=\varnothing \vee x=A\right)\leftrightarrow \left(A\setminus x=\varnothing \vee A\setminus x=A\right)\right)$$
19	18	orbi2d	$$⊢x\in 𝒫A\to \left(\left(\neg A\setminus x\in \mathrm{Fin}\vee \left(x=\varnothing \vee x=A\right)\right)\leftrightarrow \left(\neg A\setminus x\in \mathrm{Fin}\vee \left(A\setminus x=\varnothing \vee A\setminus x=A\right)\right)\right)$$
20	19	bicomd	$$⊢x\in 𝒫A\to \left(\left(\neg A\setminus x\in \mathrm{Fin}\vee \left(A\setminus x=\varnothing \vee A\setminus x=A\right)\right)\leftrightarrow \left(\neg A\setminus x\in \mathrm{Fin}\vee \left(x=\varnothing \vee x=A\right)\right)\right)$$
21	20	rabbiia	$$⊢\left\{x\in 𝒫A|\left(\neg A\setminus x\in \mathrm{Fin}\vee \left(A\setminus x=\varnothing \vee A\setminus x=A\right)\right)\right\}=\left\{x\in 𝒫A|\left(\neg A\setminus x\in \mathrm{Fin}\vee \left(x=\varnothing \vee x=A\right)\right)\right\}$$