Metamath Proof Explorer


Theorem odrngtset

Description: The open sets of an ordered metric ring. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Hypothesis odrngstr.w W = Base ndx B + ndx + ˙ ndx · ˙ TopSet ndx J ndx ˙ dist ndx D
Assertion odrngtset J V J = TopSet W

Proof

Step Hyp Ref Expression
1 odrngstr.w W = Base ndx B + ndx + ˙ ndx · ˙ TopSet ndx J ndx ˙ dist ndx D
2 1 odrngstr W Struct 1 12
3 tsetid TopSet = Slot TopSet ndx
4 snsstp1 TopSet ndx J TopSet ndx J ndx ˙ dist ndx D
5 ssun2 TopSet ndx J ndx ˙ dist ndx D Base ndx B + ndx + ˙ ndx · ˙ TopSet ndx J ndx ˙ dist ndx D
6 5 1 sseqtrri TopSet ndx J ndx ˙ dist ndx D W
7 4 6 sstri TopSet ndx J W
8 2 3 7 strfv J V J = TopSet W