Definition df-cusgra 25950

Description: Define the class of all complete (undirected simple) graphs. An undirected simple graph is called complete if every pair of distinct vertices is connected by a (unique) edge. (Contributed by Alexander van der Vekens, 12-Oct-2017.)

Assertion

Ref	Expression
df-cusgra	⊢ ComplUSGrph = {⟨𝑣, 𝑒⟩ ∣ (𝑣 USGrph 𝑒 ∧ ∀𝑘 ∈ 𝑣 ∀𝑛 ∈ (𝑣 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝑒)}

Distinct variable group:   𝑣,𝑒,𝑘,𝑛

Detailed syntax breakdown of Definition df-cusgra

Step	Hyp	Ref	Expression
1		ccusgra 25947	. 2 class ComplUSGrph
2		vv	. . . . . 6 setvar 𝑣
3	2	cv 1474	. . . . 5 class 𝑣
4		ve	. . . . . 6 setvar 𝑒
5	4	cv 1474	. . . . 5 class 𝑒
6		cusg 25859	. . . . 5 class USGrph
7	3, 5, 6	wbr 4583	. . . 4 wff 𝑣 USGrph 𝑒
8		vn	. . . . . . . . 9 setvar 𝑛
9	8	cv 1474	. . . . . . . 8 class 𝑛
10		vk	. . . . . . . . 9 setvar 𝑘
11	10	cv 1474	. . . . . . . 8 class 𝑘
12	9, 11	cpr 4127	. . . . . . 7 class {𝑛, 𝑘}
13	5	crn 5039	. . . . . . 7 class ran 𝑒
14	12, 13	wcel 1977	. . . . . 6 wff {𝑛, 𝑘} ∈ ran 𝑒
15	11	csn 4125	. . . . . . 7 class {𝑘}
16	3, 15	cdif 3537	. . . . . 6 class (𝑣 ∖ {𝑘})
17	14, 8, 16	wral 2896	. . . . 5 wff ∀𝑛 ∈ (𝑣 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝑒
18	17, 10, 3	wral 2896	. . . 4 wff ∀𝑘 ∈ 𝑣 ∀𝑛 ∈ (𝑣 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝑒
19	7, 18	wa 383	. . 3 wff (𝑣 USGrph 𝑒 ∧ ∀𝑘 ∈ 𝑣 ∀𝑛 ∈ (𝑣 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝑒)
20	19, 2, 4	copab 4642	. 2 class {⟨𝑣, 𝑒⟩ ∣ (𝑣 USGrph 𝑒 ∧ ∀𝑘 ∈ 𝑣 ∀𝑛 ∈ (𝑣 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝑒)}
21	1, 20	wceq 1475	1 wff ComplUSGrph = {⟨𝑣, 𝑒⟩ ∣ (𝑣 USGrph 𝑒 ∧ ∀𝑘 ∈ 𝑣 ∀𝑛 ∈ (𝑣 ∖ {𝑘}){𝑛, 𝑘} ∈ ran 𝑒)}

This definition is referenced by:  iscusgra  25985  iscusgra0  25986  cusgrasize  26006