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

Definition df-frgra 26309
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 26308 . 2 class FriendGrph
2 vv . . . . . 6 setvar 𝑣
32cv 1473 . . . . 5 class 𝑣
4 ve . . . . . 6 setvar 𝑒
54cv 1473 . . . . 5 class 𝑒
6 cusg 25652 . . . . 5 class USGrph
73, 5, 6wbr 4577 . . . 4 wff 𝑣 USGrph 𝑒
8 vx . . . . . . . . . . 11 setvar 𝑥
98cv 1473 . . . . . . . . . 10 class 𝑥
10 vk . . . . . . . . . . 11 setvar 𝑘
1110cv 1473 . . . . . . . . . 10 class 𝑘
129, 11cpr 4126 . . . . . . . . 9 class {𝑥, 𝑘}
13 vl . . . . . . . . . . 11 setvar 𝑙
1413cv 1473 . . . . . . . . . 10 class 𝑙
159, 14cpr 4126 . . . . . . . . 9 class {𝑥, 𝑙}
1612, 15cpr 4126 . . . . . . . 8 class {{𝑥, 𝑘}, {𝑥, 𝑙}}
175crn 5028 . . . . . . . 8 class ran 𝑒
1816, 17wss 3539 . . . . . . 7 wff {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝑒
1918, 8, 3wreu 2897 . . . . . 6 wff ∃!𝑥𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝑒
2011csn 4124 . . . . . . 7 class {𝑘}
213, 20cdif 3536 . . . . . 6 class (𝑣 ∖ {𝑘})
2219, 13, 21wral 2895 . . . . 5 wff 𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝑒
2322, 10, 3wral 2895 . . . 4 wff 𝑘𝑣𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝑒
247, 23wa 382 . . 3 wff (𝑣 USGrph 𝑒 ∧ ∀𝑘𝑣𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝑒)
2524, 2, 4copab 4636 . 2 class {⟨𝑣, 𝑒⟩ ∣ (𝑣 USGrph 𝑒 ∧ ∀𝑘𝑣𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝑒)}
261, 25wceq 1474 1 wff FriendGrph = {⟨𝑣, 𝑒⟩ ∣ (𝑣 USGrph 𝑒 ∧ ∀𝑘𝑣𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ ran 𝑒)}
Colors of variables: wff setvar class
This definition is referenced by:  isfrgra  26310  frisusgrapr  26311
  Copyright terms: Public domain W3C validator