Definition df-grtri

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 , and the vertices of a cycle of size 3 are a triangle in a graph, see cycl3grtri . (Contributed by AV, 20-Jul-2025)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgrtri	⊢ GrTriangles
1		vg	⊢ 𝑔
2		cvv	⊢ V
3		cvtx	⊢ Vtx
4	1	cv	⊢ 𝑔
5	4 3	cfv	⊢ ( Vtx ‘ 𝑔 )
6		vv	⊢ 𝑣
7		cedg	⊢ Edg
8	4 7	cfv	⊢ ( Edg ‘ 𝑔 )
9		ve	⊢ 𝑒
10		vt	⊢ 𝑡
11	6	cv	⊢ 𝑣
12	11	cpw	⊢ 𝒫 𝑣
13		vf	⊢ 𝑓
14	13	cv	⊢ 𝑓
15		cc0	⊢ 0
16		cfzo	⊢ ..^
17		c3	⊢ 3
18	15 17 16	co	⊢ ( 0 ..^ 3 )
19	10	cv	⊢ 𝑡
20	18 19 14	wf1o	⊢ 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡
21	15 14	cfv	⊢ ( 𝑓 ‘ 0 )
22		c1	⊢ 1
23	22 14	cfv	⊢ ( 𝑓 ‘ 1 )
24	21 23	cpr	⊢ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) }
25	9	cv	⊢ 𝑒
26	24 25	wcel	⊢ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝑒
27		c2	⊢ 2
28	27 14	cfv	⊢ ( 𝑓 ‘ 2 )
29	21 28	cpr	⊢ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) }
30	29 25	wcel	⊢ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒
31	23 28	cpr	⊢ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) }
32	31 25	wcel	⊢ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒
33	26 30 32	w3a	⊢ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 )
34	20 33	wa	⊢ ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ) )
35	34 13	wex	⊢ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ) )
36	35 10 12	crab	⊢ { 𝑡 ∈ 𝒫 𝑣 ∣ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ) ) }
37	9 8 36	csb	⊢ ⦋ ( Edg ‘ 𝑔 ) / 𝑒 ⦌ { 𝑡 ∈ 𝒫 𝑣 ∣ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ) ) }
38	6 5 37	csb	⊢ ⦋ ( Vtx ‘ 𝑔 ) / 𝑣 ⦌ ⦋ ( Edg ‘ 𝑔 ) / 𝑒 ⦌ { 𝑡 ∈ 𝒫 𝑣 ∣ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ) ) }
39	1 2 38	cmpt	⊢ ( 𝑔 ∈ V ↦ ⦋ ( Vtx ‘ 𝑔 ) / 𝑣 ⦌ ⦋ ( Edg ‘ 𝑔 ) / 𝑒 ⦌ { 𝑡 ∈ 𝒫 𝑣 ∣ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ) ) } )
40	0 39	wceq	⊢ GrTriangles = ( 𝑔 ∈ V ↦ ⦋ ( Vtx ‘ 𝑔 ) / 𝑣 ⦌ ⦋ ( Edg ‘ 𝑔 ) / 𝑒 ⦌ { 𝑡 ∈ 𝒫 𝑣 ∣ ∃ 𝑓 ( 𝑓 : ( 0 ..^ 3 ) –1-1-onto→ 𝑡 ∧ ( { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 1 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 0 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ∧ { ( 𝑓 ‘ 1 ) , ( 𝑓 ‘ 2 ) } ∈ 𝑒 ) ) } )