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 | ¬ A x Fin A x = A x = A = x 𝒫 A | ¬ A x Fin x = x = A

Proof

Step Hyp Ref Expression
1 disj3 A x = A = A x
2 eqcom A = A x A x = A
3 1 2 bitri A x = A x = A
4 velpw x 𝒫 A x A
5 sseqin2 x A A x = x
6 4 5 bitri x 𝒫 A A x = x
7 eqeq1 A x = x A x = x =
8 6 7 sylbi x 𝒫 A A x = x =
9 3 8 syl5rbbr x 𝒫 A x = A x = A
10 eqss x = A x A A x
11 ssdif0 A x A x =
12 11 bicomi A x = A x
13 4 12 anbi12i x 𝒫 A A x = x A A x
14 10 13 bitr4i x = A x 𝒫 A A x =
15 14 baib x 𝒫 A x = A A x =
16 9 15 orbi12d x 𝒫 A x = x = A A x = A A x =
17 orcom A x = A A x = A x = A x = A
18 16 17 syl6bb x 𝒫 A x = x = A A x = A x = A
19 18 orbi2d x 𝒫 A ¬ A x Fin x = x = A ¬ A x Fin A x = A x = A
20 19 bicomd x 𝒫 A ¬ A x Fin A x = A x = A ¬ A x Fin x = x = A
21 20 rabbiia x 𝒫 A | ¬ A x Fin A x = A x = A = x 𝒫 A | ¬ A x Fin x = x = A