Theorem indistps2ALT

Description: The indiscrete topology on a set A expressed as a topological space, using direct component assignments. Here we show how to derive the direct component assignment version indistps2 from the structural version indistps . (Contributed by NM, 24-Oct-2012) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		indistps2ALT.a	⊢ ( Base ‘ 𝐾 ) = 𝐴
2		indistps2ALT.j	⊢ ( TopOpen ‘ 𝐾 ) = { ∅ , 𝐴 }
3		fvex	⊢ ( Base ‘ 𝐾 ) ∈ V
4	1 3	eqeltrri	⊢ 𝐴 ∈ V
5		indistopon	⊢ ( 𝐴 ∈ V → { ∅ , 𝐴 } ∈ ( TopOn ‘ 𝐴 ) )
6	4 5	ax-mp	⊢ { ∅ , 𝐴 } ∈ ( TopOn ‘ 𝐴 )
7	1	eqcomi	⊢ 𝐴 = ( Base ‘ 𝐾 )
8	2	eqcomi	⊢ { ∅ , 𝐴 } = ( TopOpen ‘ 𝐾 )
9	7 8	istps	⊢ ( 𝐾 ∈ TopSp ↔ { ∅ , 𝐴 } ∈ ( TopOn ‘ 𝐴 ) )
10	6 9	mpbir	⊢ 𝐾 ∈ TopSp