Definition df-frgr 28524

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.) (Revised by AV, 3-Jan-2024.)

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 28523	. 2 class FriendGraph
2		vx	. . . . . . . . . . . 12 setvar 𝑥
3	2	cv 1538	. . . . . . . . . . 11 class 𝑥
4		vk	. . . . . . . . . . . 12 setvar 𝑘
5	4	cv 1538	. . . . . . . . . . 11 class 𝑘
6	3, 5	cpr 4560	. . . . . . . . . 10 class {𝑥, 𝑘}
7		vl	. . . . . . . . . . . 12 setvar 𝑙
8	7	cv 1538	. . . . . . . . . . 11 class 𝑙
9	3, 8	cpr 4560	. . . . . . . . . 10 class {𝑥, 𝑙}
10	6, 9	cpr 4560	. . . . . . . . 9 class {{𝑥, 𝑘}, {𝑥, 𝑙}}
11		ve	. . . . . . . . . 10 setvar 𝑒
12	11	cv 1538	. . . . . . . . 9 class 𝑒
13	10, 12	wss 3883	. . . . . . . 8 wff {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒
14		vv	. . . . . . . . 9 setvar 𝑣
15	14	cv 1538	. . . . . . . 8 class 𝑣
16	13, 2, 15	wreu 3065	. . . . . . 7 wff ∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒
17	5	csn 4558	. . . . . . . 8 class {𝑘}
18	15, 17	cdif 3880	. . . . . . 7 class (𝑣 ∖ {𝑘})
19	16, 7, 18	wral 3063	. . . . . 6 wff ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒
20	19, 4, 15	wral 3063	. . . . 5 wff ∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒
21		vg	. . . . . . 7 setvar 𝑔
22	21	cv 1538	. . . . . 6 class 𝑔
23		cedg 27320	. . . . . 6 class Edg
24	22, 23	cfv 6418	. . . . 5 class (Edg‘𝑔)
25	20, 11, 24	wsbc 3711	. . . 4 wff [(Edg‘𝑔) / 𝑒]∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒
26		cvtx 27269	. . . . 5 class Vtx
27	22, 26	cfv 6418	. . . 4 class (Vtx‘𝑔)
28	25, 14, 27	wsbc 3711	. . 3 wff [(Vtx‘𝑔) / 𝑣][(Edg‘𝑔) / 𝑒]∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒
29		cusgr 27422	. . 3 class USGraph
30	28, 21, 29	crab 3067	. 2 class {𝑔 ∈ USGraph ∣ [(Vtx‘𝑔) / 𝑣][(Edg‘𝑔) / 𝑒]∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒}
31	1, 30	wceq 1539	1 wff FriendGraph = {𝑔 ∈ USGraph ∣ [(Vtx‘𝑔) / 𝑣][(Edg‘𝑔) / 𝑒]∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒}

This definition is referenced by:  isfrgr  28525