Metamath Proof Explorer

Theorem baseltedgf

Description: The index value of the Base slot is less than the index value of the .ef slot. (Contributed by AV, 21-Sep-2020)

Ref Expression
Assertion baseltedgf 
|- ( Base ` ndx ) < ( .ef ` ndx )

Proof

Step Hyp Ref Expression
1 1nn 
 |-  1 e. NN
2 8nn0 
 |-  8 e. NN0
3 1nn0 
 |-  1 e. NN0
4 1lt10 
 |-  1 < ; 1 0
5 1 2 3 4 declti 
 |-  1 < ; 1 8
6 df-base 
 |-  Base = Slot 1
7 6 1 ndxarg 
 |-  ( Base ` ndx ) = 1
8 df-edgf 
 |-  .ef = Slot ; 1 8
9 8nn 
 |-  8 e. NN
10 3 9 decnncl 
 |-  ; 1 8 e. NN
11 8 10 ndxarg 
 |-  ( .ef ` ndx ) = ; 1 8
12 5 7 11 3brtr4i 
 |-  ( Base ` ndx ) < ( .ef ` ndx )