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 ⊢ φ → G Struct X
basvtxval.d ⊢ φ → 2 ≤ dom ⁡ G
edgfiedgval.e ⊢ φ → E ∈ Y
edgfiedgval.f ⊢ φ → ef ⁡ ndx E ∈ G
Assertion edgfiedgval ⊢ φ → iEdg ⁡ G = E

Proof

Step Hyp Ref Expression
1 basvtxval.s ⊢ φ → G Struct X
2 basvtxval.d ⊢ φ → 2 ≤ dom ⁡ G
3 edgfiedgval.e ⊢ φ → E ∈ Y
4 edgfiedgval.f ⊢ φ → ef ⁡ ndx E ∈ G
5 structn0fun ⊢ G Struct X → Fun ⁡ G ∖ ∅
6 1 5 syl ⊢ φ → Fun ⁡ G ∖ ∅
7 funiedgdmge2val ⊢ Fun ⁡ G ∖ ∅ ∧ 2 ≤ dom ⁡ G → iEdg ⁡ G = ef ⁡ G
8 6 2 7 syl2anc ⊢ φ → iEdg ⁡ G = ef ⁡ G
9 edgfid ⊢ ef = Slot ef ⁡ ndx
10 structex ⊢ G Struct X → G ∈ V
11 1 10 syl ⊢ φ → G ∈ V
12 structfung ⊢ G Struct X → Fun ⁡ G -1 -1
13 1 12 syl ⊢ φ → Fun ⁡ G -1 -1
14 9 11 13 4 3 strfv2d ⊢ φ → E = ef ⁡ G
15 8 14 eqtr4d ⊢ φ → iEdg ⁡ G = E