dfpth2

Description: Alternate definition for a pair of classes/functions to be a path (in an undirected graph). (Contributed by AV, 4-Oct-2025)

		Ref	Expression
	Assertion	dfpth2	$⊢ F Paths (G) P \leftrightarrow (F Trails (G) P \land Fun {({P ↾}_{(1 \dots \|F\|)})}^{-1} \land P (0) \notin P [(1 ..^\|F\|)])$

Proof

Step	Hyp	Ref	Expression
1		ispth	$⊢ F Paths (G) P \leftrightarrow (F Trails (G) P \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset)$
2		istrl	$⊢ F Trails (G) P \leftrightarrow (F Walks (G) P \land Fun F^{-1})$
3		wlkcl	$⊢ F Walks (G) P \to \|F\| \in ℕ_{0}$
4		eqid	$⊢ Vtx (G) = Vtx (G)$
5	4	wlkp	$⊢ F Walks (G) P \to P : (0 \dots \|F\|) ⟶ Vtx (G)$
6		ffn	$⊢ P : (0 \dots \|F\|) ⟶ Vtx (G) \to P Fn (0 \dots \|F\|)$
7	6	adantl	$⊢ (\|F\| \in ℕ_{0} \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \to P Fn (0 \dots \|F\|)$
8		0elfz	$⊢ \|F\| \in ℕ_{0} \to 0 \in (0 \dots \|F\|)$
9	8	adantr	$⊢ (\|F\| \in ℕ_{0} \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \to 0 \in (0 \dots \|F\|)$
10		nn0fz0	$⊢ \|F\| \in ℕ_{0} \leftrightarrow \|F\| \in (0 \dots \|F\|)$
11	10	birani	$⊢ (\|F\| \in ℕ_{0} \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \to \|F\| \in (0 \dots \|F\|)$
12	7 9 11	3jca	$⊢ (\|F\| \in ℕ_{0} \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \to (P Fn (0 \dots \|F\|) \land 0 \in (0 \dots \|F\|) \land \|F\| \in (0 \dots \|F\|))$
13	3 5 12	syl2anc	$⊢ F Walks (G) P \to (P Fn (0 \dots \|F\|) \land 0 \in (0 \dots \|F\|) \land \|F\| \in (0 \dots \|F\|))$
14	13	adantr	$⊢ (F Walks (G) P \land Fun F^{-1}) \to (P Fn (0 \dots \|F\|) \land 0 \in (0 \dots \|F\|) \land \|F\| \in (0 \dots \|F\|))$
15	2 14	sylbi	$⊢ F Trails (G) P \to (P Fn (0 \dots \|F\|) \land 0 \in (0 \dots \|F\|) \land \|F\| \in (0 \dots \|F\|))$
16		fnimapr	$⊢ (P Fn (0 \dots \|F\|) \land 0 \in (0 \dots \|F\|) \land \|F\| \in (0 \dots \|F\|)) \to P [\{0, \|F\|\}] = \{P (0), P (\|F\|)\}$
17	15 16	syl	$⊢ F Trails (G) P \to P [\{0, \|F\|\}] = \{P (0), P (\|F\|)\}$
18	17	ineq1d	$⊢ F Trails (G) P \to P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \{P (0), P (\|F\|)\} \cap P [(1 ..^\|F\|)]$
19	18	eqeq1d	$⊢ F Trails (G) P \to (P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset \leftrightarrow \{P (0), P (\|F\|)\} \cap P [(1 ..^\|F\|)] = \emptyset)$
20		disj	$⊢ \{P (0), P (\|F\|)\} \cap P [(1 ..^\|F\|)] = \emptyset \leftrightarrow \forall x \in \{P (0), P (\|F\|)\} \neg x \in P [(1 ..^\|F\|)]$
21		fvex	$⊢ P (0) \in V$
22		fvex	$⊢ P (\|F\|) \in V$
23		eleq1	$⊢ x = P (0) \to (x \in P [(1 ..^\|F\|)] \leftrightarrow P (0) \in P [(1 ..^\|F\|)])$
24	23	notbid	$⊢ x = P (0) \to (\neg x \in P [(1 ..^\|F\|)] \leftrightarrow \neg P (0) \in P [(1 ..^\|F\|)])$
25		eleq1	$⊢ x = P (\|F\|) \to (x \in P [(1 ..^\|F\|)] \leftrightarrow P (\|F\|) \in P [(1 ..^\|F\|)])$
26	25	notbid	$⊢ x = P (\|F\|) \to (\neg x \in P [(1 ..^\|F\|)] \leftrightarrow \neg P (\|F\|) \in P [(1 ..^\|F\|)])$
27	21 22 24 26	ralpr	$⊢ \forall x \in \{P (0), P (\|F\|)\} \neg x \in P [(1 ..^\|F\|)] \leftrightarrow (\neg P (0) \in P [(1 ..^\|F\|)] \land \neg P (\|F\|) \in P [(1 ..^\|F\|)])$
28		df-nel	$⊢ P (0) \notin P [(1 ..^\|F\|)] \leftrightarrow \neg P (0) \in P [(1 ..^\|F\|)]$
29	28	bicomi	$⊢ \neg P (0) \in P [(1 ..^\|F\|)] \leftrightarrow P (0) \notin P [(1 ..^\|F\|)]$
30	27 29	bianbi	$⊢ \forall x \in \{P (0), P (\|F\|)\} \neg x \in P [(1 ..^\|F\|)] \leftrightarrow (P (0) \notin P [(1 ..^\|F\|)] \land \neg P (\|F\|) \in P [(1 ..^\|F\|)])$
31	20 30	bitri	$⊢ \{P (0), P (\|F\|)\} \cap P [(1 ..^\|F\|)] = \emptyset \leftrightarrow (P (0) \notin P [(1 ..^\|F\|)] \land \neg P (\|F\|) \in P [(1 ..^\|F\|)])$
32	19 31	bitrdi	$⊢ F Trails (G) P \to (P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset \leftrightarrow (P (0) \notin P [(1 ..^\|F\|)] \land \neg P (\|F\|) \in P [(1 ..^\|F\|)]))$
33	32	anbi2d	$⊢ F Trails (G) P \to ((Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \leftrightarrow (Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land (P (0) \notin P [(1 ..^\|F\|)] \land \neg P (\|F\|) \in P [(1 ..^\|F\|)])))$
34		ancom	$⊢ (P (0) \notin P [(1 ..^\|F\|)] \land \neg P (\|F\|) \in P [(1 ..^\|F\|)]) \leftrightarrow (\neg P (\|F\|) \in P [(1 ..^\|F\|)] \land P (0) \notin P [(1 ..^\|F\|)])$
35	34	bianass	$⊢ (Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land (P (0) \notin P [(1 ..^\|F\|)] \land \neg P (\|F\|) \in P [(1 ..^\|F\|)])) \leftrightarrow ((Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land \neg P (\|F\|) \in P [(1 ..^\|F\|)]) \land P (0) \notin P [(1 ..^\|F\|)])$
36	35	a1i	$⊢ F Trails (G) P \to ((Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land (P (0) \notin P [(1 ..^\|F\|)] \land \neg P (\|F\|) \in P [(1 ..^\|F\|)])) \leftrightarrow ((Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land \neg P (\|F\|) \in P [(1 ..^\|F\|)]) \land P (0) \notin P [(1 ..^\|F\|)]))$
37		noel	$⊢ \neg P (\|F\|) \in \emptyset$
38	37	biantru	$⊢ Fun {({P ↾}_{\emptyset})}^{-1} \leftrightarrow (Fun {({P ↾}_{\emptyset})}^{-1} \land \neg P (\|F\|) \in \emptyset)$
39	38	bicomi	$⊢ (Fun {({P ↾}_{\emptyset})}^{-1} \land \neg P (\|F\|) \in \emptyset) \leftrightarrow Fun {({P ↾}_{\emptyset})}^{-1}$
40	39	a1i	$⊢ \|F\| = 0 \to ((Fun {({P ↾}_{\emptyset})}^{-1} \land \neg P (\|F\|) \in \emptyset) \leftrightarrow Fun {({P ↾}_{\emptyset})}^{-1})$
41		oveq2	$⊢ \|F\| = 0 \to (1 ..^\|F\|) = (1 ..^0)$
42		0le1	$⊢ 0 \leq 1$
43		1z	$⊢ 1 \in ℤ$
44		0z	$⊢ 0 \in ℤ$
45		fzon	$⊢ (1 \in ℤ \land 0 \in ℤ) \to (0 \leq 1 \leftrightarrow (1 ..^0) = \emptyset)$
46	43 44 45	mp2an	$⊢ 0 \leq 1 \leftrightarrow (1 ..^0) = \emptyset$
47	42 46	mpbi	$⊢ (1 ..^0) = \emptyset$
48	41 47	eqtrdi	$⊢ \|F\| = 0 \to (1 ..^\|F\|) = \emptyset$
49	48	reseq2d	$⊢ \|F\| = 0 \to {P ↾}_{(1 ..^\|F\|)} = {P ↾}_{\emptyset}$
50	49	cnveqd	$⊢ \|F\| = 0 \to {({P ↾}_{(1 ..^\|F\|)})}^{-1} = {({P ↾}_{\emptyset})}^{-1}$
51	50	funeqd	$⊢ \|F\| = 0 \to (Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \leftrightarrow Fun {({P ↾}_{\emptyset})}^{-1})$
52	48	imaeq2d	$⊢ \|F\| = 0 \to P [(1 ..^\|F\|)] = P [\emptyset]$
53		ima0	$⊢ P [\emptyset] = \emptyset$
54	52 53	eqtrdi	$⊢ \|F\| = 0 \to P [(1 ..^\|F\|)] = \emptyset$
55	54	eleq2d	$⊢ \|F\| = 0 \to (P (\|F\|) \in P [(1 ..^\|F\|)] \leftrightarrow P (\|F\|) \in \emptyset)$
56	55	notbid	$⊢ \|F\| = 0 \to (\neg P (\|F\|) \in P [(1 ..^\|F\|)] \leftrightarrow \neg P (\|F\|) \in \emptyset)$
57	51 56	anbi12d	$⊢ \|F\| = 0 \to ((Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land \neg P (\|F\|) \in P [(1 ..^\|F\|)]) \leftrightarrow (Fun {({P ↾}_{\emptyset})}^{-1} \land \neg P (\|F\|) \in \emptyset))$
58		oveq2	$⊢ \|F\| = 0 \to (1 \dots \|F\|) = (1 \dots 0)$
59		fz10	$⊢ (1 \dots 0) = \emptyset$
60	58 59	eqtrdi	$⊢ \|F\| = 0 \to (1 \dots \|F\|) = \emptyset$
61	60	reseq2d	$⊢ \|F\| = 0 \to {P ↾}_{(1 \dots \|F\|)} = {P ↾}_{\emptyset}$
62	61	cnveqd	$⊢ \|F\| = 0 \to {({P ↾}_{(1 \dots \|F\|)})}^{-1} = {({P ↾}_{\emptyset})}^{-1}$
63	62	funeqd	$⊢ \|F\| = 0 \to (Fun {({P ↾}_{(1 \dots \|F\|)})}^{-1} \leftrightarrow Fun {({P ↾}_{\emptyset})}^{-1})$
64	40 57 63	3bitr4d	$⊢ \|F\| = 0 \to ((Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land \neg P (\|F\|) \in P [(1 ..^\|F\|)]) \leftrightarrow Fun {({P ↾}_{(1 \dots \|F\|)})}^{-1})$
65	64	a1d	$⊢ \|F\| = 0 \to (F Trails (G) P \to ((Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land \neg P (\|F\|) \in P [(1 ..^\|F\|)]) \leftrightarrow Fun {({P ↾}_{(1 \dots \|F\|)})}^{-1}))$
66		df-nel	$⊢ P (\|F\|) \notin P [(1 ..^\|F\|)] \leftrightarrow \neg P (\|F\|) \in P [(1 ..^\|F\|)]$
67	66	bicomi	$⊢ \neg P (\|F\|) \in P [(1 ..^\|F\|)] \leftrightarrow P (\|F\|) \notin P [(1 ..^\|F\|)]$
68	67	anbi2i	$⊢ (Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land \neg P (\|F\|) \in P [(1 ..^\|F\|)]) \leftrightarrow (Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P (\|F\|) \notin P [(1 ..^\|F\|)])$
69		trliswlk	$⊢ F Trails (G) P \to F Walks (G) P$
70	3 10	sylib	$⊢ F Walks (G) P \to \|F\| \in (0 \dots \|F\|)$
71		fzonel	$⊢ \neg \|F\| \in (1 ..^\|F\|)$
72	71	a1i	$⊢ F Walks (G) P \to \neg \|F\| \in (1 ..^\|F\|)$
73	70 72	eldifd	$⊢ F Walks (G) P \to \|F\| \in ((0 \dots \|F\|) ∖ (1 ..^\|F\|))$
74		1eluzge0	$⊢ 1 \in ℤ_{\geq 0}$
75		fzoss1	$⊢ 1 \in ℤ_{\geq 0} \to (1 ..^\|F\|) \subseteq (0 ..^\|F\|)$
76	74 75	mp1i	$⊢ F Walks (G) P \to (1 ..^\|F\|) \subseteq (0 ..^\|F\|)$
77		fzossfz	$⊢ (0 ..^\|F\|) \subseteq (0 \dots \|F\|)$
78	76 77	sstrdi	$⊢ F Walks (G) P \to (1 ..^\|F\|) \subseteq (0 \dots \|F\|)$
79	5 73 78	3jca	$⊢ F Walks (G) P \to (P : (0 \dots \|F\|) ⟶ Vtx (G) \land \|F\| \in ((0 \dots \|F\|) ∖ (1 ..^\|F\|)) \land (1 ..^\|F\|) \subseteq (0 \dots \|F\|))$
80		resf1ext2b	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land \|F\| \in ((0 \dots \|F\|) ∖ (1 ..^\|F\|)) \land (1 ..^\|F\|) \subseteq (0 \dots \|F\|)) \to ((Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P (\|F\|) \notin P [(1 ..^\|F\|)]) \leftrightarrow Fun {({P ↾}_{((1 ..^\|F\|) \cup \{\|F\|\})})}^{-1})$
81	69 79 80	3syl	$⊢ F Trails (G) P \to ((Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P (\|F\|) \notin P [(1 ..^\|F\|)]) \leftrightarrow Fun {({P ↾}_{((1 ..^\|F\|) \cup \{\|F\|\})})}^{-1})$
82	68 81	bitrid	$⊢ F Trails (G) P \to ((Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land \neg P (\|F\|) \in P [(1 ..^\|F\|)]) \leftrightarrow Fun {({P ↾}_{((1 ..^\|F\|) \cup \{\|F\|\})})}^{-1})$
83	82	adantl	$⊢ (\|F\| \neq 0 \land F Trails (G) P) \to ((Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land \neg P (\|F\|) \in P [(1 ..^\|F\|)]) \leftrightarrow Fun {({P ↾}_{((1 ..^\|F\|) \cup \{\|F\|\})})}^{-1})$
84		elnnne0	$⊢ \|F\| \in ℕ \leftrightarrow (\|F\| \in ℕ_{0} \land \|F\| \neq 0)$
85		elnnuz	$⊢ \|F\| \in ℕ \leftrightarrow \|F\| \in ℤ_{\geq 1}$
86	84 85	sylbb1	$⊢ (\|F\| \in ℕ_{0} \land \|F\| \neq 0) \to \|F\| \in ℤ_{\geq 1}$
87	86	ex	$⊢ \|F\| \in ℕ_{0} \to (\|F\| \neq 0 \to \|F\| \in ℤ_{\geq 1})$
88	69 3 87	3syl	$⊢ F Trails (G) P \to (\|F\| \neq 0 \to \|F\| \in ℤ_{\geq 1})$
89	88	impcom	$⊢ (\|F\| \neq 0 \land F Trails (G) P) \to \|F\| \in ℤ_{\geq 1}$
90		fzisfzounsn	$⊢ \|F\| \in ℤ_{\geq 1} \to (1 \dots \|F\|) = (1 ..^\|F\|) \cup \{\|F\|\}$
91	89 90	syl	$⊢ (\|F\| \neq 0 \land F Trails (G) P) \to (1 \dots \|F\|) = (1 ..^\|F\|) \cup \{\|F\|\}$
92	91	eqcomd	$⊢ (\|F\| \neq 0 \land F Trails (G) P) \to (1 ..^\|F\|) \cup \{\|F\|\} = (1 \dots \|F\|)$
93	92	reseq2d	$⊢ (\|F\| \neq 0 \land F Trails (G) P) \to {P ↾}_{((1 ..^\|F\|) \cup \{\|F\|\})} = {P ↾}_{(1 \dots \|F\|)}$
94	93	cnveqd	$⊢ (\|F\| \neq 0 \land F Trails (G) P) \to {({P ↾}_{((1 ..^\|F\|) \cup \{\|F\|\})})}^{-1} = {({P ↾}_{(1 \dots \|F\|)})}^{-1}$
95	94	funeqd	$⊢ (\|F\| \neq 0 \land F Trails (G) P) \to (Fun {({P ↾}_{((1 ..^\|F\|) \cup \{\|F\|\})})}^{-1} \leftrightarrow Fun {({P ↾}_{(1 \dots \|F\|)})}^{-1})$
96	83 95	bitrd	$⊢ (\|F\| \neq 0 \land F Trails (G) P) \to ((Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land \neg P (\|F\|) \in P [(1 ..^\|F\|)]) \leftrightarrow Fun {({P ↾}_{(1 \dots \|F\|)})}^{-1})$
97	96	ex	$⊢ \|F\| \neq 0 \to (F Trails (G) P \to ((Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land \neg P (\|F\|) \in P [(1 ..^\|F\|)]) \leftrightarrow Fun {({P ↾}_{(1 \dots \|F\|)})}^{-1}))$
98	65 97	pm2.61ine	$⊢ F Trails (G) P \to ((Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land \neg P (\|F\|) \in P [(1 ..^\|F\|)]) \leftrightarrow Fun {({P ↾}_{(1 \dots \|F\|)})}^{-1})$
99	98	anbi1d	$⊢ F Trails (G) P \to (((Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land \neg P (\|F\|) \in P [(1 ..^\|F\|)]) \land P (0) \notin P [(1 ..^\|F\|)]) \leftrightarrow (Fun {({P ↾}_{(1 \dots \|F\|)})}^{-1} \land P (0) \notin P [(1 ..^\|F\|)]))$
100	33 36 99	3bitrd	$⊢ F Trails (G) P \to ((Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \leftrightarrow (Fun {({P ↾}_{(1 \dots \|F\|)})}^{-1} \land P (0) \notin P [(1 ..^\|F\|)]))$
101	100	pm5.32i	$⊢ (F Trails (G) P \land (Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset)) \leftrightarrow (F Trails (G) P \land (Fun {({P ↾}_{(1 \dots \|F\|)})}^{-1} \land P (0) \notin P [(1 ..^\|F\|)]))$
102		3anass	$⊢ (F Trails (G) P \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \leftrightarrow (F Trails (G) P \land (Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset))$
103		3anass	$⊢ (F Trails (G) P \land Fun {({P ↾}_{(1 \dots \|F\|)})}^{-1} \land P (0) \notin P [(1 ..^\|F\|)]) \leftrightarrow (F Trails (G) P \land (Fun {({P ↾}_{(1 \dots \|F\|)})}^{-1} \land P (0) \notin P [(1 ..^\|F\|)]))$
104	101 102 103	3bitr4i	$⊢ (F Trails (G) P \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \leftrightarrow (F Trails (G) P \land Fun {({P ↾}_{(1 \dots \|F\|)})}^{-1} \land P (0) \notin P [(1 ..^\|F\|)])$
105	1 104	bitri	$⊢ F Paths (G) P \leftrightarrow (F Trails (G) P \land Fun {({P ↾}_{(1 \dots \|F\|)})}^{-1} \land P (0) \notin P [(1 ..^\|F\|)])$

Metamath Proof Explorer

Theorem dfpth2

Proof