Theorem indistps2

Description: The indiscrete topology on a set A expressed as a topological space, using direct component assignments. Compare with indistps . The advantage of this version is that it is the shortest to state and easiest to work with in most situations. Theorems indistpsALT and indistps2ALT show that the two forms can be derived from each other. (Contributed by NM, 24-Oct-2012)

	Ref	Expression
Hypotheses	indistps2.a	⊢ ( Base ‘ 𝐾 ) = 𝐴
	indistps2.j	⊢ ( TopOpen ‘ 𝐾 ) = { ∅ , 𝐴 }
Assertion	indistps2	⊢ 𝐾 ∈ TopSp

Proof

Step	Hyp	Ref	Expression
1		indistps2.a	⊢ ( Base ‘ 𝐾 ) = 𝐴
2		indistps2.j	⊢ ( TopOpen ‘ 𝐾 ) = { ∅ , 𝐴 }
3		0ex	⊢ ∅ ∈ V
4		fvex	⊢ ( Base ‘ 𝐾 ) ∈ V
5	1 4	eqeltrri	⊢ 𝐴 ∈ V
6	3 5	unipr	⊢ ∪ { ∅ , 𝐴 } = ( ∅ ∪ 𝐴 )
7		uncom	⊢ ( ∅ ∪ 𝐴 ) = ( 𝐴 ∪ ∅ )
8		un0	⊢ ( 𝐴 ∪ ∅ ) = 𝐴
9	6 7 8	3eqtrri	⊢ 𝐴 = ∪ { ∅ , 𝐴 }
10		indistop	⊢ { ∅ , 𝐴 } ∈ Top
11	1 2 9 10	istpsi	⊢ 𝐾 ∈ TopSp