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 , 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 = ( g e. _V |-> [_ ( Vtx ` g ) / v ]_ [_ ( Edg ` g ) / e ]_ { t e. ~P v | E. f ( f : ( 0 ..^ 3 ) -1-1-onto-> t /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. e /\ { ( f ` 0 ) , ( f ` 2 ) } e. e /\ { ( f ` 1 ) , ( f ` 2 ) } e. e ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgrtri 
 |-  GrTriangles
1 vg 
 |-  g
2 cvv 
 |-  _V
3 cvtx 
 |-  Vtx
4 1 cv 
 |-  g
5 4 3 cfv 
 |-  ( Vtx ` g )
6 vv 
 |-  v
7 cedg 
 |-  Edg
8 4 7 cfv 
 |-  ( Edg ` g )
9 ve 
 |-  e
10 vt 
 |-  t
11 6 cv 
 |-  v
12 11 cpw 
 |-  ~P v
13 vf 
 |-  f
14 13 cv 
 |-  f
15 cc0 
 |-  0
16 cfzo 
 |-  ..^
17 c3 
 |-  3
18 15 17 16 co 
 |-  ( 0 ..^ 3 )
19 10 cv 
 |-  t
20 18 19 14 wf1o 
 |-  f : ( 0 ..^ 3 ) -1-1-onto-> t
21 15 14 cfv 
 |-  ( f ` 0 )
22 c1 
 |-  1
23 22 14 cfv 
 |-  ( f ` 1 )
24 21 23 cpr 
 |-  { ( f ` 0 ) , ( f ` 1 ) }
25 9 cv 
 |-  e
26 24 25 wcel 
 |-  { ( f ` 0 ) , ( f ` 1 ) } e. e
27 c2 
 |-  2
28 27 14 cfv 
 |-  ( f ` 2 )
29 21 28 cpr 
 |-  { ( f ` 0 ) , ( f ` 2 ) }
30 29 25 wcel 
 |-  { ( f ` 0 ) , ( f ` 2 ) } e. e
31 23 28 cpr 
 |-  { ( f ` 1 ) , ( f ` 2 ) }
32 31 25 wcel 
 |-  { ( f ` 1 ) , ( f ` 2 ) } e. e
33 26 30 32 w3a 
 |-  ( { ( f ` 0 ) , ( f ` 1 ) } e. e /\ { ( f ` 0 ) , ( f ` 2 ) } e. e /\ { ( f ` 1 ) , ( f ` 2 ) } e. e )
34 20 33 wa 
 |-  ( f : ( 0 ..^ 3 ) -1-1-onto-> t /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. e /\ { ( f ` 0 ) , ( f ` 2 ) } e. e /\ { ( f ` 1 ) , ( f ` 2 ) } e. e ) )
35 34 13 wex 
 |-  E. f ( f : ( 0 ..^ 3 ) -1-1-onto-> t /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. e /\ { ( f ` 0 ) , ( f ` 2 ) } e. e /\ { ( f ` 1 ) , ( f ` 2 ) } e. e ) )
36 35 10 12 crab 
 |-  { t e. ~P v | E. f ( f : ( 0 ..^ 3 ) -1-1-onto-> t /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. e /\ { ( f ` 0 ) , ( f ` 2 ) } e. e /\ { ( f ` 1 ) , ( f ` 2 ) } e. e ) ) }
37 9 8 36 csb 
 |-  [_ ( Edg ` g ) / e ]_ { t e. ~P v | E. f ( f : ( 0 ..^ 3 ) -1-1-onto-> t /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. e /\ { ( f ` 0 ) , ( f ` 2 ) } e. e /\ { ( f ` 1 ) , ( f ` 2 ) } e. e ) ) }
38 6 5 37 csb 
 |-  [_ ( Vtx ` g ) / v ]_ [_ ( Edg ` g ) / e ]_ { t e. ~P v | E. f ( f : ( 0 ..^ 3 ) -1-1-onto-> t /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. e /\ { ( f ` 0 ) , ( f ` 2 ) } e. e /\ { ( f ` 1 ) , ( f ` 2 ) } e. e ) ) }
39 1 2 38 cmpt 
 |-  ( g e. _V |-> [_ ( Vtx ` g ) / v ]_ [_ ( Edg ` g ) / e ]_ { t e. ~P v | E. f ( f : ( 0 ..^ 3 ) -1-1-onto-> t /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. e /\ { ( f ` 0 ) , ( f ` 2 ) } e. e /\ { ( f ` 1 ) , ( f ` 2 ) } e. e ) ) } )
40 0 39 wceq 
 |-  GrTriangles = ( g e. _V |-> [_ ( Vtx ` g ) / v ]_ [_ ( Edg ` g ) / e ]_ { t e. ~P v | E. f ( f : ( 0 ..^ 3 ) -1-1-onto-> t /\ ( { ( f ` 0 ) , ( f ` 1 ) } e. e /\ { ( f ` 0 ) , ( f ` 2 ) } e. e /\ { ( f ` 1 ) , ( f ` 2 ) } e. e ) ) } )