Metamath Proof Explorer


Theorem umgrbi

Description: Show that an unordered pair is a valid edge in a multigraph. (Contributed by AV, 9-Mar-2021)

Ref Expression
Hypotheses umgrbi.x X V
umgrbi.y Y V
umgrbi.n X Y
Assertion umgrbi X Y x 𝒫 V | x = 2

Proof

Step Hyp Ref Expression
1 umgrbi.x X V
2 umgrbi.y Y V
3 umgrbi.n X Y
4 prssi X V Y V X Y V
5 1 2 4 mp2an X Y V
6 prex X Y V
7 6 elpw X Y 𝒫 V X Y V
8 5 7 mpbir X Y 𝒫 V
9 hashprg X V Y V X Y X Y = 2
10 3 9 mpbii X V Y V X Y = 2
11 1 2 10 mp2an X Y = 2
12 fveqeq2 x = X Y x = 2 X Y = 2
13 12 elrab X Y x 𝒫 V | x = 2 X Y 𝒫 V X Y = 2
14 8 11 13 mpbir2an X Y x 𝒫 V | x = 2