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

Metamath Proof Explorer

Theorem otpstset

Description: The open sets of a topological ordered space. (Contributed by Mario Carneiro, 12-Nov-2015) (Revised by AV, 9-Sep-2021)

		Ref	Expression
	Hypothesis	otpsstr.w	$⊢ K = \{⟨{Base}_{ndx}, B⟩, ⟨TopSet (ndx), J⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩\}$
	Assertion	otpstset	$⊢ J \in V \to J = TopSet (K)$

Step	Hyp	Ref	Expression
1		otpsstr.w	$⊢ K = \{⟨{Base}_{ndx}, B⟩, ⟨TopSet (ndx), J⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩\}$
2	1	otpsstr	$⊢ K Struct ⟨1, 10⟩$
3		tsetid	$⊢ TopSet = Slot TopSet (ndx)$
4		snsstp2	$⊢ \{⟨TopSet (ndx), J⟩\} \subseteq \{⟨{Base}_{ndx}, B⟩, ⟨TopSet (ndx), J⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩\}$
5	4 1	sseqtrri	$⊢ \{⟨TopSet (ndx), J⟩\} \subseteq K$
6	2 3 5	strfv	$⊢ J \in V \to J = TopSet (K)$