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 e. V | A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) }
4 3 a1i 
 |-  ( E = (/) -> ( UnivVtx ` G ) = { v e. V | A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) } )
5 4 neeq1d 
 |-  ( E = (/) -> ( ( UnivVtx ` G ) =/= (/) <-> { v e. V | A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) } =/= (/) ) )
6 rabn0 
 |-  ( { v e. V | A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) } =/= (/) <-> E. v e. V A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) )
7 6 a1i 
 |-  ( E = (/) -> ( { v e. V | A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) } =/= (/) <-> E. v e. V A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) ) )
8 falseral0 
 |-  ( ( A. n -. n e. (/) /\ A. n e. ( V \ { v } ) n e. (/) ) -> ( V \ { v } ) = (/) )
9 8 ex 
 |-  ( A. n -. n e. (/) -> ( A. n e. ( V \ { v } ) n e. (/) -> ( V \ { v } ) = (/) ) )
10 noel 
 |-  -. n e. (/)
11 9 10 mpg 
 |-  ( A. n e. ( V \ { v } ) n e. (/) -> ( V \ { v } ) = (/) )
12 ssdif0 
 |-  ( V C_ { v } <-> ( V \ { v } ) = (/) )
13 sssn 
 |-  ( V C_ { v } <-> ( V = (/) \/ V = { v } ) )
14 ne0i 
 |-  ( v e. V -> V =/= (/) )
15 eqneqall 
 |-  ( V = (/) -> ( V =/= (/) -> V = { v } ) )
16 14 15 syl5 
 |-  ( V = (/) -> ( v e. V -> V = { v } ) )
17 ax-1 
 |-  ( V = { v } -> ( v e. V -> V = { v } ) )
18 16 17 jaoi 
 |-  ( ( V = (/) \/ V = { v } ) -> ( v e. V -> V = { v } ) )
19 13 18 sylbi 
 |-  ( V C_ { v } -> ( v e. V -> V = { v } ) )
20 12 19 sylbir 
 |-  ( ( V \ { v } ) = (/) -> ( v e. V -> V = { v } ) )
21 11 20 syl 
 |-  ( A. n e. ( V \ { v } ) n e. (/) -> ( v e. V -> V = { v } ) )
22 21 impcom 
 |-  ( ( v e. V /\ A. n e. ( V \ { v } ) n e. (/) ) -> V = { v } )
23 vsnid 
 |-  v e. { v }
24 eleq2 
 |-  ( V = { v } -> ( v e. V <-> v e. { v } ) )
25 23 24 mpbiri 
 |-  ( V = { v } -> v e. V )
26 ralel 
 |-  A. n e. (/) n e. (/)
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 } -> ( A. n e. ( V \ { v } ) n e. (/) <-> A. n e. (/) n e. (/) ) )
31 26 30 mpbiri 
 |-  ( V = { v } -> A. n e. ( V \ { v } ) n e. (/) )
32 25 31 jca 
 |-  ( V = { v } -> ( v e. V /\ A. n e. ( V \ { v } ) n e. (/) ) )
33 22 32 impbii 
 |-  ( ( v e. V /\ A. n e. ( V \ { v } ) n e. (/) ) <-> V = { v } )
34 33 a1i 
 |-  ( E = (/) -> ( ( v e. V /\ A. n e. ( V \ { v } ) n e. (/) ) <-> V = { v } ) )
35 34 exbidv 
 |-  ( E = (/) -> ( E. v ( v e. V /\ A. n e. ( V \ { v } ) n e. (/) ) <-> E. 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 e. ( G NeighbVtx v ) <-> n e. (/) ) )
40 39 rexralbidv 
 |-  ( E = (/) -> ( E. v e. V A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) <-> E. v e. V A. n e. ( V \ { v } ) n e. (/) ) )
41 df-rex 
 |-  ( E. v e. V A. n e. ( V \ { v } ) n e. (/) <-> E. v ( v e. V /\ A. n e. ( V \ { v } ) n e. (/) ) )
42 40 41 bitrdi 
 |-  ( E = (/) -> ( E. v e. V A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) <-> E. v ( v e. V /\ A. n e. ( V \ { v } ) n e. (/) ) ) )
43 1 fvexi 
 |-  V e. _V
44 hash1snb 
 |-  ( V e. _V -> ( ( # ` V ) = 1 <-> E. v V = { v } ) )
45 43 44 mp1i 
 |-  ( E = (/) -> ( ( # ` V ) = 1 <-> E. v V = { v } ) )
46 35 42 45 3bitr4d 
 |-  ( E = (/) -> ( E. v e. V A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) <-> ( # ` V ) = 1 ) )
47 5 7 46 3bitrd 
 |-  ( E = (/) -> ( ( UnivVtx ` G ) =/= (/) <-> ( # ` V ) = 1 ) )