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