Definition df-frgra 26516

Description: Define the class of all Friendship Graphs. A graph is called a friendship graph if every pair of its vertices has exactly one common neighbor. (Contributed by Alexander van der Vekens and Mario Carneiro, 2-Oct-2017.)

Assertion

Ref	Expression
df-frgra	⊢ FriendGrph = {⟨𝑣, 𝑒⟩ ∣ (𝑣 USGrph 𝑒 ∧ ∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝑒)}

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

Detailed syntax breakdown of Definition df-frgra

Step	Hyp	Ref	Expression
1		cfrgra 26515	. 2 class FriendGrph
2		vv	. . . . . 6 setvar 𝑣
3	2	cv 1474	. . . . 5 class 𝑣
4		ve	. . . . . 6 setvar 𝑒
5	4	cv 1474	. . . . 5 class 𝑒
6		cusg 25859	. . . . 5 class USGrph
7	3, 5, 6	wbr 4583	. . . 4 wff 𝑣 USGrph 𝑒
8		vx	. . . . . . . . . . 11 setvar 𝑥
9	8	cv 1474	. . . . . . . . . 10 class 𝑥
10		vk	. . . . . . . . . . 11 setvar 𝑘
11	10	cv 1474	. . . . . . . . . 10 class 𝑘
12	9, 11	cpr 4127	. . . . . . . . 9 class {𝑥, 𝑘}
13		vl	. . . . . . . . . . 11 setvar 𝑙
14	13	cv 1474	. . . . . . . . . 10 class 𝑙
15	9, 14	cpr 4127	. . . . . . . . 9 class {𝑥, 𝑙}
16	12, 15	cpr 4127	. . . . . . . 8 class {{𝑥, 𝑘}, {𝑥, 𝑙}}
17	5	crn 5039	. . . . . . . 8 class ran 𝑒
18	16, 17	wss 3540	. . . . . . 7 wff {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝑒
19	18, 8, 3	wreu 2898	. . . . . 6 wff ∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝑒
20	11	csn 4125	. . . . . . 7 class {𝑘}
21	3, 20	cdif 3537	. . . . . 6 class (𝑣 ∖ {𝑘})
22	19, 13, 21	wral 2896	. . . . 5 wff ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝑒
23	22, 10, 3	wral 2896	. . . 4 wff ∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝑒
24	7, 23	wa 383	. . 3 wff (𝑣 USGrph 𝑒 ∧ ∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝑒)
25	24, 2, 4	copab 4642	. 2 class {⟨𝑣, 𝑒⟩ ∣ (𝑣 USGrph 𝑒 ∧ ∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝑒)}
26	1, 25	wceq 1475	1 wff FriendGrph = {⟨𝑣, 𝑒⟩ ∣ (𝑣 USGrph 𝑒 ∧ ∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝑒)}

This definition is referenced by:  isfrgra  26517  frisusgrapr  26518