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