Metamath Proof Explorer


Theorem umgrupgr

Description: An undirected multigraph is an undirected pseudograph. (Contributed by AV, 25-Nov-2020)

Ref Expression
Assertion umgrupgr ( 𝐺 ∈ UMGraph → 𝐺 ∈ UPGraph )

Proof

Step Hyp Ref Expression
1 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2 eqid ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
3 1 2 isumgr ( 𝐺 ∈ UMGraph → ( 𝐺 ∈ UMGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
4 id ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
5 2re 2 ∈ ℝ
6 5 leidi 2 ≤ 2
7 6 a1i ( ( ♯ ‘ 𝑥 ) = 2 → 2 ≤ 2 )
8 breq1 ( ( ♯ ‘ 𝑥 ) = 2 → ( ( ♯ ‘ 𝑥 ) ≤ 2 ↔ 2 ≤ 2 ) )
9 7 8 mpbird ( ( ♯ ‘ 𝑥 ) = 2 → ( ♯ ‘ 𝑥 ) ≤ 2 )
10 9 a1i ( 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) → ( ( ♯ ‘ 𝑥 ) = 2 → ( ♯ ‘ 𝑥 ) ≤ 2 ) )
11 10 ss2rabi { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ⊆ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 }
12 11 a1i ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } → { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ⊆ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
13 4 12 fssd ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
14 3 13 syl6bi ( 𝐺 ∈ UMGraph → ( 𝐺 ∈ UMGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) )
15 14 pm2.43i ( 𝐺 ∈ UMGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
16 1 2 isupgr ( 𝐺 ∈ UMGraph → ( 𝐺 ∈ UPGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑥 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ) )
17 15 16 mpbird ( 𝐺 ∈ UMGraph → 𝐺 ∈ UPGraph )