Metamath Proof Explorer

Theorem wrdumgr

Description: The property of being an undirected multigraph, expressing the edges as "words". (Contributed by AV, 24-Nov-2020)

Ref Expression
Hypotheses isumgr.v ⊢ V = Vtx ⁡ G
isumgr.e ⊢ E = iEdg ⁡ G
Assertion wrdumgr ⊢ G ∈ U ∧ E ∈ Word X → G ∈ UMGraph ↔ E ∈ Word x ∈ 𝒫 V | x = 2

Proof

Step Hyp Ref Expression
1 isumgr.v ⊢ V = Vtx ⁡ G
2 isumgr.e ⊢ E = iEdg ⁡ G
3 1 2 isumgrs ⊢ G ∈ U → G ∈ UMGraph ↔ E : dom ⁡ E ⟶ x ∈ 𝒫 V | x = 2
4 3 adantr ⊢ G ∈ U ∧ E ∈ Word X → G ∈ UMGraph ↔ E : dom ⁡ E ⟶ x ∈ 𝒫 V | x = 2
5 wrdf ⊢ E ∈ Word X → E : 0 ..^ E ⟶ X
6 5 adantl ⊢ G ∈ U ∧ E ∈ Word X → E : 0 ..^ E ⟶ X
7 6 fdmd ⊢ G ∈ U ∧ E ∈ Word X → dom ⁡ E = 0 ..^ E
8 7 feq2d ⊢ G ∈ U ∧ E ∈ Word X → E : dom ⁡ E ⟶ x ∈ 𝒫 V | x = 2 ↔ E : 0 ..^ E ⟶ x ∈ 𝒫 V | x = 2
9 iswrdi ⊢ E : 0 ..^ E ⟶ x ∈ 𝒫 V | x = 2 → E ∈ Word x ∈ 𝒫 V | x = 2
10 wrdf ⊢ E ∈ Word x ∈ 𝒫 V | x = 2 → E : 0 ..^ E ⟶ x ∈ 𝒫 V | x = 2
11 9 10 impbii ⊢ E : 0 ..^ E ⟶ x ∈ 𝒫 V | x = 2 ↔ E ∈ Word x ∈ 𝒫 V | x = 2
12 8 11 bitrdi ⊢ G ∈ U ∧ E ∈ Word X → E : dom ⁡ E ⟶ x ∈ 𝒫 V | x = 2 ↔ E ∈ Word x ∈ 𝒫 V | x = 2
13 4 12 bitrd ⊢ G ∈ U ∧ E ∈ Word X → G ∈ UMGraph ↔ E ∈ Word x ∈ 𝒫 V | x = 2