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