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 𝐾 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ , ⟨ ( le ‘ ndx ) , ⟩ }
Assertion otpstset ( 𝐽𝑉𝐽 = ( TopSet ‘ 𝐾 ) )

Proof

Step Hyp Ref Expression
1 otpsstr.w 𝐾 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ , ⟨ ( le ‘ ndx ) , ⟩ }
2 1 otpsstr 𝐾 Struct ⟨ 1 , 1 0 ⟩
3 tsetid TopSet = Slot ( TopSet ‘ ndx )
4 snsstp2 { ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ⊆ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ , ⟨ ( le ‘ ndx ) , ⟩ }
5 4 1 sseqtrri { ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ⊆ 𝐾
6 2 3 5 strfv ( 𝐽𝑉𝐽 = ( TopSet ‘ 𝐾 ) )