Theorem indistop

Description: The indiscrete topology on a set A . Part of Example 2 in Munkres p. 77. (Contributed by FL, 16-Jul-2006) (Revised by Stefan Allan, 6-Nov-2008) (Revised by Mario Carneiro, 13-Aug-2015)

	Ref	Expression
Assertion	indistop	⊢ { ∅ , 𝐴 } ∈ Top

Proof

Step	Hyp	Ref	Expression
1		indislem	⊢ { ∅ , ( I ‘ 𝐴 ) } = { ∅ , 𝐴 }
2		fvex	⊢ ( I ‘ 𝐴 ) ∈ V
3		indistopon	⊢ ( ( I ‘ 𝐴 ) ∈ V → { ∅ , ( I ‘ 𝐴 ) } ∈ ( TopOn ‘ ( I ‘ 𝐴 ) ) )
4	2 3	ax-mp	⊢ { ∅ , ( I ‘ 𝐴 ) } ∈ ( TopOn ‘ ( I ‘ 𝐴 ) )
5	4	topontopi	⊢ { ∅ , ( I ‘ 𝐴 ) } ∈ Top
6	1 5	eqeltrri	⊢ { ∅ , 𝐴 } ∈ Top