Theorem basendxltplendx

Description: The index value of the Base slot is less than the index value of the le slot. (Contributed by AV, 30-Oct-2024)

	Ref	Expression
Assertion	basendxltplendx	⊢ ( Base ‘ ndx ) < ( le ‘ ndx )

Proof

Step	Hyp	Ref	Expression
1		1lt10	⊢ 1 < ; 1 0
2		basendx	⊢ ( Base ‘ ndx ) = 1
3		plendx	⊢ ( le ‘ ndx ) = ; 1 0
4	1 2 3	3brtr4i	⊢ ( Base ‘ ndx ) < ( le ‘ ndx )