Description: Utility theorem: index-independent form of df-lng . (Contributed by Thierry Arnoux, 27-Mar-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | lngid | ⊢ LineG = Slot ( LineG ‘ ndx ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-lng | ⊢ LineG = Slot ; 1 7 | |
2 | 1nn0 | ⊢ 1 ∈ ℕ0 | |
3 | 7nn | ⊢ 7 ∈ ℕ | |
4 | 2 3 | decnncl | ⊢ ; 1 7 ∈ ℕ |
5 | 1 4 | ndxid | ⊢ LineG = Slot ( LineG ‘ ndx ) |