Definition df-grtri 47719

Description: Definition of a triangles in a graph. A triangle in a graph is a set of three (different) vertices completely connected with each other. Such vertices induce a closed walk of length 3, see grtriclwlk3 47726. (TODO: and a cycle of length 3 ,see grtricycl ). (Contributed by AV, 20-Jul-2025.)

Assertion

Ref	Expression
df-grtri	⊢ GrTriangles = (𝑔 ∈ V ↦ ⦋(Vtx‘𝑔) / 𝑣⦌⦋(Edg‘𝑔) / 𝑒⦌{𝑡 ∈ 𝒫 𝑣 ∣ ∃𝑓(𝑓:(0..^3)–1-1-onto→𝑡 ∧ ({(𝑓‘0), (𝑓‘1)} ∈ 𝑒 ∧ {(𝑓‘0), (𝑓‘2)} ∈ 𝑒 ∧ {(𝑓‘1), (𝑓‘2)} ∈ 𝑒))})

Distinct variable group:   𝑒,𝑓,𝑔,𝑡,𝑣

Detailed syntax breakdown of Definition df-grtri

Step	Hyp	Ref	Expression
1		cgrtri 47718	. 2 class GrTriangles
2		vg	. . 3 setvar 𝑔
3		cvv 3482	. . 3 class V
4		vv	. . . 4 setvar 𝑣
5	2	cv 1536	. . . . 5 class 𝑔
6		cvtx 29022	. . . . 5 class Vtx
7	5, 6	cfv 6572	. . . 4 class (Vtx‘𝑔)
8		ve	. . . . 5 setvar 𝑒
9		cedg 29073	. . . . . 6 class Edg
10	5, 9	cfv 6572	. . . . 5 class (Edg‘𝑔)
11		cc0 11180	. . . . . . . . . 10 class 0
12		c3 12345	. . . . . . . . . 10 class 3
13		cfzo 13707	. . . . . . . . . 10 class ..^
14	11, 12, 13	co 7445	. . . . . . . . 9 class (0..^3)
15		vt	. . . . . . . . . 10 setvar 𝑡
16	15	cv 1536	. . . . . . . . 9 class 𝑡
17		vf	. . . . . . . . . 10 setvar 𝑓
18	17	cv 1536	. . . . . . . . 9 class 𝑓
19	14, 16, 18	wf1o 6571	. . . . . . . 8 wff 𝑓:(0..^3)–1-1-onto→𝑡
20	11, 18	cfv 6572	. . . . . . . . . . 11 class (𝑓‘0)
21		c1 11181	. . . . . . . . . . . 12 class 1
22	21, 18	cfv 6572	. . . . . . . . . . 11 class (𝑓‘1)
23	20, 22	cpr 4650	. . . . . . . . . 10 class {(𝑓‘0), (𝑓‘1)}
24	8	cv 1536	. . . . . . . . . 10 class 𝑒
25	23, 24	wcel 2103	. . . . . . . . 9 wff {(𝑓‘0), (𝑓‘1)} ∈ 𝑒
26		c2 12344	. . . . . . . . . . . 12 class 2
27	26, 18	cfv 6572	. . . . . . . . . . 11 class (𝑓‘2)
28	20, 27	cpr 4650	. . . . . . . . . 10 class {(𝑓‘0), (𝑓‘2)}
29	28, 24	wcel 2103	. . . . . . . . 9 wff {(𝑓‘0), (𝑓‘2)} ∈ 𝑒
30	22, 27	cpr 4650	. . . . . . . . . 10 class {(𝑓‘1), (𝑓‘2)}
31	30, 24	wcel 2103	. . . . . . . . 9 wff {(𝑓‘1), (𝑓‘2)} ∈ 𝑒
32	25, 29, 31	w3a 1087	. . . . . . . 8 wff ({(𝑓‘0), (𝑓‘1)} ∈ 𝑒 ∧ {(𝑓‘0), (𝑓‘2)} ∈ 𝑒 ∧ {(𝑓‘1), (𝑓‘2)} ∈ 𝑒)
33	19, 32	wa 395	. . . . . . 7 wff (𝑓:(0..^3)–1-1-onto→𝑡 ∧ ({(𝑓‘0), (𝑓‘1)} ∈ 𝑒 ∧ {(𝑓‘0), (𝑓‘2)} ∈ 𝑒 ∧ {(𝑓‘1), (𝑓‘2)} ∈ 𝑒))
34	33, 17	wex 1777	. . . . . 6 wff ∃𝑓(𝑓:(0..^3)–1-1-onto→𝑡 ∧ ({(𝑓‘0), (𝑓‘1)} ∈ 𝑒 ∧ {(𝑓‘0), (𝑓‘2)} ∈ 𝑒 ∧ {(𝑓‘1), (𝑓‘2)} ∈ 𝑒))
35	4	cv 1536	. . . . . . 7 class 𝑣
36	35	cpw 4622	. . . . . 6 class 𝒫 𝑣
37	34, 15, 36	crab 3438	. . . . 5 class {𝑡 ∈ 𝒫 𝑣 ∣ ∃𝑓(𝑓:(0..^3)–1-1-onto→𝑡 ∧ ({(𝑓‘0), (𝑓‘1)} ∈ 𝑒 ∧ {(𝑓‘0), (𝑓‘2)} ∈ 𝑒 ∧ {(𝑓‘1), (𝑓‘2)} ∈ 𝑒))}
38	8, 10, 37	csb 3915	. . . 4 class ⦋(Edg‘𝑔) / 𝑒⦌{𝑡 ∈ 𝒫 𝑣 ∣ ∃𝑓(𝑓:(0..^3)–1-1-onto→𝑡 ∧ ({(𝑓‘0), (𝑓‘1)} ∈ 𝑒 ∧ {(𝑓‘0), (𝑓‘2)} ∈ 𝑒 ∧ {(𝑓‘1), (𝑓‘2)} ∈ 𝑒))}
39	4, 7, 38	csb 3915	. . 3 class ⦋(Vtx‘𝑔) / 𝑣⦌⦋(Edg‘𝑔) / 𝑒⦌{𝑡 ∈ 𝒫 𝑣 ∣ ∃𝑓(𝑓:(0..^3)–1-1-onto→𝑡 ∧ ({(𝑓‘0), (𝑓‘1)} ∈ 𝑒 ∧ {(𝑓‘0), (𝑓‘2)} ∈ 𝑒 ∧ {(𝑓‘1), (𝑓‘2)} ∈ 𝑒))}
40	2, 3, 39	cmpt 5252	. 2 class (𝑔 ∈ V ↦ ⦋(Vtx‘𝑔) / 𝑣⦌⦋(Edg‘𝑔) / 𝑒⦌{𝑡 ∈ 𝒫 𝑣 ∣ ∃𝑓(𝑓:(0..^3)–1-1-onto→𝑡 ∧ ({(𝑓‘0), (𝑓‘1)} ∈ 𝑒 ∧ {(𝑓‘0), (𝑓‘2)} ∈ 𝑒 ∧ {(𝑓‘1), (𝑓‘2)} ∈ 𝑒))})
41	1, 40	wceq 1537	1 wff GrTriangles = (𝑔 ∈ V ↦ ⦋(Vtx‘𝑔) / 𝑣⦌⦋(Edg‘𝑔) / 𝑒⦌{𝑡 ∈ 𝒫 𝑣 ∣ ∃𝑓(𝑓:(0..^3)–1-1-onto→𝑡 ∧ ({(𝑓‘0), (𝑓‘1)} ∈ 𝑒 ∧ {(𝑓‘0), (𝑓‘2)} ∈ 𝑒 ∧ {(𝑓‘1), (𝑓‘2)} ∈ 𝑒))})

This definition is referenced by:  grtri  47721