df-pthson

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpthson	$class PathsOn$
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		ctrlson	$class TrailsOn$
13	5 12	cfv	$class TrailsOn (g)$
14	7	cv	$setvar b$
15	11 14 13	co	$class (a TrailsOn (g) b)$
16	9	cv	$setvar p$
17	10 16 15	wbr	$wff f (a TrailsOn (g) b) p$
18		cpths	$class Paths$
19	5 18	cfv	$class Paths (g)$
20	10 16 19	wbr	$wff f Paths (g) p$
21	17 20	wa	$wff (f (a TrailsOn (g) b) p \land f Paths (g) p)$
22	21 8 9	copab	$class \{⟨f, p⟩ \| (f (a TrailsOn (g) b) p \land f Paths (g) p)\}$
23	3 7 6 6 22	cmpo	$class (a \in Vtx (g), b \in Vtx (g) ⟼ \{⟨f, p⟩ \| (f (a TrailsOn (g) b) p \land f Paths (g) p)\})$
24	1 2 23	cmpt	$class (g \in V ⟼ (a \in Vtx (g), b \in Vtx (g) ⟼ \{⟨f, p⟩ \| (f (a TrailsOn (g) b) p \land f Paths (g) p)\}))$
25	0 24	wceq	$wff PathsOn = (g \in V ⟼ (a \in Vtx (g), b \in Vtx (g) ⟼ \{⟨f, p⟩ \| (f (a TrailsOn (g) b) p \land f Paths (g) p)\}))$

Metamath Proof Explorer

Definition df-pthson

Detailed syntax breakdown