Metamath Proof Explorer


Theorem lngndx

Description: Index value of the "line" slot. Use ndxarg . (Contributed by Thierry Arnoux, 27-Mar-2019)

Ref Expression
Assertion lngndx Line 𝒢 ndx = 17

Proof

Step Hyp Ref Expression
1 df-lng Line 𝒢 = Slot 17
2 1nn0 1 0
3 7nn 7
4 2 3 decnncl 17
5 1 4 ndxarg Line 𝒢 ndx = 17