# Metamath Proof Explorer

## 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(¬{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(¬{A}\setminus {x}\in \mathrm{Fin}\vee \left({x}=\varnothing \vee {x}={A}\right)\right)\right\}$

### Proof

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