This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem upgruhgr

Description: An undirected pseudograph is an undirected hypergraph. (Contributed by Alexander van der Vekens, 27-Dec-2017) (Revised by AV, 10-Oct-2020)

Ref Expression
Assertion upgruhgr ( 𝐺 ∈ UPGraph → 𝐺 ∈ UHGraph )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
3 1 2 upgrf ⊢ ( 𝐺 ∈ UPGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
4 ssrab2 ⊢ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ⊆ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } )
5 fss ⊢ ( ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ∧ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ⊆ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) )
6 3 4 5 sylancl ⊢ ( 𝐺 ∈ UPGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) )
7 1 2 isuhgr ⊢ ( 𝐺 ∈ UPGraph → ( 𝐺 ∈ UHGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ) )
8 6 7 mpbird ⊢ ( 𝐺 ∈ UPGraph → 𝐺 ∈ UHGraph )