Theorem indistpsALT

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

	Ref	Expression
Hypotheses	indistpsALT.a	⊢ 𝐴 ∈ V
	indistpsALT.k	⊢ 𝐾 = { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( TopSet ‘ ndx ) , { ∅ , 𝐴 } ⟩ }
Assertion	indistpsALT	⊢ 𝐾 ∈ TopSp

Proof

Step	Hyp	Ref	Expression
1		indistpsALT.a	⊢ 𝐴 ∈ V
2		indistpsALT.k	⊢ 𝐾 = { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( TopSet ‘ ndx ) , { ∅ , 𝐴 } ⟩ }
3		indistopon	⊢ ( 𝐴 ∈ V → { ∅ , 𝐴 } ∈ ( TopOn ‘ 𝐴 ) )
4		df-tset	⊢ TopSet = Slot 9
5		1lt9	⊢ 1 < 9
6		9nn	⊢ 9 ∈ ℕ
7	2 4 5 6	2strbas	⊢ ( 𝐴 ∈ V → 𝐴 = ( Base ‘ 𝐾 ) )
8	1 7	ax-mp	⊢ 𝐴 = ( Base ‘ 𝐾 )
9		prex	⊢ { ∅ , 𝐴 } ∈ V
10	2 4 5 6	2strop	⊢ ( { ∅ , 𝐴 } ∈ V → { ∅ , 𝐴 } = ( TopSet ‘ 𝐾 ) )
11	9 10	ax-mp	⊢ { ∅ , 𝐴 } = ( TopSet ‘ 𝐾 )
12	8 11	tsettps	⊢ ( { ∅ , 𝐴 } ∈ ( TopOn ‘ 𝐴 ) → 𝐾 ∈ TopSp )
13	1 3 12	mp2b	⊢ 𝐾 ∈ TopSp