This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐺 ) = 𝐸 )