Metamath Proof Explorer

Theorem iedgedg

Description: An indexed edge is an edge. (Contributed by AV, 19-Dec-2021)

Ref Expression
Hypothesis iedgedg.e ⊢ E = iEdg ⁡ G
Assertion iedgedg ⊢ Fun ⁡ E ∧ I ∈ dom ⁡ E → E ⁡ I ∈ Edg ⁡ G

Proof

Step Hyp Ref Expression
1 iedgedg.e ⊢ E = iEdg ⁡ G
2 fvelrn ⊢ Fun ⁡ E ∧ I ∈ dom ⁡ E → E ⁡ I ∈ ran ⁡ E
3 edgval ⊢ Edg ⁡ G = ran ⁡ iEdg ⁡ G
4 1 rneqi ⊢ ran ⁡ E = ran ⁡ iEdg ⁡ G
5 3 4 eqtr4i ⊢ Edg ⁡ G = ran ⁡ E
6 2 5 eleqtrrdi ⊢ Fun ⁡ E ∧ I ∈ dom ⁡ E → E ⁡ I ∈ Edg ⁡ G