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

Definition df-spthon 24722
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 24710 . 2  class SPathOn
2 vv . . 3  setvar  v
3 ve . . 3  setvar  e
4 cvv 3106 . . 3  class  _V
5 va . . . 4  setvar  a
6 vb . . . 4  setvar  b
72cv 1397 . . . 4  class  v
8 vf . . . . . . . 8  setvar  f
98cv 1397 . . . . . . 7  class  f
10 vp . . . . . . . 8  setvar  p
1110cv 1397 . . . . . . 7  class  p
125cv 1397 . . . . . . . 8  class  a
136cv 1397 . . . . . . . 8  class  b
143cv 1397 . . . . . . . . 9  class  e
15 cwlkon 24707 . . . . . . . . 9  class WalkOn
167, 14, 15co 6270 . . . . . . . 8  class  ( v WalkOn 
e )
1712, 13, 16co 6270 . . . . . . 7  class  ( a ( v WalkOn  e ) b )
189, 11, 17wbr 4439 . . . . . 6  wff  f ( a ( v WalkOn  e
) b ) p
19 cspath 24706 . . . . . . . 8  class SPaths
207, 14, 19co 6270 . . . . . . 7  class  ( v SPaths 
e )
219, 11, 20wbr 4439 . . . . . 6  wff  f ( v SPaths  e ) p
2218, 21wa 367 . . . . 5  wff  ( f ( a ( v WalkOn 
e ) b ) p  /\  f ( v SPaths  e ) p )
2322, 8, 10copab 4496 . . . 4  class  { <. f ,  p >.  |  ( f ( a ( v WalkOn  e ) b ) p  /\  f
( v SPaths  e )
p ) }
245, 6, 7, 7, 23cmpt2 6272 . . 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 6272 . 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 1398 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 setvar class
This definition is referenced by:  spthon  24789  spthonprp  24792
  Copyright terms: Public domain W3C validator