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

Definition df-2wlkonot 25275
 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 WalkOn
Distinct variable group:   ,,,,,,

Detailed syntax breakdown of Definition df-2wlkonot
StepHypRef Expression
1 c2wlkonot 25272 . 2 2WalksOnOt
2 vv . . 3
3 ve . . 3
4 cvv 3059 . . 3
5 va . . . 4
6 vb . . . 4
72cv 1404 . . . 4
8 vf . . . . . . . . . 10
98cv 1404 . . . . . . . . 9
10 vp . . . . . . . . . 10
1110cv 1404 . . . . . . . . 9
125cv 1404 . . . . . . . . . 10
136cv 1404 . . . . . . . . . 10
143cv 1404 . . . . . . . . . . 11
15 cwlkon 24919 . . . . . . . . . . 11 WalkOn
167, 14, 15co 6278 . . . . . . . . . 10 WalkOn
1712, 13, 16co 6278 . . . . . . . . 9 WalkOn
189, 11, 17wbr 4395 . . . . . . . 8 WalkOn
19 chash 12452 . . . . . . . . . 10
209, 19cfv 5569 . . . . . . . . 9
21 c2 10626 . . . . . . . . 9
2220, 21wceq 1405 . . . . . . . 8
23 vt . . . . . . . . . . . . 13
2423cv 1404 . . . . . . . . . . . 12
25 c1st 6782 . . . . . . . . . . . 12
2624, 25cfv 5569 . . . . . . . . . . 11
2726, 25cfv 5569 . . . . . . . . . 10
2827, 12wceq 1405 . . . . . . . . 9
29 c2nd 6783 . . . . . . . . . . 11
3026, 29cfv 5569 . . . . . . . . . 10
31 c1 9523 . . . . . . . . . . 11
3231, 11cfv 5569 . . . . . . . . . 10
3330, 32wceq 1405 . . . . . . . . 9
3424, 29cfv 5569 . . . . . . . . . 10
3534, 13wceq 1405 . . . . . . . . 9
3628, 33, 35w3a 974 . . . . . . . 8
3718, 22, 36w3a 974 . . . . . . 7 WalkOn
3837, 10wex 1633 . . . . . 6 WalkOn
3938, 8wex 1633 . . . . 5 WalkOn
407, 7cxp 4821 . . . . . 6
4140, 7cxp 4821 . . . . 5
4239, 23, 41crab 2758 . . . 4 WalkOn
435, 6, 7, 7, 42cmpt2 6280 . . 3 WalkOn
442, 3, 4, 4, 43cmpt2 6280 . 2 WalkOn
451, 44wceq 1405 1 2WalksOnOt WalkOn
 Colors of variables: wff setvar class This definition is referenced by:  is2wlkonot  25280  2wlkonot3v  25292
 Copyright terms: Public domain W3C validator