Metamath Proof Explorer


Theorem topdifinfindis

Description: Part of Exercise 3 of Munkres p. 83. The topology of all subsets x of A such that the complement of x in A is infinite, or x is the empty set, or x is all of A , is the trivial topology when A is finite. (Contributed by ML, 14-Jul-2020)

Ref Expression
Hypothesis topdifinf.t T = x 𝒫 A | ¬ A x Fin x = x = A
Assertion topdifinfindis A Fin T = A

Proof

Step Hyp Ref Expression
1 topdifinf.t T = x 𝒫 A | ¬ A x Fin x = x = A
2 nfv x A Fin
3 nfrab1 _ x x 𝒫 A | ¬ A x Fin x = x = A
4 1 3 nfcxfr _ x T
5 nfcv _ x A
6 0elpw 𝒫 A
7 eleq1a 𝒫 A x = x 𝒫 A
8 6 7 mp1i A Fin x = x 𝒫 A
9 pwidg A Fin A 𝒫 A
10 eleq1a A 𝒫 A x = A x 𝒫 A
11 9 10 syl A Fin x = A x 𝒫 A
12 8 11 jaod A Fin x = x = A x 𝒫 A
13 12 pm4.71rd A Fin x = x = A x 𝒫 A x = x = A
14 vex x V
15 14 elpr x A x = x = A
16 15 a1i A Fin x A x = x = A
17 1 rabeq2i x T x 𝒫 A ¬ A x Fin x = x = A
18 diffi A Fin A x Fin
19 biortn A x Fin x = x = A ¬ A x Fin x = x = A
20 18 19 syl A Fin x = x = A ¬ A x Fin x = x = A
21 20 anbi2d A Fin x 𝒫 A x = x = A x 𝒫 A ¬ A x Fin x = x = A
22 17 21 bitr4id A Fin x T x 𝒫 A x = x = A
23 13 16 22 3bitr4rd A Fin x T x A
24 2 4 5 23 eqrd A Fin T = A