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 e. ComplGraph )

Proof

Step Hyp Ref Expression
1 cplgr0v.v 
 |-  V = ( Vtx ` G )
2 simpr 
 |-  ( ( ( # ` V ) = 1 /\ v e. V ) -> v e. V )
3 ral0 
 |-  A. n e. (/) n e. ( G NeighbVtx v )
4 1 fvexi 
 |-  V e. _V
5 hash1snb 
 |-  ( V e. _V -> ( ( # ` V ) = 1 <-> E. n V = { n } ) )
6 4 5 ax-mp 
 |-  ( ( # ` V ) = 1 <-> E. n V = { n } )
7 velsn 
 |-  ( v e. { 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 e. { n } -> ( { n } \ { v } ) = (/) )
13 12 a1i 
 |-  ( V = { n } -> ( v e. { n } -> ( { n } \ { v } ) = (/) ) )
14 eleq2 
 |-  ( V = { n } -> ( v e. V <-> v e. { 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 e. V -> ( V \ { v } ) = (/) ) )
18 17 exlimiv 
 |-  ( E. n V = { n } -> ( v e. V -> ( V \ { v } ) = (/) ) )
19 6 18 sylbi 
 |-  ( ( # ` V ) = 1 -> ( v e. V -> ( V \ { v } ) = (/) ) )
20 19 imp 
 |-  ( ( ( # ` V ) = 1 /\ v e. V ) -> ( V \ { v } ) = (/) )
21 20 raleqdv 
 |-  ( ( ( # ` V ) = 1 /\ v e. V ) -> ( A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) <-> A. n e. (/) n e. ( G NeighbVtx v ) ) )
22 3 21 mpbiri 
 |-  ( ( ( # ` V ) = 1 /\ v e. V ) -> A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) )
23 1 uvtxel 
 |-  ( v e. ( UnivVtx ` G ) <-> ( v e. V /\ A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) ) )
24 2 22 23 sylanbrc 
 |-  ( ( ( # ` V ) = 1 /\ v e. V ) -> v e. ( UnivVtx ` G ) )
25 24 ralrimiva 
 |-  ( ( # ` V ) = 1 -> A. v e. V v e. ( UnivVtx ` G ) )
26 1 cplgr1vlem 
 |-  ( ( # ` V ) = 1 -> G e. _V )
27 1 iscplgr 
 |-  ( G e. _V -> ( G e. ComplGraph <-> A. v e. V v e. ( UnivVtx ` G ) ) )
28 26 27 syl 
 |-  ( ( # ` V ) = 1 -> ( G e. ComplGraph <-> A. v e. V v e. ( UnivVtx ` G ) ) )
29 25 28 mpbird 
 |-  ( ( # ` V ) = 1 -> G e. ComplGraph )