This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ { ∅ , 𝐴 } ) = { ∅ , 𝐴 }

Proof

Step Hyp Ref Expression
1 indistop ⊢ { ∅ , 𝐴 } ∈ Top
2 indisuni ⊢ ( I ‘ 𝐴 ) = ∪ { ∅ , 𝐴 }
3 2 iscld ⊢ ( { ∅ , 𝐴 } ∈ Top → ( 𝑥 ∈ ( Clsd ‘ { ∅ , 𝐴 } ) ↔ ( 𝑥 ⊆ ( I ‘ 𝐴 ) ∧ ( ( I ‘ 𝐴 ) ∖ 𝑥 ) ∈ { ∅ , 𝐴 } ) ) )
4 1 3 ax-mp ⊢ ( 𝑥 ∈ ( Clsd ‘ { ∅ , 𝐴 } ) ↔ ( 𝑥 ⊆ ( I ‘ 𝐴 ) ∧ ( ( I ‘ 𝐴 ) ∖ 𝑥 ) ∈ { ∅ , 𝐴 } ) )
5 dfss4 ⊢ ( 𝑥 ⊆ ( I ‘ 𝐴 ) ↔ ( ( I ‘ 𝐴 ) ∖ ( ( I ‘ 𝐴 ) ∖ 𝑥 ) ) = 𝑥 )
6 5 birani ⊢ ( ( 𝑥 ⊆ ( I ‘ 𝐴 ) ∧ ( ( I ‘ 𝐴 ) ∖ 𝑥 ) ∈ { ∅ , 𝐴 } ) → ( ( I ‘ 𝐴 ) ∖ ( ( I ‘ 𝐴 ) ∖ 𝑥 ) ) = 𝑥 )
7 simpr ⊢ ( ( 𝑥 ⊆ ( I ‘ 𝐴 ) ∧ ( ( I ‘ 𝐴 ) ∖ 𝑥 ) ∈ { ∅ , 𝐴 } ) → ( ( I ‘ 𝐴 ) ∖ 𝑥 ) ∈ { ∅ , 𝐴 } )
8 indislem ⊢ { ∅ , ( I ‘ 𝐴 ) } = { ∅ , 𝐴 }
9 7 8 eleqtrrdi ⊢ ( ( 𝑥 ⊆ ( I ‘ 𝐴 ) ∧ ( ( I ‘ 𝐴 ) ∖ 𝑥 ) ∈ { ∅ , 𝐴 } ) → ( ( I ‘ 𝐴 ) ∖ 𝑥 ) ∈ { ∅ , ( I ‘ 𝐴 ) } )
10 elpri ⊢ ( ( ( I ‘ 𝐴 ) ∖ 𝑥 ) ∈ { ∅ , ( I ‘ 𝐴 ) } → ( ( ( I ‘ 𝐴 ) ∖ 𝑥 ) = ∅ ∨ ( ( I ‘ 𝐴 ) ∖ 𝑥 ) = ( I ‘ 𝐴 ) ) )
11 difeq2 ⊢ ( ( ( I ‘ 𝐴 ) ∖ 𝑥 ) = ∅ → ( ( I ‘ 𝐴 ) ∖ ( ( I ‘ 𝐴 ) ∖ 𝑥 ) ) = ( ( I ‘ 𝐴 ) ∖ ∅ ) )
12 dif0 ⊢ ( ( I ‘ 𝐴 ) ∖ ∅ ) = ( I ‘ 𝐴 )
13 11 12 eqtrdi ⊢ ( ( ( I ‘ 𝐴 ) ∖ 𝑥 ) = ∅ → ( ( I ‘ 𝐴 ) ∖ ( ( I ‘ 𝐴 ) ∖ 𝑥 ) ) = ( I ‘ 𝐴 ) )
14 fvex ⊢ ( I ‘ 𝐴 ) ∈ V
15 14 prid2 ⊢ ( I ‘ 𝐴 ) ∈ { ∅ , ( I ‘ 𝐴 ) }
16 15 8 eleqtri ⊢ ( I ‘ 𝐴 ) ∈ { ∅ , 𝐴 }
17 13 16 eqeltrdi ⊢ ( ( ( I ‘ 𝐴 ) ∖ 𝑥 ) = ∅ → ( ( I ‘ 𝐴 ) ∖ ( ( I ‘ 𝐴 ) ∖ 𝑥 ) ) ∈ { ∅ , 𝐴 } )
18 difeq2 ⊢ ( ( ( I ‘ 𝐴 ) ∖ 𝑥 ) = ( I ‘ 𝐴 ) → ( ( I ‘ 𝐴 ) ∖ ( ( I ‘ 𝐴 ) ∖ 𝑥 ) ) = ( ( I ‘ 𝐴 ) ∖ ( I ‘ 𝐴 ) ) )
19 difid ⊢ ( ( I ‘ 𝐴 ) ∖ ( I ‘ 𝐴 ) ) = ∅
20 18 19 eqtrdi ⊢ ( ( ( I ‘ 𝐴 ) ∖ 𝑥 ) = ( I ‘ 𝐴 ) → ( ( I ‘ 𝐴 ) ∖ ( ( I ‘ 𝐴 ) ∖ 𝑥 ) ) = ∅ )
21 0ex ⊢ ∅ ∈ V
22 21 prid1 ⊢ ∅ ∈ { ∅ , 𝐴 }
23 20 22 eqeltrdi ⊢ ( ( ( I ‘ 𝐴 ) ∖ 𝑥 ) = ( I ‘ 𝐴 ) → ( ( I ‘ 𝐴 ) ∖ ( ( I ‘ 𝐴 ) ∖ 𝑥 ) ) ∈ { ∅ , 𝐴 } )
24 17 23 jaoi ⊢ ( ( ( ( I ‘ 𝐴 ) ∖ 𝑥 ) = ∅ ∨ ( ( I ‘ 𝐴 ) ∖ 𝑥 ) = ( I ‘ 𝐴 ) ) → ( ( I ‘ 𝐴 ) ∖ ( ( I ‘ 𝐴 ) ∖ 𝑥 ) ) ∈ { ∅ , 𝐴 } )
25 9 10 24 3syl ⊢ ( ( 𝑥 ⊆ ( I ‘ 𝐴 ) ∧ ( ( I ‘ 𝐴 ) ∖ 𝑥 ) ∈ { ∅ , 𝐴 } ) → ( ( I ‘ 𝐴 ) ∖ ( ( I ‘ 𝐴 ) ∖ 𝑥 ) ) ∈ { ∅ , 𝐴 } )
26 6 25 eqeltrrd ⊢ ( ( 𝑥 ⊆ ( I ‘ 𝐴 ) ∧ ( ( I ‘ 𝐴 ) ∖ 𝑥 ) ∈ { ∅ , 𝐴 } ) → 𝑥 ∈ { ∅ , 𝐴 } )
27 4 26 sylbi ⊢ ( 𝑥 ∈ ( Clsd ‘ { ∅ , 𝐴 } ) → 𝑥 ∈ { ∅ , 𝐴 } )
28 27 ssriv ⊢ ( Clsd ‘ { ∅ , 𝐴 } ) ⊆ { ∅ , 𝐴 }
29 0cld ⊢ ( { ∅ , 𝐴 } ∈ Top → ∅ ∈ ( Clsd ‘ { ∅ , 𝐴 } ) )
30 1 29 ax-mp ⊢ ∅ ∈ ( Clsd ‘ { ∅ , 𝐴 } )
31 2 topcld ⊢ ( { ∅ , 𝐴 } ∈ Top → ( I ‘ 𝐴 ) ∈ ( Clsd ‘ { ∅ , 𝐴 } ) )
32 1 31 ax-mp ⊢ ( I ‘ 𝐴 ) ∈ ( Clsd ‘ { ∅ , 𝐴 } )
33 prssi ⊢ ( ( ∅ ∈ ( Clsd ‘ { ∅ , 𝐴 } ) ∧ ( I ‘ 𝐴 ) ∈ ( Clsd ‘ { ∅ , 𝐴 } ) ) → { ∅ , ( I ‘ 𝐴 ) } ⊆ ( Clsd ‘ { ∅ , 𝐴 } ) )
34 30 32 33 mp2an ⊢ { ∅ , ( I ‘ 𝐴 ) } ⊆ ( Clsd ‘ { ∅ , 𝐴 } )
35 8 34 eqsstrri ⊢ { ∅ , 𝐴 } ⊆ ( Clsd ‘ { ∅ , 𝐴 } )
36 28 35 eqssi ⊢ ( Clsd ‘ { ∅ , 𝐴 } ) = { ∅ , 𝐴 }