This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 Could not format assertion : No typesetting found for |- 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 ) ) } ) with typecode |-

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgrtri Could not format GrTriangles : No typesetting found for class GrTriangles with typecode class
1 vg setvar g
2 cvv class V
3 cvtx class Vtx
4 1 cv setvar g
5 4 3 cfv class Vtx ⁡ g
6 vv setvar v
7 cedg class Edg
8 4 7 cfv class Edg ⁡ g
9 ve setvar e
10 vt setvar t
11 6 cv setvar v
12 11 cpw class 𝒫 v
13 vf setvar f
14 13 cv setvar f
15 cc0 class 0
16 cfzo class ..^
17 c3 class 3
18 15 17 16 co class 0 ..^ 3
19 10 cv setvar t
20 18 19 14 wf1o wff f : 0 ..^ 3 ⟶ 1-1 onto t
21 15 14 cfv class f ⁡ 0
22 c1 class 1
23 22 14 cfv class f ⁡ 1
24 21 23 cpr class f ⁡ 0 f ⁡ 1
25 9 cv setvar e
26 24 25 wcel wff f ⁡ 0 f ⁡ 1 ∈ e
27 c2 class 2
28 27 14 cfv class f ⁡ 2
29 21 28 cpr class f ⁡ 0 f ⁡ 2
30 29 25 wcel wff f ⁡ 0 f ⁡ 2 ∈ e
31 23 28 cpr class f ⁡ 1 f ⁡ 2
32 31 25 wcel wff f ⁡ 1 f ⁡ 2 ∈ e
33 26 30 32 w3a wff f ⁡ 0 f ⁡ 1 ∈ e ∧ f ⁡ 0 f ⁡ 2 ∈ e ∧ f ⁡ 1 f ⁡ 2 ∈ e
34 20 33 wa wff f : 0 ..^ 3 ⟶ 1-1 onto t ∧ f ⁡ 0 f ⁡ 1 ∈ e ∧ f ⁡ 0 f ⁡ 2 ∈ e ∧ f ⁡ 1 f ⁡ 2 ∈ e
35 34 13 wex wff ∃ f f : 0 ..^ 3 ⟶ 1-1 onto t ∧ f ⁡ 0 f ⁡ 1 ∈ e ∧ f ⁡ 0 f ⁡ 2 ∈ e ∧ f ⁡ 1 f ⁡ 2 ∈ e
36 35 10 12 crab class t ∈ 𝒫 v | ∃ f f : 0 ..^ 3 ⟶ 1-1 onto t ∧ f ⁡ 0 f ⁡ 1 ∈ e ∧ f ⁡ 0 f ⁡ 2 ∈ e ∧ f ⁡ 1 f ⁡ 2 ∈ e
37 9 8 36 csb class ⦋ Edg ⁡ g / e⦌ t ∈ 𝒫 v | ∃ f f : 0 ..^ 3 ⟶ 1-1 onto t ∧ f ⁡ 0 f ⁡ 1 ∈ e ∧ f ⁡ 0 f ⁡ 2 ∈ e ∧ f ⁡ 1 f ⁡ 2 ∈ e
38 6 5 37 csb class ⦋ Vtx ⁡ g / v⦌ ⦋ Edg ⁡ g / e⦌ t ∈ 𝒫 v | ∃ f f : 0 ..^ 3 ⟶ 1-1 onto t ∧ f ⁡ 0 f ⁡ 1 ∈ e ∧ f ⁡ 0 f ⁡ 2 ∈ e ∧ f ⁡ 1 f ⁡ 2 ∈ e
39 1 2 38 cmpt class g ∈ V ⟼ ⦋ Vtx ⁡ g / v⦌ ⦋ Edg ⁡ g / e⦌ t ∈ 𝒫 v | ∃ f f : 0 ..^ 3 ⟶ 1-1 onto t ∧ f ⁡ 0 f ⁡ 1 ∈ e ∧ f ⁡ 0 f ⁡ 2 ∈ e ∧ f ⁡ 1 f ⁡ 2 ∈ e
40 0 39 wceq Could not format 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 ) ) } ) : No typesetting found for wff 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 ) ) } ) with typecode wff