Metamath Proof Explorer

Theorem ocndx

Description: Index value of the df-ocomp slot. (Contributed by Mario Carneiro, 25-Oct-2015) (New usage is discouraged.)

Ref Expression
Assertion ocndx 
|- ( oc ` ndx ) = ; 1 1

Proof

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