Metamath Proof Explorer


Theorem usgrexi

Description: An arbitrary set regarded as vertices together with the set of pairs of elements of this set regarded as edges is a simple graph. (Contributed by Alexander van der Vekens, 12-Jan-2018) (Revised by AV, 5-Nov-2020) (Proof shortened by AV, 10-Nov-2021)

Ref Expression
Hypothesis usgrexi.p P = x 𝒫 V | x = 2
Assertion usgrexi V W V I P USGraph

Proof

Step Hyp Ref Expression
1 usgrexi.p P = x 𝒫 V | x = 2
2 1 usgrexilem V W I P : dom I P 1-1 x 𝒫 V | x = 2
3 1 cusgrexilem1 V W I P V
4 opiedgfv V W I P V iEdg V I P = I P
5 3 4 mpdan V W iEdg V I P = I P
6 5 dmeqd V W dom iEdg V I P = dom I P
7 opvtxfv V W I P V Vtx V I P = V
8 3 7 mpdan V W Vtx V I P = V
9 8 pweqd V W 𝒫 Vtx V I P = 𝒫 V
10 9 rabeqdv V W x 𝒫 Vtx V I P | x = 2 = x 𝒫 V | x = 2
11 5 6 10 f1eq123d V W iEdg V I P : dom iEdg V I P 1-1 x 𝒫 Vtx V I P | x = 2 I P : dom I P 1-1 x 𝒫 V | x = 2
12 2 11 mpbird V W iEdg V I P : dom iEdg V I P 1-1 x 𝒫 Vtx V I P | x = 2
13 opex V I P V
14 eqid Vtx V I P = Vtx V I P
15 eqid iEdg V I P = iEdg V I P
16 14 15 isusgrs V I P V V I P USGraph iEdg V I P : dom iEdg V I P 1-1 x 𝒫 Vtx V I P | x = 2
17 13 16 mp1i V W V I P USGraph iEdg V I P : dom iEdg V I P 1-1 x 𝒫 Vtx V I P | x = 2
18 12 17 mpbird V W V I P USGraph