MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-spthon Unicode version

Definition df-spthon 21478
Description: Define the collection of simple paths with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens, 1-Mar-2018.)
Assertion
Ref Expression
df-spthon  |- SPathOn  =  ( v  e.  _V , 
e  e.  _V  |->  ( a  e.  v ,  b  e.  v  |->  {
<. f ,  p >.  |  ( f ( a ( v WalkOn  e ) b ) p  /\  f ( v SPaths  e
) p ) } ) )
Distinct variable groups:    v, e,
f, p    a, b,
e, f, p, v

Detailed syntax breakdown of Definition df-spthon
StepHypRef Expression
1 cspthon 21466 . 2  class SPathOn
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 . . . . . . . 8  set  f
98cv 1648 . . . . . . 7  class  f
10 vp . . . . . . . 8  set  p
1110cv 1648 . . . . . . 7  class  p
125cv 1648 . . . . . . . 8  class  a
136cv 1648 . . . . . . . 8  class  b
143cv 1648 . . . . . . . . 9  class  e
15 cwlkon 21463 . . . . . . . . 9  class WalkOn
167, 14, 15co 6040 . . . . . . . 8  class  ( v WalkOn 
e )
1712, 13, 16co 6040 . . . . . . 7  class  ( a ( v WalkOn  e ) b )
189, 11, 17wbr 4172 . . . . . 6  wff  f ( a ( v WalkOn  e
) b ) p
19 cspath 21462 . . . . . . . 8  class SPaths
207, 14, 19co 6040 . . . . . . 7  class  ( v SPaths 
e )
219, 11, 20wbr 4172 . . . . . 6  wff  f ( v SPaths  e ) p
2218, 21wa 359 . . . . 5  wff  ( f ( a ( v WalkOn 
e ) b ) p  /\  f ( v SPaths  e ) p )
2322, 8, 10copab 4225 . . . 4  class  { <. f ,  p >.  |  ( f ( a ( v WalkOn  e ) b ) p  /\  f
( v SPaths  e )
p ) }
245, 6, 7, 7, 23cmpt2 6042 . . 3  class  ( a  e.  v ,  b  e.  v  |->  { <. f ,  p >.  |  ( f ( a ( v WalkOn  e ) b ) p  /\  f
( v SPaths  e )
p ) } )
252, 3, 4, 4, 24cmpt2 6042 . 2  class  ( v  e.  _V ,  e  e.  _V  |->  ( a  e.  v ,  b  e.  v  |->  { <. f ,  p >.  |  ( f ( a ( v WalkOn  e ) b ) p  /\  f
( v SPaths  e )
p ) } ) )
261, 25wceq 1649 1  wff SPathOn  =  ( v  e.  _V , 
e  e.  _V  |->  ( a  e.  v ,  b  e.  v  |->  {
<. f ,  p >.  |  ( f ( a ( v WalkOn  e ) b ) p  /\  f ( v SPaths  e
) p ) } ) )
Colors of variables: wff set class
This definition is referenced by:  spthon  21535  spthonprp  21538
  Copyright terms: Public domain W3C validator