This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database GRAPH THEORY Undirected graphs Undirected simple graphs 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 } )