Metamath Proof Explorer

Theorem frgr0v

Description: Any null graph (set with no vertices) is a friendship graph iff its edge function is empty. (Contributed by Alexander van der Vekens, 4-Oct-2017) (Revised by AV, 29-Mar-2021)

Ref Expression
Assertion frgr0v 
|- ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> ( G e. FriendGraph <-> ( iEdg ` G ) = (/) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
3 1 2 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 ) ) )
4 usgruhgr 
 |-  ( G e. USGraph -> G e. UHGraph )
5 4 adantr 
 |-  ( ( 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 ) ) -> G e. UHGraph )
6 uhgr0vb 
 |-  ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> ( G e. UHGraph <-> ( iEdg ` G ) = (/) ) )
7 5 6 syl5ib 
 |-  ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> ( ( 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 ) ) -> ( iEdg ` G ) = (/) ) )
8 simpll 
 |-  ( ( ( G e. W /\ ( Vtx ` G ) = (/) ) /\ ( iEdg ` G ) = (/) ) -> G e. W )
9 simpr 
 |-  ( ( ( G e. W /\ ( Vtx ` G ) = (/) ) /\ ( iEdg ` G ) = (/) ) -> ( iEdg ` G ) = (/) )
10 8 9 usgr0e 
 |-  ( ( ( G e. W /\ ( Vtx ` G ) = (/) ) /\ ( iEdg ` G ) = (/) ) -> G e. USGraph )
11 ral0 
 |-  A. k e. (/) A. l e. ( ( Vtx ` G ) \ { k } ) E! x e. ( Vtx ` G ) { { x , k } , { x , l } } C_ ( Edg ` G )
12 raleq 
 |-  ( ( Vtx ` G ) = (/) -> ( 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. (/) A. l e. ( ( Vtx ` G ) \ { k } ) E! x e. ( Vtx ` G ) { { x , k } , { x , l } } C_ ( Edg ` G ) ) )
13 12 adantl 
 |-  ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> ( 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. (/) A. l e. ( ( Vtx ` G ) \ { k } ) E! x e. ( Vtx ` G ) { { x , k } , { x , l } } C_ ( Edg ` G ) ) )
14 11 13 mpbiri 
 |-  ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> A. k e. ( Vtx ` G ) A. l e. ( ( Vtx ` G ) \ { k } ) E! x e. ( Vtx ` G ) { { x , k } , { x , l } } C_ ( Edg ` G ) )
15 14 adantr 
 |-  ( ( ( G e. W /\ ( Vtx ` G ) = (/) ) /\ ( iEdg ` G ) = (/) ) -> A. k e. ( Vtx ` G ) A. l e. ( ( Vtx ` G ) \ { k } ) E! x e. ( Vtx ` G ) { { x , k } , { x , l } } C_ ( Edg ` G ) )
16 10 15 jca 
 |-  ( ( ( G e. W /\ ( Vtx ` G ) = (/) ) /\ ( iEdg ` G ) = (/) ) -> ( 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 ) ) )
17 16 ex 
 |-  ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> ( ( iEdg ` G ) = (/) -> ( 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 ) ) ) )
18 7 17 impbid 
 |-  ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> ( ( 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 ) ) <-> ( iEdg ` G ) = (/) ) )
19 3 18 syl5bb 
 |-  ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> ( G e. FriendGraph <-> ( iEdg ` G ) = (/) ) )