This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database GRAPH THEORY Undirected graphs Undirected hypergraphs uhgrfun
Description: The edge function of an undirected hypergraph is a function.
(Contributed by Alexander van der Vekens , 26-Dec-2017) (Revised by AV , 15-Dec-2020)
Ref
Expression
Hypothesis
uhgrfun.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
Assertion
uhgrfun ⊢ ( 𝐺 ∈ UHGraph → Fun 𝐸 )
Proof
Step
Hyp
Ref
Expression
1
uhgrfun.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
2
eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
3
2 1
uhgrf ⊢ ( 𝐺 ∈ UHGraph → 𝐸 : dom 𝐸 ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) )
4
3
ffund ⊢ ( 𝐺 ∈ UHGraph → Fun 𝐸 )