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

Definition df-2wlksot 26386
 Description: Define the collection of all walks of length 2 as ordered triple (in a graph). (Contributed by Alexander van der Vekens, 15-Feb-2018.)
Assertion
Ref Expression
df-2wlksot 2WalksOt = (𝑣 ∈ V, 𝑒 ∈ V ↦ {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑎𝑣𝑏𝑣 𝑡 ∈ (𝑎(𝑣 2WalksOnOt 𝑒)𝑏)})
Distinct variable group:   𝑎,𝑏,𝑒,𝑣,𝑡

Detailed syntax breakdown of Definition df-2wlksot
StepHypRef Expression
1 c2wlkot 26381 . 2 class 2WalksOt
2 vv . . 3 setvar 𝑣
3 ve . . 3 setvar 𝑒
4 cvv 3173 . . 3 class V
5 vt . . . . . . . 8 setvar 𝑡
65cv 1474 . . . . . . 7 class 𝑡
7 va . . . . . . . . 9 setvar 𝑎
87cv 1474 . . . . . . . 8 class 𝑎
9 vb . . . . . . . . 9 setvar 𝑏
109cv 1474 . . . . . . . 8 class 𝑏
112cv 1474 . . . . . . . . 9 class 𝑣
123cv 1474 . . . . . . . . 9 class 𝑒
13 c2wlkonot 26382 . . . . . . . . 9 class 2WalksOnOt
1411, 12, 13co 6549 . . . . . . . 8 class (𝑣 2WalksOnOt 𝑒)
158, 10, 14co 6549 . . . . . . 7 class (𝑎(𝑣 2WalksOnOt 𝑒)𝑏)
166, 15wcel 1977 . . . . . 6 wff 𝑡 ∈ (𝑎(𝑣 2WalksOnOt 𝑒)𝑏)
1716, 9, 11wrex 2897 . . . . 5 wff 𝑏𝑣 𝑡 ∈ (𝑎(𝑣 2WalksOnOt 𝑒)𝑏)
1817, 7, 11wrex 2897 . . . 4 wff 𝑎𝑣𝑏𝑣 𝑡 ∈ (𝑎(𝑣 2WalksOnOt 𝑒)𝑏)
1911, 11cxp 5036 . . . . 5 class (𝑣 × 𝑣)
2019, 11cxp 5036 . . . 4 class ((𝑣 × 𝑣) × 𝑣)
2118, 5, 20crab 2900 . . 3 class {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑎𝑣𝑏𝑣 𝑡 ∈ (𝑎(𝑣 2WalksOnOt 𝑒)𝑏)}
222, 3, 4, 4, 21cmpt2 6551 . 2 class (𝑣 ∈ V, 𝑒 ∈ V ↦ {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑎𝑣𝑏𝑣 𝑡 ∈ (𝑎(𝑣 2WalksOnOt 𝑒)𝑏)})
231, 22wceq 1475 1 wff 2WalksOt = (𝑣 ∈ V, 𝑒 ∈ V ↦ {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑎𝑣𝑏𝑣 𝑡 ∈ (𝑎(𝑣 2WalksOnOt 𝑒)𝑏)})
 Colors of variables: wff setvar class This definition is referenced by:  2wlksot  26394
 Copyright terms: Public domain W3C validator