Definition df-grtri 47839

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 47846, and the vertices of a cycle of size 3 are a triangle in a graph, see cycl3grtri 47848. (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 47838	. 2 class GrTriangles
2		vg	. . 3 setvar 𝑔
3		cvv 3463	. . 3 class V
4		vv	. . . 4 setvar 𝑣
5	2	cv 1538	. . . . 5 class 𝑔
6		cvtx 28940	. . . . 5 class Vtx
7	5, 6	cfv 6540	. . . 4 class (Vtx‘𝑔)
8		ve	. . . . 5 setvar 𝑒
9		cedg 28991	. . . . . 6 class Edg
10	5, 9	cfv 6540	. . . . 5 class (Edg‘𝑔)
11		cc0 11136	. . . . . . . . . 10 class 0
12		c3 12303	. . . . . . . . . 10 class 3
13		cfzo 13675	. . . . . . . . . 10 class ..^
14	11, 12, 13	co 7412	. . . . . . . . 9 class (0..^3)
15		vt	. . . . . . . . . 10 setvar 𝑡
16	15	cv 1538	. . . . . . . . 9 class 𝑡
17		vf	. . . . . . . . . 10 setvar 𝑓
18	17	cv 1538	. . . . . . . . 9 class 𝑓
19	14, 16, 18	wf1o 6539	. . . . . . . 8 wff 𝑓:(0..^3)–1-1-onto→𝑡
20	11, 18	cfv 6540	. . . . . . . . . . 11 class (𝑓‘0)
21		c1 11137	. . . . . . . . . . . 12 class 1
22	21, 18	cfv 6540	. . . . . . . . . . 11 class (𝑓‘1)
23	20, 22	cpr 4608	. . . . . . . . . 10 class {(𝑓‘0), (𝑓‘1)}
24	8	cv 1538	. . . . . . . . . 10 class 𝑒
25	23, 24	wcel 2107	. . . . . . . . 9 wff {(𝑓‘0), (𝑓‘1)} ∈ 𝑒
26		c2 12302	. . . . . . . . . . . 12 class 2
27	26, 18	cfv 6540	. . . . . . . . . . 11 class (𝑓‘2)
28	20, 27	cpr 4608	. . . . . . . . . 10 class {(𝑓‘0), (𝑓‘2)}
29	28, 24	wcel 2107	. . . . . . . . 9 wff {(𝑓‘0), (𝑓‘2)} ∈ 𝑒
30	22, 27	cpr 4608	. . . . . . . . . 10 class {(𝑓‘1), (𝑓‘2)}
31	30, 24	wcel 2107	. . . . . . . . 9 wff {(𝑓‘1), (𝑓‘2)} ∈ 𝑒
32	25, 29, 31	w3a 1086	. . . . . . . 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 1778	. . . . . 6 wff ∃𝑓(𝑓:(0..^3)–1-1-onto→𝑡 ∧ ({(𝑓‘0), (𝑓‘1)} ∈ 𝑒 ∧ {(𝑓‘0), (𝑓‘2)} ∈ 𝑒 ∧ {(𝑓‘1), (𝑓‘2)} ∈ 𝑒))
35	4	cv 1538	. . . . . . 7 class 𝑣
36	35	cpw 4580	. . . . . 6 class 𝒫 𝑣
37	34, 15, 36	crab 3419	. . . . 5 class {𝑡 ∈ 𝒫 𝑣 ∣ ∃𝑓(𝑓:(0..^3)–1-1-onto→𝑡 ∧ ({(𝑓‘0), (𝑓‘1)} ∈ 𝑒 ∧ {(𝑓‘0), (𝑓‘2)} ∈ 𝑒 ∧ {(𝑓‘1), (𝑓‘2)} ∈ 𝑒))}
38	8, 10, 37	csb 3879	. . . 4 class ⦋(Edg‘𝑔) / 𝑒⦌{𝑡 ∈ 𝒫 𝑣 ∣ ∃𝑓(𝑓:(0..^3)–1-1-onto→𝑡 ∧ ({(𝑓‘0), (𝑓‘1)} ∈ 𝑒 ∧ {(𝑓‘0), (𝑓‘2)} ∈ 𝑒 ∧ {(𝑓‘1), (𝑓‘2)} ∈ 𝑒))}
39	4, 7, 38	csb 3879	. . 3 class ⦋(Vtx‘𝑔) / 𝑣⦌⦋(Edg‘𝑔) / 𝑒⦌{𝑡 ∈ 𝒫 𝑣 ∣ ∃𝑓(𝑓:(0..^3)–1-1-onto→𝑡 ∧ ({(𝑓‘0), (𝑓‘1)} ∈ 𝑒 ∧ {(𝑓‘0), (𝑓‘2)} ∈ 𝑒 ∧ {(𝑓‘1), (𝑓‘2)} ∈ 𝑒))}
40	2, 3, 39	cmpt 5205	. 2 class (𝑔 ∈ V ↦ ⦋(Vtx‘𝑔) / 𝑣⦌⦋(Edg‘𝑔) / 𝑒⦌{𝑡 ∈ 𝒫 𝑣 ∣ ∃𝑓(𝑓:(0..^3)–1-1-onto→𝑡 ∧ ({(𝑓‘0), (𝑓‘1)} ∈ 𝑒 ∧ {(𝑓‘0), (𝑓‘2)} ∈ 𝑒 ∧ {(𝑓‘1), (𝑓‘2)} ∈ 𝑒))})
41	1, 40	wceq 1539	1 wff GrTriangles = (𝑔 ∈ V ↦ ⦋(Vtx‘𝑔) / 𝑣⦌⦋(Edg‘𝑔) / 𝑒⦌{𝑡 ∈ 𝒫 𝑣 ∣ ∃𝑓(𝑓:(0..^3)–1-1-onto→𝑡 ∧ ({(𝑓‘0), (𝑓‘1)} ∈ 𝑒 ∧ {(𝑓‘0), (𝑓‘2)} ∈ 𝑒 ∧ {(𝑓‘1), (𝑓‘2)} ∈ 𝑒))})

This definition is referenced by:  grtri  47841