df-trlson

Description: Define the collection of trails with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017) (Revised by AV, 28-Dec-2020)

		Ref	Expression
	Assertion	df-trlson	$⊢ TrailsOn = (g \in V ⟼ (a \in Vtx (g), b \in Vtx (g) ⟼ \{⟨f, p⟩ \| (f (a WalksOn (g) b) p \land f Trails (g) p)\}))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctrlson	$class TrailsOn$
1		vg	$setvar g$
2		cvv	$class V$
3		va	$setvar a$
4		cvtx	$class Vtx$
5	1	cv	$setvar g$
6	5 4	cfv	$class Vtx (g)$
7		vb	$setvar b$
8		vf	$setvar f$
9		vp	$setvar p$
10	8	cv	$setvar f$
11	3	cv	$setvar a$
12		cwlkson	$class WalksOn$
13	5 12	cfv	$class WalksOn (g)$
14	7	cv	$setvar b$
15	11 14 13	co	$class (a WalksOn (g) b)$
16	9	cv	$setvar p$
17	10 16 15	wbr	$wff f (a WalksOn (g) b) p$
18		ctrls	$class Trails$
19	5 18	cfv	$class Trails (g)$
20	10 16 19	wbr	$wff f Trails (g) p$
21	17 20	wa	$wff (f (a WalksOn (g) b) p \land f Trails (g) p)$
22	21 8 9	copab	$class \{⟨f, p⟩ \| (f (a WalksOn (g) b) p \land f Trails (g) p)\}$
23	3 7 6 6 22	cmpo	$class (a \in Vtx (g), b \in Vtx (g) ⟼ \{⟨f, p⟩ \| (f (a WalksOn (g) b) p \land f Trails (g) p)\})$
24	1 2 23	cmpt	$class (g \in V ⟼ (a \in Vtx (g), b \in Vtx (g) ⟼ \{⟨f, p⟩ \| (f (a WalksOn (g) b) p \land f Trails (g) p)\}))$
25	0 24	wceq	$wff TrailsOn = (g \in V ⟼ (a \in Vtx (g), b \in Vtx (g) ⟼ \{⟨f, p⟩ \| (f (a WalksOn (g) b) p \land f Trails (g) p)\}))$

Metamath Proof Explorer

Definition df-trlson

Detailed syntax breakdown