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

Metamath Proof Explorer

Theorem usgrumgruspgr

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

Ref Expression
Assertion usgrumgruspgr ( 𝐺 ∈ USGraph ↔ ( 𝐺 ∈ UMGraph ∧ 𝐺 ∈ USPGraph ) )

Proof

Step Hyp Ref Expression
1 usgrumgr ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UMGraph )
2 usgruspgr ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ USPGraph )
3 1 2 jca ⊢ ( 𝐺 ∈ USGraph → ( 𝐺 ∈ UMGraph ∧ 𝐺 ∈ USPGraph ) )
4 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
5 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
6 4 5 uspgrf ⊢ ( 𝐺 ∈ USPGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
7 umgredgss ⊢ ( 𝐺 ∈ UMGraph → ( Edg ‘ 𝐺 ) ⊆ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
8 edgval ⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
9 prprrab ⊢ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } = { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 }
10 9 eqcomi ⊢ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } = { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 }
11 7 8 10 3sstr3g ⊢ ( 𝐺 ∈ UMGraph → ran ( iEdg ‘ 𝐺 ) ⊆ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
12 f1ssr ⊢ ( ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ∧ ran ( iEdg ‘ 𝐺 ) ⊆ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
13 6 11 12 syl2anr ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝐺 ∈ USPGraph ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
14 4 5 isusgr ⊢ ( 𝐺 ∈ UMGraph → ( 𝐺 ∈ USGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
15 14 adantr ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝐺 ∈ USPGraph ) → ( 𝐺 ∈ USGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
16 13 15 mpbird ⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝐺 ∈ USPGraph ) → 𝐺 ∈ USGraph )
17 3 16 impbii ⊢ ( 𝐺 ∈ USGraph ↔ ( 𝐺 ∈ UMGraph ∧ 𝐺 ∈ USPGraph ) )