Theorem edgfndxid

Description: The value of the edge function extractor is the value of the corresponding slot of the structure. (Contributed by AV, 21-Sep-2020)

	Ref	Expression
Assertion	edgfndxid	⊢ ( 𝐺 ∈ 𝑉 → ( .ef ‘ 𝐺 ) = ( 𝐺 ‘ ( .ef ‘ ndx ) ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝐺 ∈ 𝑉 → 𝐺 ∈ 𝑉 )
2		df-edgf	⊢ .ef = Slot ; 1 8
3		1nn0	⊢ 1 ∈ ℕ0
4		8nn	⊢ 8 ∈ ℕ
5	3 4	decnncl	⊢ ; 1 8 ∈ ℕ
6	1 2 5	strndxid	⊢ ( 𝐺 ∈ 𝑉 → ( 𝐺 ‘ ( .ef ‘ ndx ) ) = ( .ef ‘ 𝐺 ) )
7	6	eqcomd	⊢ ( 𝐺 ∈ 𝑉 → ( .ef ‘ 𝐺 ) = ( 𝐺 ‘ ( .ef ‘ ndx ) ) )