Metamath Proof Explorer

Theorem edgiedgb

Description: A set is an edge iff it is an indexed edge. (Contributed by AV, 17-Oct-2020) (Revised by AV, 8-Dec-2021)

Ref Expression
Hypothesis edgiedgb.i ⊢ I = iEdg ⁡ G
Assertion edgiedgb ⊢ Fun ⁡ I → E ∈ Edg ⁡ G ↔ ∃ x ∈ dom ⁡ I E = I ⁡ x

Proof

Step Hyp Ref Expression
1 edgiedgb.i ⊢ I = iEdg ⁡ G
2 edgval ⊢ Edg ⁡ G = ran ⁡ iEdg ⁡ G
3 1 eqcomi ⊢ iEdg ⁡ G = I
4 3 rneqi ⊢ ran ⁡ iEdg ⁡ G = ran ⁡ I
5 2 4 eqtri ⊢ Edg ⁡ G = ran ⁡ I
6 5 eleq2i ⊢ E ∈ Edg ⁡ G ↔ E ∈ ran ⁡ I
7 elrnrexdmb ⊢ Fun ⁡ I → E ∈ ran ⁡ I ↔ ∃ x ∈ dom ⁡ I E = I ⁡ x
8 6 7 bitrid ⊢ Fun ⁡ I → E ∈ Edg ⁡ G ↔ ∃ x ∈ dom ⁡ I E = I ⁡ x