Users' Mathboxes 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  =  ( v  e.  _V , 
e  e.  _V  |->  { t  e.  ( ( v  X.  v )  X.  v )  |  E. a  e.  v  E. b  e.  v  t  e.  ( a ( v 2WalksOnOt  e )
b ) } )
Distinct variable group:    a, b, e, v, t

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