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

Definition df-2spthonot 26387
 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, 𝑒 ∈ V ↦ (𝑎𝑣, 𝑏𝑣 ↦ {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))}))
Distinct variable group:   𝑎,𝑏,𝑒,𝑣,𝑡,𝑓,𝑝

Detailed syntax breakdown of Definition df-2spthonot
StepHypRef Expression
1 c2pthonot 26384 . 2 class 2SPathOnOt
2 vv . . 3 setvar 𝑣
3 ve . . 3 setvar 𝑒
4 cvv 3173 . . 3 class V
5 va . . . 4 setvar 𝑎
6 vb . . . 4 setvar 𝑏
72cv 1474 . . . 4 class 𝑣
8 vf . . . . . . . . . 10 setvar 𝑓
98cv 1474 . . . . . . . . 9 class 𝑓
10 vp . . . . . . . . . 10 setvar 𝑝
1110cv 1474 . . . . . . . . 9 class 𝑝
125cv 1474 . . . . . . . . . 10 class 𝑎
136cv 1474 . . . . . . . . . 10 class 𝑏
143cv 1474 . . . . . . . . . . 11 class 𝑒
15 cspthon 26033 . . . . . . . . . . 11 class SPathOn
167, 14, 15co 6549 . . . . . . . . . 10 class (𝑣 SPathOn 𝑒)
1712, 13, 16co 6549 . . . . . . . . 9 class (𝑎(𝑣 SPathOn 𝑒)𝑏)
189, 11, 17wbr 4583 . . . . . . . 8 wff 𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝
19 chash 12979 . . . . . . . . . 10 class #
209, 19cfv 5804 . . . . . . . . 9 class (#‘𝑓)
21 c2 10947 . . . . . . . . 9 class 2
2220, 21wceq 1475 . . . . . . . 8 wff (#‘𝑓) = 2
23 vt . . . . . . . . . . . . 13 setvar 𝑡
2423cv 1474 . . . . . . . . . . . 12 class 𝑡
25 c1st 7057 . . . . . . . . . . . 12 class 1st
2624, 25cfv 5804 . . . . . . . . . . 11 class (1st𝑡)
2726, 25cfv 5804 . . . . . . . . . 10 class (1st ‘(1st𝑡))
2827, 12wceq 1475 . . . . . . . . 9 wff (1st ‘(1st𝑡)) = 𝑎
29 c2nd 7058 . . . . . . . . . . 11 class 2nd
3026, 29cfv 5804 . . . . . . . . . 10 class (2nd ‘(1st𝑡))
31 c1 9816 . . . . . . . . . . 11 class 1
3231, 11cfv 5804 . . . . . . . . . 10 class (𝑝‘1)
3330, 32wceq 1475 . . . . . . . . 9 wff (2nd ‘(1st𝑡)) = (𝑝‘1)
3424, 29cfv 5804 . . . . . . . . . 10 class (2nd𝑡)
3534, 13wceq 1475 . . . . . . . . 9 wff (2nd𝑡) = 𝑏
3628, 33, 35w3a 1031 . . . . . . . 8 wff ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏)
3718, 22, 36w3a 1031 . . . . . . 7 wff (𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))
3837, 10wex 1695 . . . . . 6 wff 𝑝(𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))
3938, 8wex 1695 . . . . 5 wff 𝑓𝑝(𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))
407, 7cxp 5036 . . . . . 6 class (𝑣 × 𝑣)
4140, 7cxp 5036 . . . . 5 class ((𝑣 × 𝑣) × 𝑣)
4239, 23, 41crab 2900 . . . 4 class {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))}
435, 6, 7, 7, 42cmpt2 6551 . . 3 class (𝑎𝑣, 𝑏𝑣 ↦ {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))})
442, 3, 4, 4, 43cmpt2 6551 . 2 class (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎𝑣, 𝑏𝑣 ↦ {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))}))
451, 44wceq 1475 1 wff 2SPathOnOt = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎𝑣, 𝑏𝑣 ↦ {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑓𝑝(𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st𝑡)) = 𝑎 ∧ (2nd ‘(1st𝑡)) = (𝑝‘1) ∧ (2nd𝑡) = 𝑏))}))
 Colors of variables: wff setvar class This definition is referenced by:  is2spthonot  26391  2spthonot3v  26403
 Copyright terms: Public domain W3C validator