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 𝐼 = ( iEdg ‘ 𝐺 )
Assertion edgiedgb ( Fun 𝐼 → ( 𝐸 ∈ ( Edg ‘ 𝐺 ) ↔ ∃ 𝑥 ∈ dom 𝐼 𝐸 = ( 𝐼𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 edgiedgb.i 𝐼 = ( iEdg ‘ 𝐺 )
2 edgval ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
3 1 eqcomi ( iEdg ‘ 𝐺 ) = 𝐼
4 3 rneqi ran ( iEdg ‘ 𝐺 ) = ran 𝐼
5 2 4 eqtri ( Edg ‘ 𝐺 ) = ran 𝐼
6 5 eleq2i ( 𝐸 ∈ ( Edg ‘ 𝐺 ) ↔ 𝐸 ∈ ran 𝐼 )
7 elrnrexdmb ( Fun 𝐼 → ( 𝐸 ∈ ran 𝐼 ↔ ∃ 𝑥 ∈ dom 𝐼 𝐸 = ( 𝐼𝑥 ) ) )
8 6 7 syl5bb ( Fun 𝐼 → ( 𝐸 ∈ ( Edg ‘ 𝐺 ) ↔ ∃ 𝑥 ∈ dom 𝐼 𝐸 = ( 𝐼𝑥 ) ) )