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

Metamath Proof Explorer

Theorem basendxlttsetndx

Description: The index of the slot for the base set is less than 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)$