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 ushgrf
Description: The edge function of an undirected simple hypergraph is a one-to-one
function into the power set of the set of vertices. (Contributed by AV , 9-Oct-2020)
Ref
Expression
Hypotheses
uhgrf.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
uhgrf.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
Assertion
ushgrf ⊢ ( 𝐺 ∈ USHGraph → 𝐸 : dom 𝐸 –1-1 → ( 𝒫 𝑉 ∖ { ∅ } ) )
Proof
Step
Hyp
Ref
Expression
1
uhgrf.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2
uhgrf.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3
1 2
isushgr ⊢ ( 𝐺 ∈ USHGraph → ( 𝐺 ∈ USHGraph ↔ 𝐸 : dom 𝐸 –1-1 → ( 𝒫 𝑉 ∖ { ∅ } ) ) )
4
3
ibi ⊢ ( 𝐺 ∈ USHGraph → 𝐸 : dom 𝐸 –1-1 → ( 𝒫 𝑉 ∖ { ∅ } ) )