Theorem 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→ ( 𝒫 𝑉 ∖ { ∅ } ) )