Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-frgr Structured version   Visualization version   GIF version

Definition df-frgr 28156
 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
StepHypRef Expression
1 cfrgr 28155 . 2 class FriendGraph
2 vx . . . . . . . . . . . 12 setvar 𝑥
32cv 1537 . . . . . . . . . . 11 class 𝑥
4 vk . . . . . . . . . . . 12 setvar 𝑘
54cv 1537 . . . . . . . . . . 11 class 𝑘
63, 5cpr 4527 . . . . . . . . . 10 class {𝑥, 𝑘}
7 vl . . . . . . . . . . . 12 setvar 𝑙
87cv 1537 . . . . . . . . . . 11 class 𝑙
93, 8cpr 4527 . . . . . . . . . 10 class {𝑥, 𝑙}
106, 9cpr 4527 . . . . . . . . 9 class {{𝑥, 𝑘}, {𝑥, 𝑙}}
11 ve . . . . . . . . . 10 setvar 𝑒
1211cv 1537 . . . . . . . . 9 class 𝑒
1310, 12wss 3860 . . . . . . . 8 wff {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒
14 vv . . . . . . . . 9 setvar 𝑣
1514cv 1537 . . . . . . . 8 class 𝑣
1613, 2, 15wreu 3072 . . . . . . 7 wff ∃!𝑥𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒
175csn 4525 . . . . . . . 8 class {𝑘}
1815, 17cdif 3857 . . . . . . 7 class (𝑣 ∖ {𝑘})
1916, 7, 18wral 3070 . . . . . 6 wff 𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒
2019, 4, 15wral 3070 . . . . 5 wff 𝑘𝑣𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒
21 vg . . . . . . 7 setvar 𝑔
2221cv 1537 . . . . . 6 class 𝑔
23 cedg 26952 . . . . . 6 class Edg
2422, 23cfv 6340 . . . . 5 class (Edg‘𝑔)
2520, 11, 24wsbc 3698 . . . 4 wff [(Edg‘𝑔) / 𝑒]𝑘𝑣𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒
26 cvtx 26901 . . . . 5 class Vtx
2722, 26cfv 6340 . . . 4 class (Vtx‘𝑔)
2825, 14, 27wsbc 3698 . . 3 wff [(Vtx‘𝑔) / 𝑣][(Edg‘𝑔) / 𝑒]𝑘𝑣𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒
29 cusgr 27054 . . 3 class USGraph
3028, 21, 29crab 3074 . 2 class {𝑔 ∈ USGraph ∣ [(Vtx‘𝑔) / 𝑣][(Edg‘𝑔) / 𝑒]𝑘𝑣𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒}
311, 30wceq 1538 1 wff FriendGraph = {𝑔 ∈ USGraph ∣ [(Vtx‘𝑔) / 𝑣][(Edg‘𝑔) / 𝑒]𝑘𝑣𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒}
 Colors of variables: wff setvar class This definition is referenced by:  isfrgr  28157
 Copyright terms: Public domain W3C validator