Theorem basendxltunifndx

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