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

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
StepHypRef Expression
1 cfrgra 26515 . 2 class FriendGrph
2 vv . . . . . 6 setvar 𝑣
32cv 1474 . . . . 5 class 𝑣
4 ve . . . . . 6 setvar 𝑒
54cv 1474 . . . . 5 class 𝑒
6 cusg 25859 . . . . 5 class USGrph
73, 5, 6wbr 4583 . . . 4 wff 𝑣 USGrph 𝑒
8 vx . . . . . . . . . . 11 setvar 𝑥
98cv 1474 . . . . . . . . . 10 class 𝑥
10 vk . . . . . . . . . . 11 setvar 𝑘
1110cv 1474 . . . . . . . . . 10 class 𝑘
129, 11cpr 4127 . . . . . . . . 9 class {𝑥, 𝑘}
13 vl . . . . . . . . . . 11 setvar 𝑙
1413cv 1474 . . . . . . . . . 10 class 𝑙
159, 14cpr 4127 . . . . . . . . 9 class {𝑥, 𝑙}
1612, 15cpr 4127 . . . . . . . 8 class {{𝑥, 𝑘}, {𝑥, 𝑙}}
175crn 5039 . . . . . . . 8 class ran 𝑒
1816, 17wss 3540 . . . . . . 7 wff {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝑒
1918, 8, 3wreu 2898 . . . . . 6 wff ∃!𝑥𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝑒
2011csn 4125 . . . . . . 7 class {𝑘}
213, 20cdif 3537 . . . . . 6 class (𝑣 ∖ {𝑘})
2219, 13, 21wral 2896 . . . . 5 wff 𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝑒
2322, 10, 3wral 2896 . . . 4 wff 𝑘𝑣𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝑒
247, 23wa 383 . . 3 wff (𝑣 USGrph 𝑒 ∧ ∀𝑘𝑣𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝑒)
2524, 2, 4copab 4642 . 2 class {⟨𝑣, 𝑒⟩ ∣ (𝑣 USGrph 𝑒 ∧ ∀𝑘𝑣𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝑒)}
261, 25wceq 1475 1 wff FriendGrph = {⟨𝑣, 𝑒⟩ ∣ (𝑣 USGrph 𝑒 ∧ ∀𝑘𝑣𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝑒)}
 Colors of variables: wff setvar class This definition is referenced by:  isfrgra  26517  frisusgrapr  26518
 Copyright terms: Public domain W3C validator