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