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 x𝒫A|¬AxFinAx=Ax=A=x𝒫A|¬AxFinx=x=A

Proof

Step Hyp Ref Expression
1 velpw x𝒫AxA
2 sseqin2 xAAx=x
3 1 2 bitri x𝒫AAx=x
4 eqeq1 Ax=xAx=x=
5 3 4 sylbi x𝒫AAx=x=
6 disj3 Ax=A=Ax
7 eqcom A=AxAx=A
8 6 7 bitri Ax=Ax=A
9 5 8 bitr3di x𝒫Ax=Ax=A
10 eqss x=AxAAx
11 ssdif0 AxAx=
12 11 bicomi Ax=Ax
13 1 12 anbi12i x𝒫AAx=xAAx
14 10 13 bitr4i x=Ax𝒫AAx=
15 14 baib x𝒫Ax=AAx=
16 9 15 orbi12d x𝒫Ax=x=AAx=AAx=
17 orcom Ax=AAx=Ax=Ax=A
18 16 17 bitrdi x𝒫Ax=x=AAx=Ax=A
19 18 orbi2d x𝒫A¬AxFinx=x=A¬AxFinAx=Ax=A
20 19 bicomd x𝒫A¬AxFinAx=Ax=A¬AxFinx=x=A
21 20 rabbiia x𝒫A|¬AxFinAx=Ax=A=x𝒫A|¬AxFinx=x=A