Theorem edgfiedgval

Description: The set of indexed edges of a graph represented as an extensible structure with the indexed edges in the slot for edge functions. (Contributed by AV, 14-Oct-2020) (Revised by AV, 12-Nov-2021)

	Ref	Expression
Hypotheses	basvtxval.s	⊢ ( 𝜑 → 𝐺 Struct 𝑋 )
	basvtxval.d	⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ dom 𝐺 ) )
	edgfiedgval.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑌 )
	edgfiedgval.f	⊢ ( 𝜑 → ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ ∈ 𝐺 )
Assertion	edgfiedgval	⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		basvtxval.s	⊢ ( 𝜑 → 𝐺 Struct 𝑋 )
2		basvtxval.d	⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ dom 𝐺 ) )
3		edgfiedgval.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑌 )
4		edgfiedgval.f	⊢ ( 𝜑 → ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ ∈ 𝐺 )
5		structn0fun	⊢ ( 𝐺 Struct 𝑋 → Fun ( 𝐺 ∖ { ∅ } ) )
6	1 5	syl	⊢ ( 𝜑 → Fun ( 𝐺 ∖ { ∅ } ) )
7		funiedgdmge2val	⊢ ( ( Fun ( 𝐺 ∖ { ∅ } ) ∧ 2 ≤ ( ♯ ‘ dom 𝐺 ) ) → ( iEdg ‘ 𝐺 ) = ( .ef ‘ 𝐺 ) )
8	6 2 7	syl2anc	⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = ( .ef ‘ 𝐺 ) )
9		edgfid	⊢ .ef = Slot ( .ef ‘ ndx )
10		structex	⊢ ( 𝐺 Struct 𝑋 → 𝐺 ∈ V )
11	1 10	syl	⊢ ( 𝜑 → 𝐺 ∈ V )
12		structfung	⊢ ( 𝐺 Struct 𝑋 → Fun ◡ ◡ 𝐺 )
13	1 12	syl	⊢ ( 𝜑 → Fun ◡ ◡ 𝐺 )
14	9 11 13 4 3	strfv2d	⊢ ( 𝜑 → 𝐸 = ( .ef ‘ 𝐺 ) )
15	8 14	eqtr4d	⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = 𝐸 )