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

Metamath Proof Explorer

Theorem basendxltunifndx

Description: The index of the slot for the base set is less than the index of the slot for the uniform set in an extensible structure. Formerly part of proof for tuslem . (Contributed by AV, 28-Oct-2024)

Ref Expression
Assertion basendxltunifndx ( Base ‘ ndx ) < ( UnifSet ‘ ndx )

Proof

Step Hyp Ref Expression
1 1nn ⊢ 1 ∈ ℕ
2 3nn0 ⊢ 3 ∈ ℕ0
3 1nn0 ⊢ 1 ∈ ℕ0
4 1lt10 ⊢ 1 < 1 0
5 1 2 3 4 declti ⊢ 1 < 1 3
6 basendx ⊢ ( Base ‘ ndx ) = 1
7 unifndx ⊢ ( UnifSet ‘ ndx ) = 1 3
8 5 6 7 3brtr4i ⊢ ( Base ‘ ndx ) < ( UnifSet ‘ ndx )