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