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

Step	Hyp	Ref	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 𝑏
7	2	cv 1474	. . . 4 class 𝑣
8		vf	. . . . . . . . . 10 setvar 𝑓
9	8	cv 1474	. . . . . . . . 9 class 𝑓
10		vp	. . . . . . . . . 10 setvar 𝑝
11	10	cv 1474	. . . . . . . . 9 class 𝑝
12	5	cv 1474	. . . . . . . . . 10 class 𝑎
13	6	cv 1474	. . . . . . . . . 10 class 𝑏
14	3	cv 1474	. . . . . . . . . . 11 class 𝑒
15		cspthon 26033	. . . . . . . . . . 11 class SPathOn
16	7, 14, 15	co 6549	. . . . . . . . . 10 class (𝑣 SPathOn 𝑒)
17	12, 13, 16	co 6549	. . . . . . . . 9 class (𝑎(𝑣 SPathOn 𝑒)𝑏)
18	9, 11, 17	wbr 4583	. . . . . . . 8 wff 𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝
19		chash 12979	. . . . . . . . . 10 class #
20	9, 19	cfv 5804	. . . . . . . . 9 class (#‘𝑓)
21		c2 10947	. . . . . . . . 9 class 2
22	20, 21	wceq 1475	. . . . . . . 8 wff (#‘𝑓) = 2
23		vt	. . . . . . . . . . . . 13 setvar 𝑡
24	23	cv 1474	. . . . . . . . . . . 12 class 𝑡
25		c1st 7057	. . . . . . . . . . . 12 class 1st
26	24, 25	cfv 5804	. . . . . . . . . . 11 class (1st ‘𝑡)
27	26, 25	cfv 5804	. . . . . . . . . 10 class (1st ‘(1st ‘𝑡))
28	27, 12	wceq 1475	. . . . . . . . 9 wff (1st ‘(1st ‘𝑡)) = 𝑎
29		c2nd 7058	. . . . . . . . . . 11 class 2nd
30	26, 29	cfv 5804	. . . . . . . . . 10 class (2nd ‘(1st ‘𝑡))
31		c1 9816	. . . . . . . . . . 11 class 1
32	31, 11	cfv 5804	. . . . . . . . . 10 class (𝑝‘1)
33	30, 32	wceq 1475	. . . . . . . . 9 wff (2nd ‘(1st ‘𝑡)) = (𝑝‘1)
34	24, 29	cfv 5804	. . . . . . . . . 10 class (2nd ‘𝑡)
35	34, 13	wceq 1475	. . . . . . . . 9 wff (2nd ‘𝑡) = 𝑏
36	28, 33, 35	w3a 1031	. . . . . . . 8 wff ((1st ‘(1st ‘𝑡)) = 𝑎 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝑏)
37	18, 22, 36	w3a 1031	. . . . . . 7 wff (𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝑎 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝑏))
38	37, 10	wex 1695	. . . . . 6 wff ∃𝑝(𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝑎 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝑏))
39	38, 8	wex 1695	. . . . 5 wff ∃𝑓∃𝑝(𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝑎 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝑏))
40	7, 7	cxp 5036	. . . . . 6 class (𝑣 × 𝑣)
41	40, 7	cxp 5036	. . . . 5 class ((𝑣 × 𝑣) × 𝑣)
42	39, 23, 41	crab 2900	. . . 4 class {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝑎 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝑏))}
43	5, 6, 7, 7, 42	cmpt2 6551	. . 3 class (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝑎 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝑏))})
44	2, 3, 4, 4, 43	cmpt2 6551	. 2 class (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝑎 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝑏))}))
45	1, 44	wceq 1475	1 wff 2SPathOnOt = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝑎 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝑏))}))

This definition is referenced by:  is2spthonot  26391  2spthonot3v  26403