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

Metamath Proof Explorer

Theorem isumgrs

Description: The simplified property of being an undirected multigraph. (Contributed by AV, 24-Nov-2020)

Ref Expression
Hypotheses isumgr.v ⊢ V = Vtx ⁡ G
isumgr.e ⊢ E = iEdg ⁡ G
Assertion isumgrs ⊢ G ∈ U → G ∈ UMGraph ↔ E : dom ⁡ E ⟶ x ∈ 𝒫 V | x = 2

Proof

Step Hyp Ref Expression
1 isumgr.v ⊢ V = Vtx ⁡ G
2 isumgr.e ⊢ E = iEdg ⁡ G
3 1 2 isumgr ⊢ G ∈ U → G ∈ UMGraph ↔ E : dom ⁡ E ⟶ x ∈ 𝒫 V ∖ ∅ | x = 2
4 prprrab ⊢ x ∈ 𝒫 V ∖ ∅ | x = 2 = x ∈ 𝒫 V | x = 2
5 4 a1i ⊢ G ∈ U → x ∈ 𝒫 V ∖ ∅ | x = 2 = x ∈ 𝒫 V | x = 2
6 5 feq3d ⊢ G ∈ U → E : dom ⁡ E ⟶ x ∈ 𝒫 V ∖ ∅ | x = 2 ↔ E : dom ⁡ E ⟶ x ∈ 𝒫 V | x = 2
7 3 6 bitrd ⊢ G ∈ U → G ∈ UMGraph ↔ E : dom ⁡ E ⟶ x ∈ 𝒫 V | x = 2