Metamath Proof Explorer


Theorem uvtx01vtx

Description: If a graph/class has no edges, it has universal vertices if and only if it has exactly one vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 30-Oct-2020) (Revised by AV, 14-Feb-2022)

Ref Expression
Hypotheses uvtxel.v V = Vtx G
isuvtx.e E = Edg G
Assertion uvtx01vtx E = UnivVtx G V = 1

Proof

Step Hyp Ref Expression
1 uvtxel.v V = Vtx G
2 isuvtx.e E = Edg G
3 1 uvtxval UnivVtx G = v V | n V v n G NeighbVtx v
4 3 a1i E = UnivVtx G = v V | n V v n G NeighbVtx v
5 4 neeq1d E = UnivVtx G v V | n V v n G NeighbVtx v
6 rabn0 v V | n V v n G NeighbVtx v v V n V v n G NeighbVtx v
7 6 a1i E = v V | n V v n G NeighbVtx v v V n V v n G NeighbVtx v
8 falseral0 n ¬ n n V v n V v =
9 8 ex n ¬ n n V v n V v =
10 noel ¬ n
11 9 10 mpg n V v n V v =
12 ssdif0 V v V v =
13 sssn V v V = V = v
14 ne0i v V V
15 eqneqall V = V V = v
16 14 15 syl5 V = v V V = v
17 ax-1 V = v v V V = v
18 16 17 jaoi V = V = v v V V = v
19 13 18 sylbi V v v V V = v
20 12 19 sylbir V v = v V V = v
21 11 20 syl n V v n v V V = v
22 21 impcom v V n V v n V = v
23 vsnid v v
24 eleq2 V = v v V v v
25 23 24 mpbiri V = v v V
26 ralel n n
27 difeq1 V = v V v = v v
28 difid v v =
29 27 28 eqtrdi V = v V v =
30 29 raleqdv V = v n V v n n n
31 26 30 mpbiri V = v n V v n
32 25 31 jca V = v v V n V v n
33 22 32 impbii v V n V v n V = v
34 33 a1i E = v V n V v n V = v
35 34 exbidv E = v v V n V v n v V = v
36 2 eqeq1i E = Edg G =
37 nbgr0edg Edg G = G NeighbVtx v =
38 36 37 sylbi E = G NeighbVtx v =
39 38 eleq2d E = n G NeighbVtx v n
40 39 rexralbidv E = v V n V v n G NeighbVtx v v V n V v n
41 df-rex v V n V v n v v V n V v n
42 40 41 bitrdi E = v V n V v n G NeighbVtx v v v V n V v n
43 1 fvexi V V
44 hash1snb V V V = 1 v V = v
45 43 44 mp1i E = V = 1 v V = v
46 35 42 45 3bitr4d E = v V n V v n G NeighbVtx v V = 1
47 5 7 46 3bitrd E = UnivVtx G V = 1