Metamath Proof Explorer


Theorem indiscld

Description: The closed sets of an indiscrete topology. (Contributed by FL, 5-Jan-2009) (Revised by Mario Carneiro, 14-Aug-2015)

Ref Expression
Assertion indiscld Clsd A = A

Proof

Step Hyp Ref Expression
1 indistop A Top
2 indisuni I A = A
3 2 iscld A Top x Clsd A x I A I A x A
4 1 3 ax-mp x Clsd A x I A I A x A
5 simpl x I A I A x A x I A
6 dfss4 x I A I A I A x = x
7 5 6 sylib x I A I A x A I A I A x = x
8 simpr x I A I A x A I A x A
9 indislem I A = A
10 8 9 eleqtrrdi x I A I A x A I A x I A
11 elpri I A x I A I A x = I A x = I A
12 difeq2 I A x = I A I A x = I A
13 dif0 I A = I A
14 12 13 eqtrdi I A x = I A I A x = I A
15 fvex I A V
16 15 prid2 I A I A
17 16 9 eleqtri I A A
18 14 17 eqeltrdi I A x = I A I A x A
19 difeq2 I A x = I A I A I A x = I A I A
20 difid I A I A =
21 19 20 eqtrdi I A x = I A I A I A x =
22 0ex V
23 22 prid1 A
24 21 23 eqeltrdi I A x = I A I A I A x A
25 18 24 jaoi I A x = I A x = I A I A I A x A
26 10 11 25 3syl x I A I A x A I A I A x A
27 7 26 eqeltrrd x I A I A x A x A
28 4 27 sylbi x Clsd A x A
29 28 ssriv Clsd A A
30 0cld A Top Clsd A
31 1 30 ax-mp Clsd A
32 2 topcld A Top I A Clsd A
33 1 32 ax-mp I A Clsd A
34 prssi Clsd A I A Clsd A I A Clsd A
35 31 33 34 mp2an I A Clsd A
36 9 35 eqsstrri A Clsd A
37 29 36 eqssi Clsd A = A