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