Metamath Proof Explorer

Theorem ccondx

Description: Index value of the df-cco slot. (Contributed by Mario Carneiro, 7-Jan-2017)

Ref Expression
Assertion ccondx 
|- ( comp ` ndx ) = ; 1 5

Proof

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