Theorem uspgrf

Description: The edge function of a simple pseudograph is a one-to-one function into unordered pairs of vertices. (Contributed by Alexander van der Vekens, 10-Aug-2017) (Revised by AV, 13-Oct-2020)

	Ref	Expression
Hypotheses	isuspgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	isuspgr.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
Assertion	uspgrf	⊢ ( 𝐺 ∈ USPGraph → 𝐸 : dom 𝐸 –1-1→ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )

Proof

Step	Hyp	Ref	Expression
1		isuspgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		isuspgr.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3	1 2	isuspgr	⊢ ( 𝐺 ∈ USPGraph → ( 𝐺 ∈ USPGraph ↔ 𝐸 : dom 𝐸 –1-1→ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) )
4	3	ibi	⊢ ( 𝐺 ∈ USPGraph → 𝐸 : dom 𝐸 –1-1→ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )