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