This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eltpsi

Description: Properties that determine a topological space from a construction (using no explicit indices). (Contributed by NM, 20-Oct-2012) (Revised by Mario Carneiro, 13-Aug-2015)

	Ref	Expression
Hypotheses	eltpsi.k	$⊢ K = \{⟨{Base}_{ndx}, A⟩, ⟨TopSet (ndx), J⟩\}$
	eltpsi.u	$⊢ A = ⋃ J$
	eltpsi.j	$⊢ J \in Top$
Assertion	eltpsi	$⊢ K \in TopSp$

Proof

Step	Hyp	Ref	Expression
1		eltpsi.k	$⊢ K = \{⟨{Base}_{ndx}, A⟩, ⟨TopSet (ndx), J⟩\}$
2		eltpsi.u	$⊢ A = ⋃ J$
3		eltpsi.j	$⊢ J \in Top$
4	2	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (A)$
5	3 4	mpbi	$⊢ J \in TopOn (A)$
6	1	eltpsg	$⊢ J \in TopOn (A) \to K \in TopSp$
7	5 6	ax-mp	$⊢ K \in TopSp$