Definition df-frgr 27724

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 the friendship 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.)

Assertion

Ref	Expression
df-frgr	⊢ FriendGraph = {𝑔 ∣ (𝑔 ∈ USGraph ∧ [(Vtx‘𝑔) / 𝑣][(Edg‘𝑔) / 𝑒]∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒)}

Distinct variable group:   𝑒,𝑔,𝑘,𝑙,𝑥,𝑣

Detailed syntax breakdown of Definition df-frgr

Step	Hyp	Ref	Expression
1		cfrgr 27723	. 2 class FriendGraph
2		vg	. . . . . 6 setvar 𝑔
3	2	cv 1524	. . . . 5 class 𝑔
4		cusgr 26621	. . . . 5 class USGraph
5	3, 4	wcel 2083	. . . 4 wff 𝑔 ∈ USGraph
6		vx	. . . . . . . . . . . . 13 setvar 𝑥
7	6	cv 1524	. . . . . . . . . . . 12 class 𝑥
8		vk	. . . . . . . . . . . . 13 setvar 𝑘
9	8	cv 1524	. . . . . . . . . . . 12 class 𝑘
10	7, 9	cpr 4480	. . . . . . . . . . 11 class {𝑥, 𝑘}
11		vl	. . . . . . . . . . . . 13 setvar 𝑙
12	11	cv 1524	. . . . . . . . . . . 12 class 𝑙
13	7, 12	cpr 4480	. . . . . . . . . . 11 class {𝑥, 𝑙}
14	10, 13	cpr 4480	. . . . . . . . . 10 class {{𝑥, 𝑘}, {𝑥, 𝑙}}
15		ve	. . . . . . . . . . 11 setvar 𝑒
16	15	cv 1524	. . . . . . . . . 10 class 𝑒
17	14, 16	wss 3865	. . . . . . . . 9 wff {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒
18		vv	. . . . . . . . . 10 setvar 𝑣
19	18	cv 1524	. . . . . . . . 9 class 𝑣
20	17, 6, 19	wreu 3109	. . . . . . . 8 wff ∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒
21	9	csn 4478	. . . . . . . . 9 class {𝑘}
22	19, 21	cdif 3862	. . . . . . . 8 class (𝑣 ∖ {𝑘})
23	20, 11, 22	wral 3107	. . . . . . 7 wff ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒
24	23, 8, 19	wral 3107	. . . . . 6 wff ∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒
25		cedg 26519	. . . . . . 7 class Edg
26	3, 25	cfv 6232	. . . . . 6 class (Edg‘𝑔)
27	24, 15, 26	wsbc 3711	. . . . 5 wff [(Edg‘𝑔) / 𝑒]∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒
28		cvtx 26468	. . . . . 6 class Vtx
29	3, 28	cfv 6232	. . . . 5 class (Vtx‘𝑔)
30	27, 18, 29	wsbc 3711	. . . 4 wff [(Vtx‘𝑔) / 𝑣][(Edg‘𝑔) / 𝑒]∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒
31	5, 30	wa 396	. . 3 wff (𝑔 ∈ USGraph ∧ [(Vtx‘𝑔) / 𝑣][(Edg‘𝑔) / 𝑒]∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒)
32	31, 2	cab 2777	. 2 class {𝑔 ∣ (𝑔 ∈ USGraph ∧ [(Vtx‘𝑔) / 𝑣][(Edg‘𝑔) / 𝑒]∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒)}
33	1, 32	wceq 1525	1 wff FriendGraph = {𝑔 ∣ (𝑔 ∈ USGraph ∧ [(Vtx‘𝑔) / 𝑣][(Edg‘𝑔) / 𝑒]∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒)}

This definition is referenced by:  isfrgr  27725