df-spthson

Description: Define the collection of simple paths with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens, 1-Mar-2018) (Revised by AV, 9-Jan-2021)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cspthson	$class SPathsOn$
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		cspths	$class SPaths$
19	5 18	cfv	$class SPaths (g)$
20	10 16 19	wbr	$wff f SPaths (g) p$
21	17 20	wa	$wff (f (a TrailsOn (g) b) p \land f SPaths (g) p)$
22	21 8 9	copab	$class \{⟨f, p⟩ \| (f (a TrailsOn (g) b) p \land f SPaths (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 SPaths (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 SPaths (g) p)\}))$
25	0 24	wceq	$wff SPathsOn = (g \in V ⟼ (a \in Vtx (g), b \in Vtx (g) ⟼ \{⟨f, p⟩ \| (f (a TrailsOn (g) b) p \land f SPaths (g) p)\}))$

Metamath Proof Explorer

Definition df-spthson

Detailed syntax breakdown