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

Definition df-2wlkonot 30377
Description: Define the collection of walks of length 2 with particular endpoints as ordered triple (in a graph). (Contributed by Alexander van der Vekens, 15-Feb-2018.)
Assertion
Ref Expression
df-2wlkonot  |- 2WalksOnOt  =  ( v  e.  _V , 
e  e.  _V  |->  ( a  e.  v ,  b  e.  v  |->  { t  e.  ( ( v  X.  v )  X.  v )  |  E. f E. p
( f ( a ( v WalkOn  e ) b ) p  /\  ( # `  f )  =  2  /\  (
( 1st `  ( 1st `  t ) )  =  a  /\  ( 2nd `  ( 1st `  t
) )  =  ( p `  1 )  /\  ( 2nd `  t
)  =  b ) ) } ) )
Distinct variable group:    a, b, e, v, t, f, p

Detailed syntax breakdown of Definition df-2wlkonot
StepHypRef Expression
1 c2wlkonot 30374 . 2  class 2WalksOnOt
2 vv . . 3  setvar  v
3 ve . . 3  setvar  e
4 cvv 2972 . . 3  class  _V
5 va . . . 4  setvar  a
6 vb . . . 4  setvar  b
72cv 1368 . . . 4  class  v
8 vf . . . . . . . . . 10  setvar  f
98cv 1368 . . . . . . . . 9  class  f
10 vp . . . . . . . . . 10  setvar  p
1110cv 1368 . . . . . . . . 9  class  p
125cv 1368 . . . . . . . . . 10  class  a
136cv 1368 . . . . . . . . . 10  class  b
143cv 1368 . . . . . . . . . . 11  class  e
15 cwlkon 23409 . . . . . . . . . . 11  class WalkOn
167, 14, 15co 6091 . . . . . . . . . 10  class  ( v WalkOn 
e )
1712, 13, 16co 6091 . . . . . . . . 9  class  ( a ( v WalkOn  e ) b )
189, 11, 17wbr 4292 . . . . . . . 8  wff  f ( a ( v WalkOn  e
) b ) p
19 chash 12103 . . . . . . . . . 10  class  #
209, 19cfv 5418 . . . . . . . . 9  class  ( # `  f )
21 c2 10371 . . . . . . . . 9  class  2
2220, 21wceq 1369 . . . . . . . 8  wff  ( # `  f )  =  2
23 vt . . . . . . . . . . . . 13  setvar  t
2423cv 1368 . . . . . . . . . . . 12  class  t
25 c1st 6575 . . . . . . . . . . . 12  class  1st
2624, 25cfv 5418 . . . . . . . . . . 11  class  ( 1st `  t )
2726, 25cfv 5418 . . . . . . . . . 10  class  ( 1st `  ( 1st `  t
) )
2827, 12wceq 1369 . . . . . . . . 9  wff  ( 1st `  ( 1st `  t
) )  =  a
29 c2nd 6576 . . . . . . . . . . 11  class  2nd
3026, 29cfv 5418 . . . . . . . . . 10  class  ( 2nd `  ( 1st `  t
) )
31 c1 9283 . . . . . . . . . . 11  class  1
3231, 11cfv 5418 . . . . . . . . . 10  class  ( p `
 1 )
3330, 32wceq 1369 . . . . . . . . 9  wff  ( 2nd `  ( 1st `  t
) )  =  ( p `  1 )
3424, 29cfv 5418 . . . . . . . . . 10  class  ( 2nd `  t )
3534, 13wceq 1369 . . . . . . . . 9  wff  ( 2nd `  t )  =  b
3628, 33, 35w3a 965 . . . . . . . 8  wff  ( ( 1st `  ( 1st `  t ) )  =  a  /\  ( 2nd `  ( 1st `  t
) )  =  ( p `  1 )  /\  ( 2nd `  t
)  =  b )
3718, 22, 36w3a 965 . . . . . . 7  wff  ( f ( a ( v WalkOn 
e ) b ) p  /\  ( # `  f )  =  2  /\  ( ( 1st `  ( 1st `  t
) )  =  a  /\  ( 2nd `  ( 1st `  t ) )  =  ( p ` 
1 )  /\  ( 2nd `  t )  =  b ) )
3837, 10wex 1586 . . . . . 6  wff  E. p
( f ( a ( v WalkOn  e ) b ) p  /\  ( # `  f )  =  2  /\  (
( 1st `  ( 1st `  t ) )  =  a  /\  ( 2nd `  ( 1st `  t
) )  =  ( p `  1 )  /\  ( 2nd `  t
)  =  b ) )
3938, 8wex 1586 . . . . 5  wff  E. f E. p ( f ( a ( v WalkOn  e
) b ) p  /\  ( # `  f
)  =  2  /\  ( ( 1st `  ( 1st `  t ) )  =  a  /\  ( 2nd `  ( 1st `  t
) )  =  ( p `  1 )  /\  ( 2nd `  t
)  =  b ) )
407, 7cxp 4838 . . . . . 6  class  ( v  X.  v )
4140, 7cxp 4838 . . . . 5  class  ( ( v  X.  v )  X.  v )
4239, 23, 41crab 2719 . . . 4  class  { t  e.  ( ( v  X.  v )  X.  v )  |  E. f E. p ( f ( a ( v WalkOn 
e ) b ) p  /\  ( # `  f )  =  2  /\  ( ( 1st `  ( 1st `  t
) )  =  a  /\  ( 2nd `  ( 1st `  t ) )  =  ( p ` 
1 )  /\  ( 2nd `  t )  =  b ) ) }
435, 6, 7, 7, 42cmpt2 6093 . . 3  class  ( a  e.  v ,  b  e.  v  |->  { t  e.  ( ( v  X.  v )  X.  v )  |  E. f E. p ( f ( a ( v WalkOn 
e ) b ) p  /\  ( # `  f )  =  2  /\  ( ( 1st `  ( 1st `  t
) )  =  a  /\  ( 2nd `  ( 1st `  t ) )  =  ( p ` 
1 )  /\  ( 2nd `  t )  =  b ) ) } )
442, 3, 4, 4, 43cmpt2 6093 . 2  class  ( v  e.  _V ,  e  e.  _V  |->  ( a  e.  v ,  b  e.  v  |->  { t  e.  ( ( v  X.  v )  X.  v )  |  E. f E. p ( f ( a ( v WalkOn 
e ) b ) p  /\  ( # `  f )  =  2  /\  ( ( 1st `  ( 1st `  t
) )  =  a  /\  ( 2nd `  ( 1st `  t ) )  =  ( p ` 
1 )  /\  ( 2nd `  t )  =  b ) ) } ) )
451, 44wceq 1369 1  wff 2WalksOnOt  =  ( v  e.  _V , 
e  e.  _V  |->  ( a  e.  v ,  b  e.  v  |->  { t  e.  ( ( v  X.  v )  X.  v )  |  E. f E. p
( f ( a ( v WalkOn  e ) b ) p  /\  ( # `  f )  =  2  /\  (
( 1st `  ( 1st `  t ) )  =  a  /\  ( 2nd `  ( 1st `  t
) )  =  ( p `  1 )  /\  ( 2nd `  t
)  =  b ) ) } ) )
Colors of variables: wff setvar class
This definition is referenced by:  is2wlkonot  30382  2wlkonot3v  30394
  Copyright terms: Public domain W3C validator