Metamath Proof Explorer

Definition df-frgr

Description: Define the class of all friendship graphs: a simple graph is called a friendship graph if every pair of its vertices has exactly one common neighbor. This condition is called thefriendship condition , see definition in MertziosUnger p. 152. (Contributed by Alexander van der Vekens and Mario Carneiro, 2-Oct-2017) (Revised by AV, 29-Mar-2021) (Revised by AV, 3-Jan-2024)

Ref Expression
Assertion df-frgr 
|- FriendGraph = { g e. USGraph | [. ( Vtx ` g ) / v ]. [. ( Edg ` g ) / e ]. A. k e. v A. l e. ( v \ { k } ) E! x e. v { { x , k } , { x , l } } C_ e }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfrgr 
 |-  FriendGraph
1 vg 
 |-  g
2 cusgr 
 |-  USGraph
3 cvtx 
 |-  Vtx
4 1 cv 
 |-  g
5 4 3 cfv 
 |-  ( Vtx ` g )
6 vv 
 |-  v
7 cedg 
 |-  Edg
8 4 7 cfv 
 |-  ( Edg ` g )
9 ve 
 |-  e
10 vk 
 |-  k
11 6 cv 
 |-  v
12 vl 
 |-  l
13 10 cv 
 |-  k
14 13 csn 
 |-  { k }
15 11 14 cdif 
 |-  ( v \ { k } )
16 vx 
 |-  x
17 16 cv 
 |-  x
18 17 13 cpr 
 |-  { x , k }
19 12 cv 
 |-  l
20 17 19 cpr 
 |-  { x , l }
21 18 20 cpr 
 |-  { { x , k } , { x , l } }
22 9 cv 
 |-  e
23 21 22 wss 
 |-  { { x , k } , { x , l } } C_ e
24 23 16 11 wreu 
 |-  E! x e. v { { x , k } , { x , l } } C_ e
25 24 12 15 wral 
 |-  A. l e. ( v \ { k } ) E! x e. v { { x , k } , { x , l } } C_ e
26 25 10 11 wral 
 |-  A. k e. v A. l e. ( v \ { k } ) E! x e. v { { x , k } , { x , l } } C_ e
27 26 9 8 wsbc 
 |-  [. ( Edg ` g ) / e ]. A. k e. v A. l e. ( v \ { k } ) E! x e. v { { x , k } , { x , l } } C_ e
28 27 6 5 wsbc 
 |-  [. ( Vtx ` g ) / v ]. [. ( Edg ` g ) / e ]. A. k e. v A. l e. ( v \ { k } ) E! x e. v { { x , k } , { x , l } } C_ e
29 28 1 2 crab 
 |-  { g e. USGraph | [. ( Vtx ` g ) / v ]. [. ( Edg ` g ) / e ]. A. k e. v A. l e. ( v \ { k } ) E! x e. v { { x , k } , { x , l } } C_ e }
30 0 29 wceq 
 |-  FriendGraph = { g e. USGraph | [. ( Vtx ` g ) / v ]. [. ( Edg ` g ) / e ]. A. k e. v A. l e. ( v \ { k } ) E! x e. v { { x , k } , { x , l } } C_ e }