Metamath Proof Explorer


Theorem basendxlttsetndx

Description: The index of the slot for the base set is less then the index of the slot for the topology in an extensible structure. (Contributed by AV, 31-Oct-2024)

Ref Expression
Assertion basendxlttsetndx Base ndx < TopSet ndx

Proof

Step Hyp Ref Expression
1 1lt9 1 < 9
2 basendx Base ndx = 1
3 tsetndx TopSet ndx = 9
4 1 2 3 3brtr4i Base ndx < TopSet ndx