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 ∈ USGraph | [˙ Vtx ⁡ g / v]˙ [˙ Edg ⁡ g / e]˙ ∀ k ∈ v ∀ l ∈ v ∖ k ∃! x ∈ v x k x l ⊆ e

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfrgr class FriendGraph
1 vg setvar g
2 cusgr class USGraph
3 cvtx class Vtx
4 1 cv setvar g
5 4 3 cfv class Vtx ⁡ g
6 vv setvar v
7 cedg class Edg
8 4 7 cfv class Edg ⁡ g
9 ve setvar e
10 vk setvar k
11 6 cv setvar v
12 vl setvar l
13 10 cv setvar k
14 13 csn class k
15 11 14 cdif class v ∖ k
16 vx setvar x
17 16 cv setvar x
18 17 13 cpr class x k
19 12 cv setvar l
20 17 19 cpr class x l
21 18 20 cpr class x k x l
22 9 cv setvar e
23 21 22 wss wff x k x l ⊆ e
24 23 16 11 wreu wff ∃! x ∈ v x k x l ⊆ e
25 24 12 15 wral wff ∀ l ∈ v ∖ k ∃! x ∈ v x k x l ⊆ e
26 25 10 11 wral wff ∀ k ∈ v ∀ l ∈ v ∖ k ∃! x ∈ v x k x l ⊆ e
27 26 9 8 wsbc wff [˙ Edg ⁡ g / e]˙ ∀ k ∈ v ∀ l ∈ v ∖ k ∃! x ∈ v x k x l ⊆ e
28 27 6 5 wsbc wff [˙ Vtx ⁡ g / v]˙ [˙ Edg ⁡ g / e]˙ ∀ k ∈ v ∀ l ∈ v ∖ k ∃! x ∈ v x k x l ⊆ e
29 28 1 2 crab class g ∈ USGraph | [˙ Vtx ⁡ g / v]˙ [˙ Edg ⁡ g / e]˙ ∀ k ∈ v ∀ l ∈ v ∖ k ∃! x ∈ v x k x l ⊆ e
30 0 29 wceq wff FriendGraph = g ∈ USGraph | [˙ Vtx ⁡ g / v]˙ [˙ Edg ⁡ g / e]˙ ∀ k ∈ v ∀ l ∈ v ∖ k ∃! x ∈ v x k x l ⊆ e