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 dfss4 ⊢ x ⊆ I ⁡ A ↔ I ⁡ A ∖ I ⁡ A ∖ x = x
6 5 birani ⊢ x ⊆ I ⁡ A ∧ I ⁡ A ∖ x ∈ ∅ A → I ⁡ A ∖ I ⁡ A ∖ x = x
7 simpr ⊢ x ⊆ I ⁡ A ∧ I ⁡ A ∖ x ∈ ∅ A → I ⁡ A ∖ x ∈ ∅ A
8 indislem ⊢ ∅ I ⁡ A = ∅ A
9 7 8 eleqtrrdi ⊢ x ⊆ I ⁡ A ∧ I ⁡ A ∖ x ∈ ∅ A → I ⁡ A ∖ x ∈ ∅ I ⁡ A
10 elpri ⊢ I ⁡ A ∖ x ∈ ∅ I ⁡ A → I ⁡ A ∖ x = ∅ ∨ I ⁡ A ∖ x = I ⁡ A
11 difeq2 ⊢ I ⁡ A ∖ x = ∅ → I ⁡ A ∖ I ⁡ A ∖ x = I ⁡ A ∖ ∅
12 dif0 ⊢ I ⁡ A ∖ ∅ = I ⁡ A
13 11 12 eqtrdi ⊢ I ⁡ A ∖ x = ∅ → I ⁡ A ∖ I ⁡ A ∖ x = I ⁡ A
14 fvex ⊢ I ⁡ A ∈ V
15 14 prid2 ⊢ I ⁡ A ∈ ∅ I ⁡ A
16 15 8 eleqtri ⊢ I ⁡ A ∈ ∅ A
17 13 16 eqeltrdi ⊢ I ⁡ A ∖ x = ∅ → I ⁡ A ∖ I ⁡ A ∖ x ∈ ∅ A
18 difeq2 ⊢ I ⁡ A ∖ x = I ⁡ A → I ⁡ A ∖ I ⁡ A ∖ x = I ⁡ A ∖ I ⁡ A
19 difid ⊢ I ⁡ A ∖ I ⁡ A = ∅
20 18 19 eqtrdi ⊢ I ⁡ A ∖ x = I ⁡ A → I ⁡ A ∖ I ⁡ A ∖ x = ∅
21 0ex ⊢ ∅ ∈ V
22 21 prid1 ⊢ ∅ ∈ ∅ A
23 20 22 eqeltrdi ⊢ I ⁡ A ∖ x = I ⁡ A → I ⁡ A ∖ I ⁡ A ∖ x ∈ ∅ A
24 17 23 jaoi ⊢ I ⁡ A ∖ x = ∅ ∨ I ⁡ A ∖ x = I ⁡ A → I ⁡ A ∖ I ⁡ A ∖ x ∈ ∅ A
25 9 10 24 3syl ⊢ x ⊆ I ⁡ A ∧ I ⁡ A ∖ x ∈ ∅ A → I ⁡ A ∖ I ⁡ A ∖ x ∈ ∅ A
26 6 25 eqeltrrd ⊢ x ⊆ I ⁡ A ∧ I ⁡ A ∖ x ∈ ∅ A → x ∈ ∅ A
27 4 26 sylbi ⊢ x ∈ Clsd ⁡ ∅ A → x ∈ ∅ A
28 27 ssriv ⊢ Clsd ⁡ ∅ A ⊆ ∅ A
29 0cld ⊢ ∅ A ∈ Top → ∅ ∈ Clsd ⁡ ∅ A
30 1 29 ax-mp ⊢ ∅ ∈ Clsd ⁡ ∅ A
31 2 topcld ⊢ ∅ A ∈ Top → I ⁡ A ∈ Clsd ⁡ ∅ A
32 1 31 ax-mp ⊢ I ⁡ A ∈ Clsd ⁡ ∅ A
33 prssi ⊢ ∅ ∈ Clsd ⁡ ∅ A ∧ I ⁡ A ∈ Clsd ⁡ ∅ A → ∅ I ⁡ A ⊆ Clsd ⁡ ∅ A
34 30 32 33 mp2an ⊢ ∅ I ⁡ A ⊆ Clsd ⁡ ∅ A
35 8 34 eqsstrri ⊢ ∅ A ⊆ Clsd ⁡ ∅ A
36 28 35 eqssi ⊢ Clsd ⁡ ∅ A = ∅ A