Metamath Proof Explorer


Theorem cusgrexi

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

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

Proof

Step Hyp Ref Expression
1 usgrexi.p P = x 𝒫 V | x = 2
2 1 usgrexi V W V I P USGraph
3 1 cusgrexilem1 V W I P V
4 opvtxfv V W I P V Vtx V I P = V
5 4 eqcomd V W I P V V = Vtx V I P
6 3 5 mpdan V W V = Vtx V I P
7 6 eleq2d V W v V v Vtx V I P
8 7 biimpa V W v V v Vtx V I P
9 eldifi n V v n V
10 9 adantl V W v V n V v n V
11 3 4 mpdan V W Vtx V I P = V
12 11 eleq2d V W n Vtx V I P n V
13 12 ad2antrr V W v V n V v n Vtx V I P n V
14 10 13 mpbird V W v V n V v n Vtx V I P
15 simplr V W v V n V v v V
16 11 eleq2d V W v Vtx V I P v V
17 16 ad2antrr V W v V n V v v Vtx V I P v V
18 15 17 mpbird V W v V n V v v Vtx V I P
19 14 18 jca V W v V n V v n Vtx V I P v Vtx V I P
20 eldifsni n V v n v
21 20 adantl V W v V n V v n v
22 1 cusgrexilem2 V W v V n V v e ran I P v n e
23 edgval Edg V I P = ran iEdg V I P
24 opiedgfv V W I P V iEdg V I P = I P
25 3 24 mpdan V W iEdg V I P = I P
26 25 rneqd V W ran iEdg V I P = ran I P
27 23 26 syl5eq V W Edg V I P = ran I P
28 27 rexeqdv V W e Edg V I P v n e e ran I P v n e
29 28 ad2antrr V W v V n V v e Edg V I P v n e e ran I P v n e
30 22 29 mpbird V W v V n V v e Edg V I P v n e
31 eqid Vtx V I P = Vtx V I P
32 eqid Edg V I P = Edg V I P
33 31 32 nbgrel n V I P NeighbVtx v n Vtx V I P v Vtx V I P n v e Edg V I P v n e
34 19 21 30 33 syl3anbrc V W v V n V v n V I P NeighbVtx v
35 34 ralrimiva V W v V n V v n V I P NeighbVtx v
36 11 adantr V W v V Vtx V I P = V
37 36 difeq1d V W v V Vtx V I P v = V v
38 37 raleqdv V W v V n Vtx V I P v n V I P NeighbVtx v n V v n V I P NeighbVtx v
39 35 38 mpbird V W v V n Vtx V I P v n V I P NeighbVtx v
40 31 uvtxel v UnivVtx V I P v Vtx V I P n Vtx V I P v n V I P NeighbVtx v
41 8 39 40 sylanbrc V W v V v UnivVtx V I P
42 41 ralrimiva V W v V v UnivVtx V I P
43 11 raleqdv V W v Vtx V I P v UnivVtx V I P v V v UnivVtx V I P
44 42 43 mpbird V W v Vtx V I P v UnivVtx V I P
45 opex V I P V
46 31 iscplgr V I P V V I P ComplGraph v Vtx V I P v UnivVtx V I P
47 45 46 mp1i V W V I P ComplGraph v Vtx V I P v UnivVtx V I P
48 44 47 mpbird V W V I P ComplGraph
49 iscusgr V I P ComplUSGraph V I P USGraph V I P ComplGraph
50 2 48 49 sylanbrc V W V I P ComplUSGraph