Metamath Proof Explorer

Theorem homndx

Description: Index value of the df-hom slot. (Contributed by Mario Carneiro, 7-Jan-2017) (New usage is discouraged.)

Ref Expression
Assertion homndx 
|- ( Hom ` ndx ) = ; 1 4

Proof

Step Hyp Ref Expression
1 df-hom 
 |-  Hom = Slot ; 1 4
2 1nn0 
 |-  1 e. NN0
3 4nn 
 |-  4 e. NN
4 2 3 decnncl 
 |-  ; 1 4 e. NN
5 1 4 ndxarg 
 |-  ( Hom ` ndx ) = ; 1 4