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∈GNeighbVtxv
4 1 fvexi ⊢V∈V
5 hash1snb ⊢V∈V→V=1↔∃nV=n
6 4 5 ax-mp ⊢V=1↔∃nV=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 ⊢∃nV=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∖vn∈GNeighbVtxv↔∀n∈∅n∈GNeighbVtxv
22 3 21 mpbiri ⊢V=1∧v∈V→∀n∈V∖vn∈GNeighbVtxv
23 1 uvtxel ⊢v∈UnivVtx⁡G↔v∈V∧∀n∈V∖vn∈GNeighbVtxv
24 2 22 23 sylanbrc ⊢V=1∧v∈V→v∈UnivVtx⁡G
25 24 ralrimiva ⊢V=1→∀v∈Vv∈UnivVtx⁡G
26 1 cplgr1vlem ⊢V=1→G∈V
27 1 iscplgr ⊢G∈V→G∈ComplGraph↔∀v∈Vv∈UnivVtx⁡G
28 26 27 syl ⊢V=1→G∈ComplGraph↔∀v∈Vv∈UnivVtx⁡G
29 25 28 mpbird ⊢V=1→G∈ComplGraph