Metamath Proof Explorer

Theorem umgrupgr

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

Ref Expression
Assertion umgrupgr ⊢G∈UMGraph→G∈UPGraph

Proof

Step Hyp Ref Expression
1 eqid ⊢Vtx⁡G=Vtx⁡G
2 eqid ⊢iEdg⁡G=iEdg⁡G
3 1 2 isumgr ⊢G∈UMGraph→G∈UMGraph↔iEdg⁡G:dom⁡iEdg⁡G⟶x∈𝒫Vtx⁡G∖∅|x=2
4 id ⊢iEdg⁡G:dom⁡iEdg⁡G⟶x∈𝒫Vtx⁡G∖∅|x=2→iEdg⁡G:dom⁡iEdg⁡G⟶x∈𝒫Vtx⁡G∖∅|x=2
5 2re ⊢2∈ℝ
6 5 leidi ⊢2≤2
7 6 a1i ⊢x=2→2≤2
8 breq1 ⊢x=2→x≤2↔2≤2
9 7 8 mpbird ⊢x=2→x≤2
10 9 a1i ⊢x∈𝒫Vtx⁡G∖∅→x=2→x≤2
11 10 ss2rabi ⊢x∈𝒫Vtx⁡G∖∅|x=2⊆x∈𝒫Vtx⁡G∖∅|x≤2
12 11 a1i ⊢iEdg⁡G:dom⁡iEdg⁡G⟶x∈𝒫Vtx⁡G∖∅|x=2→x∈𝒫Vtx⁡G∖∅|x=2⊆x∈𝒫Vtx⁡G∖∅|x≤2
13 4 12 fssd ⊢iEdg⁡G:dom⁡iEdg⁡G⟶x∈𝒫Vtx⁡G∖∅|x=2→iEdg⁡G:dom⁡iEdg⁡G⟶x∈𝒫Vtx⁡G∖∅|x≤2
14 3 13 syl6bi ⊢G∈UMGraph→G∈UMGraph→iEdg⁡G:dom⁡iEdg⁡G⟶x∈𝒫Vtx⁡G∖∅|x≤2
15 14 pm2.43i ⊢G∈UMGraph→iEdg⁡G:dom⁡iEdg⁡G⟶x∈𝒫Vtx⁡G∖∅|x≤2
16 1 2 isupgr ⊢G∈UMGraph→G∈UPGraph↔iEdg⁡G:dom⁡iEdg⁡G⟶x∈𝒫Vtx⁡G∖∅|x≤2
17 15 16 mpbird ⊢G∈UMGraph→G∈UPGraph