Metamath Proof Explorer

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 )