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