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

Definition df-2spthonot 28057
Description: Define the collection of simple paths of length 2 with particular endpoints as ordered triple (in a graph) . (Contributed by Alexander van der Vekens, 1-Mar-2018.)
Assertion
Ref Expression
df-2spthonot  |- 2SPathOnOt  =  ( 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 SPathOn  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-2spthonot
StepHypRef Expression
1 c2pthonot 28054 . 2  class 2SPathOnOt
2 vv . . 3  set  v
3 ve . . 3  set  e
4 cvv 2916 . . 3  class  _V
5 va . . . 4  set  a
6 vb . . . 4  set  b
72cv 1648 . . . 4  class  v
8 vf . . . . . . . . . 10  set  f
98cv 1648 . . . . . . . . 9  class  f
10 vp . . . . . . . . . 10  set  p
1110cv 1648 . . . . . . . . 9  class  p
125cv 1648 . . . . . . . . . 10  class  a
136cv 1648 . . . . . . . . . 10  class  b
143cv 1648 . . . . . . . . . . 11  class  e
15 cspthon 21466 . . . . . . . . . . 11  class SPathOn
167, 14, 15co 6040 . . . . . . . . . 10  class  ( v SPathOn 
e )
1712, 13, 16co 6040 . . . . . . . . 9  class  ( a ( v SPathOn  e ) b )
189, 11, 17wbr 4172 . . . . . . . 8  wff  f ( a ( v SPathOn  e
) b ) p
19 chash 11573 . . . . . . . . . 10  class  #
209, 19cfv 5413 . . . . . . . . 9  class  ( # `  f )
21 c2 10005 . . . . . . . . 9  class  2
2220, 21wceq 1649 . . . . . . . 8  wff  ( # `  f )  =  2
23 vt . . . . . . . . . . . . 13  set  t
2423cv 1648 . . . . . . . . . . . 12  class  t
25 c1st 6306 . . . . . . . . . . . 12  class  1st
2624, 25cfv 5413 . . . . . . . . . . 11  class  ( 1st `  t )
2726, 25cfv 5413 . . . . . . . . . 10  class  ( 1st `  ( 1st `  t
) )
2827, 12wceq 1649 . . . . . . . . 9  wff  ( 1st `  ( 1st `  t
) )  =  a
29 c2nd 6307 . . . . . . . . . . 11  class  2nd
3026, 29cfv 5413 . . . . . . . . . 10  class  ( 2nd `  ( 1st `  t
) )
31 c1 8947 . . . . . . . . . . 11  class  1
3231, 11cfv 5413 . . . . . . . . . 10  class  ( p `
 1 )
3330, 32wceq 1649 . . . . . . . . 9  wff  ( 2nd `  ( 1st `  t
) )  =  ( p `  1 )
3424, 29cfv 5413 . . . . . . . . . 10  class  ( 2nd `  t )
3534, 13wceq 1649 . . . . . . . . 9  wff  ( 2nd `  t )  =  b
3628, 33, 35w3a 936 . . . . . . . 8  wff  ( ( 1st `  ( 1st `  t ) )  =  a  /\  ( 2nd `  ( 1st `  t
) )  =  ( p `  1 )  /\  ( 2nd `  t
)  =  b )
3718, 22, 36w3a 936 . . . . . . 7  wff  ( f ( a ( v SPathOn 
e ) b ) p  /\  ( # `  f )  =  2  /\  ( ( 1st `  ( 1st `  t
) )  =  a  /\  ( 2nd `  ( 1st `  t ) )  =  ( p ` 
1 )  /\  ( 2nd `  t )  =  b ) )
3837, 10wex 1547 . . . . . 6  wff  E. p
( f ( a ( v SPathOn  e ) b ) p  /\  ( # `  f )  =  2  /\  (
( 1st `  ( 1st `  t ) )  =  a  /\  ( 2nd `  ( 1st `  t
) )  =  ( p `  1 )  /\  ( 2nd `  t
)  =  b ) )
3938, 8wex 1547 . . . . 5  wff  E. f E. p ( f ( a ( v SPathOn  e
) b ) p  /\  ( # `  f
)  =  2  /\  ( ( 1st `  ( 1st `  t ) )  =  a  /\  ( 2nd `  ( 1st `  t
) )  =  ( p `  1 )  /\  ( 2nd `  t
)  =  b ) )
407, 7cxp 4835 . . . . . 6  class  ( v  X.  v )
4140, 7cxp 4835 . . . . 5  class  ( ( v  X.  v )  X.  v )
4239, 23, 41crab 2670 . . . 4  class  { t  e.  ( ( v  X.  v )  X.  v )  |  E. f E. p ( f ( a ( v SPathOn 
e ) b ) p  /\  ( # `  f )  =  2  /\  ( ( 1st `  ( 1st `  t
) )  =  a  /\  ( 2nd `  ( 1st `  t ) )  =  ( p ` 
1 )  /\  ( 2nd `  t )  =  b ) ) }
435, 6, 7, 7, 42cmpt2 6042 . . 3  class  ( a  e.  v ,  b  e.  v  |->  { t  e.  ( ( v  X.  v )  X.  v )  |  E. f E. p ( f ( a ( v SPathOn 
e ) b ) p  /\  ( # `  f )  =  2  /\  ( ( 1st `  ( 1st `  t
) )  =  a  /\  ( 2nd `  ( 1st `  t ) )  =  ( p ` 
1 )  /\  ( 2nd `  t )  =  b ) ) } )
442, 3, 4, 4, 43cmpt2 6042 . 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 SPathOn 
e ) b ) p  /\  ( # `  f )  =  2  /\  ( ( 1st `  ( 1st `  t
) )  =  a  /\  ( 2nd `  ( 1st `  t ) )  =  ( p ` 
1 )  /\  ( 2nd `  t )  =  b ) ) } ) )
451, 44wceq 1649 1  wff 2SPathOnOt  =  ( 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 SPathOn  e ) b ) p  /\  ( # `  f )  =  2  /\  (
( 1st `  ( 1st `  t ) )  =  a  /\  ( 2nd `  ( 1st `  t
) )  =  ( p `  1 )  /\  ( 2nd `  t
)  =  b ) ) } ) )
Colors of variables: wff set class
This definition is referenced by:  is2spthonot  28061  2spthonot3v  28073
  Copyright terms: Public domain W3C validator