Definition df-frgr 27121

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 27120	. 2 class FriendGraph
2		vg	. . . . . 6 setvar 𝑔
3	2	cv 1482	. . . . 5 class 𝑔
4		cusgr 26044	. . . . 5 class USGraph
5	3, 4	wcel 1990	. . . 4 wff 𝑔 ∈ USGraph
6		vx	. . . . . . . . . . . . 13 setvar 𝑥
7	6	cv 1482	. . . . . . . . . . . 12 class 𝑥
8		vk	. . . . . . . . . . . . 13 setvar 𝑘
9	8	cv 1482	. . . . . . . . . . . 12 class 𝑘
10	7, 9	cpr 4179	. . . . . . . . . . 11 class {𝑥, 𝑘}
11		vl	. . . . . . . . . . . . 13 setvar 𝑙
12	11	cv 1482	. . . . . . . . . . . 12 class 𝑙
13	7, 12	cpr 4179	. . . . . . . . . . 11 class {𝑥, 𝑙}
14	10, 13	cpr 4179	. . . . . . . . . 10 class {{𝑥, 𝑘}, {𝑥, 𝑙}}
15		ve	. . . . . . . . . . 11 setvar 𝑒
16	15	cv 1482	. . . . . . . . . 10 class 𝑒
17	14, 16	wss 3574	. . . . . . . . 9 wff {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒
18		vv	. . . . . . . . . 10 setvar 𝑣
19	18	cv 1482	. . . . . . . . 9 class 𝑣
20	17, 6, 19	wreu 2914	. . . . . . . 8 wff ∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒
21	9	csn 4177	. . . . . . . . 9 class {𝑘}
22	19, 21	cdif 3571	. . . . . . . 8 class (𝑣 ∖ {𝑘})
23	20, 11, 22	wral 2912	. . . . . . 7 wff ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒
24	23, 8, 19	wral 2912	. . . . . 6 wff ∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒
25		cedg 25939	. . . . . . 7 class Edg
26	3, 25	cfv 5888	. . . . . 6 class (Edg‘𝑔)
27	24, 15, 26	wsbc 3435	. . . . 5 wff [(Edg‘𝑔) / 𝑒]∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒
28		cvtx 25874	. . . . . 6 class Vtx
29	3, 28	cfv 5888	. . . . 5 class (Vtx‘𝑔)
30	27, 18, 29	wsbc 3435	. . . 4 wff [(Vtx‘𝑔) / 𝑣][(Edg‘𝑔) / 𝑒]∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒
31	5, 30	wa 384	. . 3 wff (𝑔 ∈ USGraph ∧ [(Vtx‘𝑔) / 𝑣][(Edg‘𝑔) / 𝑒]∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒)
32	31, 2	cab 2608	. 2 class {𝑔 ∣ (𝑔 ∈ USGraph ∧ [(Vtx‘𝑔) / 𝑣][(Edg‘𝑔) / 𝑒]∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒)}
33	1, 32	wceq 1483	1 wff FriendGraph = {𝑔 ∣ (𝑔 ∈ USGraph ∧ [(Vtx‘𝑔) / 𝑣][(Edg‘𝑔) / 𝑒]∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒)}

This definition is referenced by:  isfrgr  27122