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