Metamath Proof Explorer

Theorem frgr1v

Description: Any graph with (at most) one vertex is a friendship graph. (Contributed by Alexander van der Vekens, 4-Oct-2017) (Revised by AV, 29-Mar-2021)

Ref Expression
Assertion frgr1v 
|- ( ( G e. USGraph /\ ( Vtx ` G ) = { N } ) -> G e. FriendGraph )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( G e. USGraph /\ ( Vtx ` G ) = { N } ) -> G e. USGraph )
2 ral0 
 |-  A. l e. (/) E! x e. { N } { { x , N } , { x , l } } C_ ( Edg ` G )
3 sneq 
 |-  ( k = N -> { k } = { N } )
4 3 difeq2d 
 |-  ( k = N -> ( { N } \ { k } ) = ( { N } \ { N } ) )
5 difid 
 |-  ( { N } \ { N } ) = (/)
6 4 5 eqtrdi 
 |-  ( k = N -> ( { N } \ { k } ) = (/) )
7 preq2 
 |-  ( k = N -> { x , k } = { x , N } )
8 7 preq1d 
 |-  ( k = N -> { { x , k } , { x , l } } = { { x , N } , { x , l } } )
9 8 sseq1d 
 |-  ( k = N -> ( { { x , k } , { x , l } } C_ ( Edg ` G ) <-> { { x , N } , { x , l } } C_ ( Edg ` G ) ) )
10 9 reubidv 
 |-  ( k = N -> ( E! x e. { N } { { x , k } , { x , l } } C_ ( Edg ` G ) <-> E! x e. { N } { { x , N } , { x , l } } C_ ( Edg ` G ) ) )
11 6 10 raleqbidv 
 |-  ( k = N -> ( A. l e. ( { N } \ { k } ) E! x e. { N } { { x , k } , { x , l } } C_ ( Edg ` G ) <-> A. l e. (/) E! x e. { N } { { x , N } , { x , l } } C_ ( Edg ` G ) ) )
12 11 ralsng 
 |-  ( N e. _V -> ( A. k e. { N } A. l e. ( { N } \ { k } ) E! x e. { N } { { x , k } , { x , l } } C_ ( Edg ` G ) <-> A. l e. (/) E! x e. { N } { { x , N } , { x , l } } C_ ( Edg ` G ) ) )
13 2 12 mpbiri 
 |-  ( N e. _V -> A. k e. { N } A. l e. ( { N } \ { k } ) E! x e. { N } { { x , k } , { x , l } } C_ ( Edg ` G ) )
14 snprc 
 |-  ( -. N e. _V <-> { N } = (/) )
15 rzal 
 |-  ( { N } = (/) -> A. k e. { N } A. l e. ( { N } \ { k } ) E! x e. { N } { { x , k } , { x , l } } C_ ( Edg ` G ) )
16 14 15 sylbi 
 |-  ( -. N e. _V -> A. k e. { N } A. l e. ( { N } \ { k } ) E! x e. { N } { { x , k } , { x , l } } C_ ( Edg ` G ) )
17 13 16 pm2.61i 
 |-  A. k e. { N } A. l e. ( { N } \ { k } ) E! x e. { N } { { x , k } , { x , l } } C_ ( Edg ` G )
18 id 
 |-  ( ( Vtx ` G ) = { N } -> ( Vtx ` G ) = { N } )
19 difeq1 
 |-  ( ( Vtx ` G ) = { N } -> ( ( Vtx ` G ) \ { k } ) = ( { N } \ { k } ) )
20 reueq1 
 |-  ( ( Vtx ` G ) = { N } -> ( E! x e. ( Vtx ` G ) { { x , k } , { x , l } } C_ ( Edg ` G ) <-> E! x e. { N } { { x , k } , { x , l } } C_ ( Edg ` G ) ) )
21 19 20 raleqbidv 
 |-  ( ( Vtx ` G ) = { N } -> ( A. l e. ( ( Vtx ` G ) \ { k } ) E! x e. ( Vtx ` G ) { { x , k } , { x , l } } C_ ( Edg ` G ) <-> A. l e. ( { N } \ { k } ) E! x e. { N } { { x , k } , { x , l } } C_ ( Edg ` G ) ) )
22 18 21 raleqbidv 
 |-  ( ( Vtx ` G ) = { N } -> ( A. k e. ( Vtx ` G ) A. l e. ( ( Vtx ` G ) \ { k } ) E! x e. ( Vtx ` G ) { { x , k } , { x , l } } C_ ( Edg ` G ) <-> A. k e. { N } A. l e. ( { N } \ { k } ) E! x e. { N } { { x , k } , { x , l } } C_ ( Edg ` G ) ) )
23 22 adantl 
 |-  ( ( G e. USGraph /\ ( Vtx ` G ) = { N } ) -> ( A. k e. ( Vtx ` G ) A. l e. ( ( Vtx ` G ) \ { k } ) E! x e. ( Vtx ` G ) { { x , k } , { x , l } } C_ ( Edg ` G ) <-> A. k e. { N } A. l e. ( { N } \ { k } ) E! x e. { N } { { x , k } , { x , l } } C_ ( Edg ` G ) ) )
24 17 23 mpbiri 
 |-  ( ( G e. USGraph /\ ( Vtx ` G ) = { N } ) -> A. k e. ( Vtx ` G ) A. l e. ( ( Vtx ` G ) \ { k } ) E! x e. ( Vtx ` G ) { { x , k } , { x , l } } C_ ( Edg ` G ) )
25 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
26 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
27 25 26 isfrgr 
 |-  ( G e. FriendGraph <-> ( G e. USGraph /\ A. k e. ( Vtx ` G ) A. l e. ( ( Vtx ` G ) \ { k } ) E! x e. ( Vtx ` G ) { { x , k } , { x , l } } C_ ( Edg ` G ) ) )
28 1 24 27 sylanbrc 
 |-  ( ( G e. USGraph /\ ( Vtx ` G ) = { N } ) -> G e. FriendGraph )