Metamath Proof Explorer

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 . (TODO: and a cycle of length 3 ,see grtricycl ). (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 ) } ∈ 𝑒 ) ) } )