Metamath Proof Explorer


Theorem cplgr1v

Description: A graph with one vertex is complete. (Contributed by Alexander van der Vekens, 13-Oct-2017) (Revised by AV, 1-Nov-2020) (Revised by AV, 23-Mar-2021) (Proof shortened by AV, 14-Feb-2022)

Ref Expression
Hypothesis cplgr0v.v V = Vtx G
Assertion cplgr1v V = 1 G ComplGraph

Proof

Step Hyp Ref Expression
1 cplgr0v.v V = Vtx G
2 simpr V = 1 v V v V
3 ral0 n n G NeighbVtx v
4 1 fvexi V V
5 hash1snb V V V = 1 n V = n
6 4 5 ax-mp V = 1 n V = n
7 velsn v n v = n
8 sneq v = n v = n
9 8 difeq2d v = n n v = n n
10 difid n n =
11 9 10 eqtrdi v = n n v =
12 7 11 sylbi v n n v =
13 12 a1i V = n v n n v =
14 eleq2 V = n v V v n
15 difeq1 V = n V v = n v
16 15 eqeq1d V = n V v = n v =
17 13 14 16 3imtr4d V = n v V V v =
18 17 exlimiv n V = n v V V v =
19 6 18 sylbi V = 1 v V V v =
20 19 imp V = 1 v V V v =
21 20 raleqdv V = 1 v V n V v n G NeighbVtx v n n G NeighbVtx v
22 3 21 mpbiri V = 1 v V n V v n G NeighbVtx v
23 1 uvtxel v UnivVtx G v V n V v n G NeighbVtx v
24 2 22 23 sylanbrc V = 1 v V v UnivVtx G
25 24 ralrimiva V = 1 v V v UnivVtx G
26 1 cplgr1vlem V = 1 G V
27 1 iscplgr G V G ComplGraph v V v UnivVtx G
28 26 27 syl V = 1 G ComplGraph v V v UnivVtx G
29 25 28 mpbird V = 1 G ComplGraph