indistpsx

Description: The indiscrete topology on a set A expressed as a topological space, using explicit structure component references. Compare with indistps and indistps2 . The advantage of this version is that the actual function for the structure is evident, and df-ndx is not needed, nor any other special definition outside of basic set theory. The disadvantage is that if the indices of the component definitions df-base and df-tset are changed in the future, this theorem will also have to be changed. Note: This theorem has hard-coded structure indices for demonstration purposes. It is not intended for general use; use indistps instead. (New usage is discouraged.) (Contributed by FL, 19-Jul-2006)

	Ref	Expression
Hypotheses	indistpsx.a	$⊢ A \in V$
	indistpsx.k	$⊢ K = \{⟨1, A⟩, ⟨9, \{\emptyset, A\}⟩\}$
Assertion	indistpsx	$⊢ K \in TopSp$

Proof

Step	Hyp	Ref	Expression
1		indistpsx.a	$⊢ A \in V$
2		indistpsx.k	$⊢ K = \{⟨1, A⟩, ⟨9, \{\emptyset, A\}⟩\}$
3		basendx	$⊢ {Base}_{ndx} = 1$
4	3	opeq1i	$⊢ ⟨{Base}_{ndx}, A⟩ = ⟨1, A⟩$
5		tsetndx	$⊢ TopSet (ndx) = 9$
6	5	opeq1i	$⊢ ⟨TopSet (ndx), \{\emptyset, A\}⟩ = ⟨9, \{\emptyset, A\}⟩$
7	4 6	preq12i	$⊢ \{⟨{Base}_{ndx}, A⟩, ⟨TopSet (ndx), \{\emptyset, A\}⟩\} = \{⟨1, A⟩, ⟨9, \{\emptyset, A\}⟩\}$
8	2 7	eqtr4i	$⊢ K = \{⟨{Base}_{ndx}, A⟩, ⟨TopSet (ndx), \{\emptyset, A\}⟩\}$
9		indistopon	$⊢ A \in V \to \{\emptyset, A\} \in TopOn (A)$
10	1 9	ax-mp	$⊢ \{\emptyset, A\} \in TopOn (A)$
11	10	toponunii	$⊢ A = ⋃ \{\emptyset, A\}$
12		indistop	$⊢ \{\emptyset, A\} \in Top$
13	8 11 12	eltpsi	$⊢ K \in TopSp$

Metamath Proof Explorer

Theorem indistpsx

Proof