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

Metamath Proof Explorer

Theorem uspgrupgrushgr

Description: A graph is a simple pseudograph iff it is a pseudograph and a simple hypergraph. (Contributed by AV, 30-Nov-2020)

Ref Expression
Assertion uspgrupgrushgr ( 𝐺 ∈ USPGraph ↔ ( 𝐺 ∈ UPGraph ∧ 𝐺 ∈ USHGraph ) )

Proof

Step Hyp Ref Expression
1 uspgrupgr ⊢ ( 𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph )
2 uspgrushgr ⊢ ( 𝐺 ∈ USPGraph → 𝐺 ∈ USHGraph )
3 1 2 jca ⊢ ( 𝐺 ∈ USPGraph → ( 𝐺 ∈ UPGraph ∧ 𝐺 ∈ USHGraph ) )
4 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
5 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
6 4 5 ushgrf ⊢ ( 𝐺 ∈ USHGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) )
7 edgval ⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
8 upgredgss ⊢ ( 𝐺 ∈ UPGraph → ( Edg ‘ 𝐺 ) ⊆ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
9 7 8 eqsstrrid ⊢ ( 𝐺 ∈ UPGraph → ran ( iEdg ‘ 𝐺 ) ⊆ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
10 f1ssr ⊢ ( ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∧ ran ( iEdg ‘ 𝐺 ) ⊆ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
11 6 9 10 syl2anr ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐺 ∈ USHGraph ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
12 4 5 isuspgr ⊢ ( 𝐺 ∈ UPGraph → ( 𝐺 ∈ USPGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) )
13 12 adantr ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐺 ∈ USHGraph ) → ( 𝐺 ∈ USPGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) )
14 11 13 mpbird ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐺 ∈ USHGraph ) → 𝐺 ∈ USPGraph )
15 3 14 impbii ⊢ ( 𝐺 ∈ USPGraph ↔ ( 𝐺 ∈ UPGraph ∧ 𝐺 ∈ USHGraph ) )