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 velpw x 𝒫 A x A
2 sseqin2 x A A x = x
3 1 2 bitri x 𝒫 A A x = x
4 eqeq1 A x = x A x = x =
5 3 4 sylbi x 𝒫 A A x = x =
6 disj3 A x = A = A x
7 eqcom A = A x A x = A
8 6 7 bitri A x = A x = A
9 5 8 bitr3di 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 1 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 bitrdi 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