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

Metamath Proof Explorer

Theorem uhgredgiedgb

Description: In a hypergraph, a set is an edge iff it is an indexed edge. (Contributed by AV, 17-Oct-2020)

Ref Expression
Hypothesis uhgredgiedgb.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion uhgredgiedgb ( 𝐺 ∈ UHGraph → ( 𝐸 ∈ ( Edg ‘ 𝐺 ) ↔ ∃ 𝑥 ∈ dom 𝐼 𝐸 = ( 𝐼 ‘ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 uhgredgiedgb.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
2 1 uhgrfun ⊢ ( 𝐺 ∈ UHGraph → Fun 𝐼 )
3 1 edgiedgb ⊢ ( Fun 𝐼 → ( 𝐸 ∈ ( Edg ‘ 𝐺 ) ↔ ∃ 𝑥 ∈ dom 𝐼 𝐸 = ( 𝐼 ‘ 𝑥 ) ) )
4 2 3 syl ⊢ ( 𝐺 ∈ UHGraph → ( 𝐸 ∈ ( Edg ‘ 𝐺 ) ↔ ∃ 𝑥 ∈ dom 𝐼 𝐸 = ( 𝐼 ‘ 𝑥 ) ) )