Metamath Proof Explorer

Theorem wrdupgr

Description: The property of being an undirected pseudograph, expressing the edges as "words". (Contributed by Mario Carneiro, 11-Mar-2015) (Revised by AV, 10-Oct-2020)

Ref Expression
Hypotheses isupgr.v ⊢ V = Vtx ⁡ G
isupgr.e ⊢ E = iEdg ⁡ G
Assertion wrdupgr ⊢ G ∈ U ∧ E ∈ Word X → G ∈ UPGraph ↔ E ∈ Word x ∈ 𝒫 V ∖ ∅ | x ≤ 2

Proof

Step Hyp Ref Expression
1 isupgr.v ⊢ V = Vtx ⁡ G
2 isupgr.e ⊢ E = iEdg ⁡ G
3 1 2 isupgr ⊢ G ∈ U → G ∈ UPGraph ↔ E : dom ⁡ E ⟶ x ∈ 𝒫 V ∖ ∅ | x ≤ 2
4 3 adantr ⊢ G ∈ U ∧ E ∈ Word X → G ∈ UPGraph ↔ 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 ∈ UPGraph ↔ E ∈ Word x ∈ 𝒫 V ∖ ∅ | x ≤ 2