Theorem indistps

Description: The indiscrete topology on a set A expressed as a topological space, using implicit structure indices. The advantage of this version over indistpsx is that it is independent of the indices of the component definitions df-base and df-tset , and if they are changed in the future, this theorem will not be affected. The advantage over indistps2 is that it is easy to eliminate the hypotheses with eqid and vtoclg to result in a closed theorem. Theorems indistpsALT and indistps2ALT show that the two forms can be derived from each other. (Contributed by FL, 19-Jul-2006)

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

Proof

Step	Hyp	Ref	Expression
1		indistps.a	⊢ 𝐴 ∈ V
2		indistps.k	⊢ 𝐾 = { ⟨ ( Base ‘ ndx ) , 𝐴 ⟩ , ⟨ ( TopSet ‘ ndx ) , { ∅ , 𝐴 } ⟩ }
3		0ex	⊢ ∅ ∈ V
4	3 1	unipr	⊢ ∪ { ∅ , 𝐴 } = ( ∅ ∪ 𝐴 )
5		uncom	⊢ ( ∅ ∪ 𝐴 ) = ( 𝐴 ∪ ∅ )
6		un0	⊢ ( 𝐴 ∪ ∅ ) = 𝐴
7	4 5 6	3eqtrri	⊢ 𝐴 = ∪ { ∅ , 𝐴 }
8		indistop	⊢ { ∅ , 𝐴 } ∈ Top
9	2 7 8	eltpsi	⊢ 𝐾 ∈ TopSp