Definition df-2spthsot 26388

Description: Define the collection of all simple paths of length 2 as ordered triple (in a graph). (Contributed by Alexander van der Vekens, 1-Mar-2018.)

Assertion

Ref	Expression
df-2spthsot	⊢ 2SPathsOt = (𝑣 ∈ V, 𝑒 ∈ V ↦ {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑎 ∈ 𝑣 ∃𝑏 ∈ 𝑣 𝑡 ∈ (𝑎(𝑣 2SPathOnOt 𝑒)𝑏)})

Distinct variable group:   𝑎,𝑏,𝑒,𝑣,𝑡

Detailed syntax breakdown of Definition df-2spthsot

Step	Hyp	Ref	Expression
1		c2spthot 26383	. 2 class 2SPathsOt
2		vv	. . 3 setvar 𝑣
3		ve	. . 3 setvar 𝑒
4		cvv 3173	. . 3 class V
5		vt	. . . . . . . 8 setvar 𝑡
6	5	cv 1474	. . . . . . 7 class 𝑡
7		va	. . . . . . . . 9 setvar 𝑎
8	7	cv 1474	. . . . . . . 8 class 𝑎
9		vb	. . . . . . . . 9 setvar 𝑏
10	9	cv 1474	. . . . . . . 8 class 𝑏
11	2	cv 1474	. . . . . . . . 9 class 𝑣
12	3	cv 1474	. . . . . . . . 9 class 𝑒
13		c2pthonot 26384	. . . . . . . . 9 class 2SPathOnOt
14	11, 12, 13	co 6549	. . . . . . . 8 class (𝑣 2SPathOnOt 𝑒)
15	8, 10, 14	co 6549	. . . . . . 7 class (𝑎(𝑣 2SPathOnOt 𝑒)𝑏)
16	6, 15	wcel 1977	. . . . . 6 wff 𝑡 ∈ (𝑎(𝑣 2SPathOnOt 𝑒)𝑏)
17	16, 9, 11	wrex 2897	. . . . 5 wff ∃𝑏 ∈ 𝑣 𝑡 ∈ (𝑎(𝑣 2SPathOnOt 𝑒)𝑏)
18	17, 7, 11	wrex 2897	. . . 4 wff ∃𝑎 ∈ 𝑣 ∃𝑏 ∈ 𝑣 𝑡 ∈ (𝑎(𝑣 2SPathOnOt 𝑒)𝑏)
19	11, 11	cxp 5036	. . . . 5 class (𝑣 × 𝑣)
20	19, 11	cxp 5036	. . . 4 class ((𝑣 × 𝑣) × 𝑣)
21	18, 5, 20	crab 2900	. . 3 class {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑎 ∈ 𝑣 ∃𝑏 ∈ 𝑣 𝑡 ∈ (𝑎(𝑣 2SPathOnOt 𝑒)𝑏)}
22	2, 3, 4, 4, 21	cmpt2 6551	. 2 class (𝑣 ∈ V, 𝑒 ∈ V ↦ {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑎 ∈ 𝑣 ∃𝑏 ∈ 𝑣 𝑡 ∈ (𝑎(𝑣 2SPathOnOt 𝑒)𝑏)})
23	1, 22	wceq 1475	1 wff 2SPathsOt = (𝑣 ∈ V, 𝑒 ∈ V ↦ {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑎 ∈ 𝑣 ∃𝑏 ∈ 𝑣 𝑡 ∈ (𝑎(𝑣 2SPathOnOt 𝑒)𝑏)})

This definition is referenced by:  2spthsot  26395