Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-frgr Structured version   Visualization version   GIF version

Definition df-frgr 41410
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
StepHypRef Expression
1 cfrgr 41409 . 2 class FriendGraph
2 vg . . . . . 6 setvar 𝑔
32cv 1473 . . . . 5 class 𝑔
4 cusgr 40360 . . . . 5 class USGraph
53, 4wcel 1976 . . . 4 wff 𝑔 ∈ USGraph
6 vx . . . . . . . . . . . . 13 setvar 𝑥
76cv 1473 . . . . . . . . . . . 12 class 𝑥
8 vk . . . . . . . . . . . . 13 setvar 𝑘
98cv 1473 . . . . . . . . . . . 12 class 𝑘
107, 9cpr 4126 . . . . . . . . . . 11 class {𝑥, 𝑘}
11 vl . . . . . . . . . . . . 13 setvar 𝑙
1211cv 1473 . . . . . . . . . . . 12 class 𝑙
137, 12cpr 4126 . . . . . . . . . . 11 class {𝑥, 𝑙}
1410, 13cpr 4126 . . . . . . . . . 10 class {{𝑥, 𝑘}, {𝑥, 𝑙}}
15 ve . . . . . . . . . . 11 setvar 𝑒
1615cv 1473 . . . . . . . . . 10 class 𝑒
1714, 16wss 3539 . . . . . . . . 9 wff {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒
18 vv . . . . . . . . . 10 setvar 𝑣
1918cv 1473 . . . . . . . . 9 class 𝑣
2017, 6, 19wreu 2897 . . . . . . . 8 wff ∃!𝑥𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒
219csn 4124 . . . . . . . . 9 class {𝑘}
2219, 21cdif 3536 . . . . . . . 8 class (𝑣 ∖ {𝑘})
2320, 11, 22wral 2895 . . . . . . 7 wff 𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒
2423, 8, 19wral 2895 . . . . . 6 wff 𝑘𝑣𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒
25 cedga 40332 . . . . . . 7 class Edg
263, 25cfv 5789 . . . . . 6 class (Edg‘𝑔)
2724, 15, 26wsbc 3401 . . . . 5 wff [(Edg‘𝑔) / 𝑒]𝑘𝑣𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒
28 cvtx 40210 . . . . . 6 class Vtx
293, 28cfv 5789 . . . . 5 class (Vtx‘𝑔)
3027, 18, 29wsbc 3401 . . . 4 wff [(Vtx‘𝑔) / 𝑣][(Edg‘𝑔) / 𝑒]𝑘𝑣𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒
315, 30wa 382 . . 3 wff (𝑔 ∈ USGraph ∧ [(Vtx‘𝑔) / 𝑣][(Edg‘𝑔) / 𝑒]𝑘𝑣𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒)
3231, 2cab 2595 . 2 class {𝑔 ∣ (𝑔 ∈ USGraph ∧ [(Vtx‘𝑔) / 𝑣][(Edg‘𝑔) / 𝑒]𝑘𝑣𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒)}
331, 32wceq 1474 1 wff FriendGraph = {𝑔 ∣ (𝑔 ∈ USGraph ∧ [(Vtx‘𝑔) / 𝑣][(Edg‘𝑔) / 𝑒]𝑘𝑣𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒)}
Colors of variables: wff setvar class
This definition is referenced by:  isfrgr  41411
  Copyright terms: Public domain W3C validator