Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-2wlksot Structured version   Unicode version

Definition df-2wlksot 30519
 Description: Define the collection of all walks of length 2 as ordered triple (in a graph). (Contributed by Alexander van der Vekens, 15-Feb-2018.)
Assertion
Ref Expression
df-2wlksot 2WalksOt 2WalksOnOt
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-2wlksot
StepHypRef Expression
1 c2wlkot 30514 . 2 2WalksOt
2 vv . . 3
3 ve . . 3
4 cvv 3071 . . 3
5 vt . . . . . . . 8
65cv 1369 . . . . . . 7
7 va . . . . . . . . 9
87cv 1369 . . . . . . . 8
9 vb . . . . . . . . 9
109cv 1369 . . . . . . . 8
112cv 1369 . . . . . . . . 9
123cv 1369 . . . . . . . . 9
13 c2wlkonot 30515 . . . . . . . . 9 2WalksOnOt
1411, 12, 13co 6193 . . . . . . . 8 2WalksOnOt
158, 10, 14co 6193 . . . . . . 7 2WalksOnOt
166, 15wcel 1758 . . . . . 6 2WalksOnOt
1716, 9, 11wrex 2796 . . . . 5 2WalksOnOt
1817, 7, 11wrex 2796 . . . 4 2WalksOnOt
1911, 11cxp 4939 . . . . 5
2019, 11cxp 4939 . . . 4
2118, 5, 20crab 2799 . . 3 2WalksOnOt
222, 3, 4, 4, 21cmpt2 6195 . 2 2WalksOnOt
231, 22wceq 1370 1 2WalksOt 2WalksOnOt
 Colors of variables: wff setvar class This definition is referenced by:  2wlksot  30527
 Copyright terms: Public domain W3C validator