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 ) )