pthhashvtx

Description: A graph containing a path has at least as many vertices as there are edges in the path. (Contributed by BTernaryTau, 5-Oct-2023)

		Ref	Expression
	Hypothesis	pthhashvtx.1	$⊢ V = Vtx (G)$
	Assertion	pthhashvtx	$⊢ F Paths (G) P \to \|F\| \leq \|V\|$

Proof

Step	Hyp	Ref	Expression
1		pthhashvtx.1	$⊢ V = Vtx (G)$
2		hashfz0	$⊢ \|F\| - 1 \in ℕ_{0} \to \|(0 \dots \|F\| - 1)\| = \|F\| - 1 + 1$
3		pthiswlk	$⊢ F Paths (G) P \to F Walks (G) P$
4		wlkcl	$⊢ F Walks (G) P \to \|F\| \in ℕ_{0}$
5	3 4	syl	$⊢ F Paths (G) P \to \|F\| \in ℕ_{0}$
6		nn0cn	$⊢ \|F\| \in ℕ_{0} \to \|F\| \in ℂ$
7		npcan1	$⊢ \|F\| \in ℂ \to \|F\| - 1 + 1 = \|F\|$
8	5 6 7	3syl	$⊢ F Paths (G) P \to \|F\| - 1 + 1 = \|F\|$
9	2 8	sylan9eqr	$⊢ (F Paths (G) P \land \|F\| - 1 \in ℕ_{0}) \to \|(0 \dots \|F\| - 1)\| = \|F\|$
10	1	wlkp	$⊢ F Walks (G) P \to P : (0 \dots \|F\|) ⟶ V$
11	3 10	syl	$⊢ F Paths (G) P \to P : (0 \dots \|F\|) ⟶ V$
12	11	ffnd	$⊢ F Paths (G) P \to P Fn (0 \dots \|F\|)$
13		fzfi	$⊢ (0 \dots \|F\| - 1) \in Fin$
14		resfnfinfin	$⊢ (P Fn (0 \dots \|F\|) \land (0 \dots \|F\| - 1) \in Fin) \to {P ↾}_{(0 \dots \|F\| - 1)} \in Fin$
15	12 13 14	sylancl	$⊢ F Paths (G) P \to {P ↾}_{(0 \dots \|F\| - 1)} \in Fin$
16		simpr	$⊢ (F Paths (G) P \land \|F\| - 1 \in ℕ_{0}) \to \|F\| - 1 \in ℕ_{0}$
17		fzssp1	$⊢ (0 \dots \|F\| - 1) \subseteq (0 \dots \|F\| - 1 + 1)$
18	8	oveq2d	$⊢ F Paths (G) P \to (0 \dots \|F\| - 1 + 1) = (0 \dots \|F\|)$
19	17 18	sseqtrid	$⊢ F Paths (G) P \to (0 \dots \|F\| - 1) \subseteq (0 \dots \|F\|)$
20	11 19	fssresd	$⊢ F Paths (G) P \to ({P ↾}_{(0 \dots \|F\| - 1)}) : (0 \dots \|F\| - 1) ⟶ V$
21	20	adantr	$⊢ (F Paths (G) P \land \|F\| - 1 \in ℕ_{0}) \to ({P ↾}_{(0 \dots \|F\| - 1)}) : (0 \dots \|F\| - 1) ⟶ V$
22		fz1ssfz0	$⊢ (1 \dots \|F\| - 1) \subseteq (0 \dots \|F\| - 1)$
23	22	a1i	$⊢ F Paths (G) P \to (1 \dots \|F\| - 1) \subseteq (0 \dots \|F\| - 1)$
24	20 23	fssresd	$⊢ F Paths (G) P \to ({({P ↾}_{(0 \dots \|F\| - 1)}) ↾}_{(1 \dots \|F\| - 1)}) : (1 \dots \|F\| - 1) ⟶ V$
25		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)$
26	25	simp2bi	$⊢ F Paths (G) P \to Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1}$
27		nn0z	$⊢ \|F\| \in ℕ_{0} \to \|F\| \in ℤ$
28		fzoval	$⊢ \|F\| \in ℤ \to (1 ..^\|F\|) = (1 \dots \|F\| - 1)$
29	27 28	syl	$⊢ \|F\| \in ℕ_{0} \to (1 ..^\|F\|) = (1 \dots \|F\| - 1)$
30	5 29	syl	$⊢ F Paths (G) P \to (1 ..^\|F\|) = (1 \dots \|F\| - 1)$
31	30	reseq2d	$⊢ F Paths (G) P \to {P ↾}_{(1 ..^\|F\|)} = {P ↾}_{(1 \dots \|F\| - 1)}$
32		resabs1	$⊢ (1 \dots \|F\| - 1) \subseteq (0 \dots \|F\| - 1) \to {({P ↾}_{(0 \dots \|F\| - 1)}) ↾}_{(1 \dots \|F\| - 1)} = {P ↾}_{(1 \dots \|F\| - 1)}$
33	22 32	ax-mp	$⊢ {({P ↾}_{(0 \dots \|F\| - 1)}) ↾}_{(1 \dots \|F\| - 1)} = {P ↾}_{(1 \dots \|F\| - 1)}$
34	31 33	eqtr4di	$⊢ F Paths (G) P \to {P ↾}_{(1 ..^\|F\|)} = {({P ↾}_{(0 \dots \|F\| - 1)}) ↾}_{(1 \dots \|F\| - 1)}$
35	34	cnveqd	$⊢ F Paths (G) P \to {({P ↾}_{(1 ..^\|F\|)})}^{-1} = {({({P ↾}_{(0 \dots \|F\| - 1)}) ↾}_{(1 \dots \|F\| - 1)})}^{-1}$
36	35	funeqd	$⊢ F Paths (G) P \to (Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \leftrightarrow Fun {({({P ↾}_{(0 \dots \|F\| - 1)}) ↾}_{(1 \dots \|F\| - 1)})}^{-1})$
37	26 36	mpbid	$⊢ F Paths (G) P \to Fun {({({P ↾}_{(0 \dots \|F\| - 1)}) ↾}_{(1 \dots \|F\| - 1)})}^{-1}$
38		df-f1	$⊢ ({({P ↾}_{(0 \dots \|F\| - 1)}) ↾}_{(1 \dots \|F\| - 1)}) : (1 \dots \|F\| - 1) \underset{1-1}{⟶} V \leftrightarrow (({({P ↾}_{(0 \dots \|F\| - 1)}) ↾}_{(1 \dots \|F\| - 1)}) : (1 \dots \|F\| - 1) ⟶ V \land Fun {({({P ↾}_{(0 \dots \|F\| - 1)}) ↾}_{(1 \dots \|F\| - 1)})}^{-1})$
39	24 37 38	sylanbrc	$⊢ F Paths (G) P \to ({({P ↾}_{(0 \dots \|F\| - 1)}) ↾}_{(1 \dots \|F\| - 1)}) : (1 \dots \|F\| - 1) \underset{1-1}{⟶} V$
40	39	adantr	$⊢ (F Paths (G) P \land \|F\| - 1 \in ℕ_{0}) \to ({({P ↾}_{(0 \dots \|F\| - 1)}) ↾}_{(1 \dots \|F\| - 1)}) : (1 \dots \|F\| - 1) \underset{1-1}{⟶} V$
41	38	simprbi	$⊢ ({({P ↾}_{(0 \dots \|F\| - 1)}) ↾}_{(1 \dots \|F\| - 1)}) : (1 \dots \|F\| - 1) \underset{1-1}{⟶} V \to Fun {({({P ↾}_{(0 \dots \|F\| - 1)}) ↾}_{(1 \dots \|F\| - 1)})}^{-1}$
42	40 41	syl	$⊢ (F Paths (G) P \land \|F\| - 1 \in ℕ_{0}) \to Fun {({({P ↾}_{(0 \dots \|F\| - 1)}) ↾}_{(1 \dots \|F\| - 1)})}^{-1}$
43		snsspr1	$⊢ \{0\} \subseteq \{0, \|F\|\}$
44		imass2	$⊢ \{0\} \subseteq \{0, \|F\|\} \to P [\{0\}] \subseteq P [\{0, \|F\|\}]$
45	43 44	ax-mp	$⊢ P [\{0\}] \subseteq P [\{0, \|F\|\}]$
46		0elfz	$⊢ \|F\| - 1 \in ℕ_{0} \to 0 \in (0 \dots \|F\| - 1)$
47	46	snssd	$⊢ \|F\| - 1 \in ℕ_{0} \to \{0\} \subseteq (0 \dots \|F\| - 1)$
48		resima2	$⊢ \{0\} \subseteq (0 \dots \|F\| - 1) \to ({P ↾}_{(0 \dots \|F\| - 1)}) [\{0\}] = P [\{0\}]$
49		sseq1	$⊢ ({P ↾}_{(0 \dots \|F\| - 1)}) [\{0\}] = P [\{0\}] \to (({P ↾}_{(0 \dots \|F\| - 1)}) [\{0\}] \subseteq P [\{0, \|F\|\}] \leftrightarrow P [\{0\}] \subseteq P [\{0, \|F\|\}])$
50	47 48 49	3syl	$⊢ \|F\| - 1 \in ℕ_{0} \to (({P ↾}_{(0 \dots \|F\| - 1)}) [\{0\}] \subseteq P [\{0, \|F\|\}] \leftrightarrow P [\{0\}] \subseteq P [\{0, \|F\|\}])$
51	45 50	mpbiri	$⊢ \|F\| - 1 \in ℕ_{0} \to ({P ↾}_{(0 \dots \|F\| - 1)}) [\{0\}] \subseteq P [\{0, \|F\|\}]$
52		resima2	$⊢ (1 \dots \|F\| - 1) \subseteq (0 \dots \|F\| - 1) \to ({P ↾}_{(0 \dots \|F\| - 1)}) [(1 \dots \|F\| - 1)] = P [(1 \dots \|F\| - 1)]$
53	22 52	ax-mp	$⊢ ({P ↾}_{(0 \dots \|F\| - 1)}) [(1 \dots \|F\| - 1)] = P [(1 \dots \|F\| - 1)]$
54	30	imaeq2d	$⊢ F Paths (G) P \to P [(1 ..^\|F\|)] = P [(1 \dots \|F\| - 1)]$
55	53 54	eqtr4id	$⊢ F Paths (G) P \to ({P ↾}_{(0 \dots \|F\| - 1)}) [(1 \dots \|F\| - 1)] = P [(1 ..^\|F\|)]$
56	55	ineq2d	$⊢ F Paths (G) P \to P [\{0, \|F\|\}] \cap ({P ↾}_{(0 \dots \|F\| - 1)}) [(1 \dots \|F\| - 1)] = P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)]$
57	25	simp3bi	$⊢ F Paths (G) P \to P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset$
58	56 57	eqtrd	$⊢ F Paths (G) P \to P [\{0, \|F\|\}] \cap ({P ↾}_{(0 \dots \|F\| - 1)}) [(1 \dots \|F\| - 1)] = \emptyset$
59		ssdisj	$⊢ (({P ↾}_{(0 \dots \|F\| - 1)}) [\{0\}] \subseteq P [\{0, \|F\|\}] \land P [\{0, \|F\|\}] \cap ({P ↾}_{(0 \dots \|F\| - 1)}) [(1 \dots \|F\| - 1)] = \emptyset) \to ({P ↾}_{(0 \dots \|F\| - 1)}) [\{0\}] \cap ({P ↾}_{(0 \dots \|F\| - 1)}) [(1 \dots \|F\| - 1)] = \emptyset$
60	51 58 59	syl2anr	$⊢ (F Paths (G) P \land \|F\| - 1 \in ℕ_{0}) \to ({P ↾}_{(0 \dots \|F\| - 1)}) [\{0\}] \cap ({P ↾}_{(0 \dots \|F\| - 1)}) [(1 \dots \|F\| - 1)] = \emptyset$
61	16 21 42 60	f1resfz0f1d	$⊢ (F Paths (G) P \land \|F\| - 1 \in ℕ_{0}) \to ({P ↾}_{(0 \dots \|F\| - 1)}) : (0 \dots \|F\| - 1) \underset{1-1}{⟶} V$
62	1	fvexi	$⊢ V \in V$
63		hashf1dmcdm	$⊢ ({P ↾}_{(0 \dots \|F\| - 1)} \in Fin \land V \in V \land ({P ↾}_{(0 \dots \|F\| - 1)}) : (0 \dots \|F\| - 1) \underset{1-1}{⟶} V) \to \|(0 \dots \|F\| - 1)\| \leq \|V\|$
64	62 63	mp3an2	$⊢ ({P ↾}_{(0 \dots \|F\| - 1)} \in Fin \land ({P ↾}_{(0 \dots \|F\| - 1)}) : (0 \dots \|F\| - 1) \underset{1-1}{⟶} V) \to \|(0 \dots \|F\| - 1)\| \leq \|V\|$
65	15 61 64	syl2an2r	$⊢ (F Paths (G) P \land \|F\| - 1 \in ℕ_{0}) \to \|(0 \dots \|F\| - 1)\| \leq \|V\|$
66	9 65	eqbrtrrd	$⊢ (F Paths (G) P \land \|F\| - 1 \in ℕ_{0}) \to \|F\| \leq \|V\|$
67		0nn0m1nnn0	$⊢ \|F\| = 0 \leftrightarrow (\|F\| \in ℕ_{0} \land \neg \|F\| - 1 \in ℕ_{0})$
68	67	biimpri	$⊢ (\|F\| \in ℕ_{0} \land \neg \|F\| - 1 \in ℕ_{0}) \to \|F\| = 0$
69	5 68	sylan	$⊢ (F Paths (G) P \land \neg \|F\| - 1 \in ℕ_{0}) \to \|F\| = 0$
70		hashge0	$⊢ V \in V \to 0 \leq \|V\|$
71	62 70	ax-mp	$⊢ 0 \leq \|V\|$
72	69 71	eqbrtrdi	$⊢ (F Paths (G) P \land \neg \|F\| - 1 \in ℕ_{0}) \to \|F\| \leq \|V\|$
73	66 72	pm2.61dan	$⊢ F Paths (G) P \to \|F\| \leq \|V\|$

Metamath Proof Explorer

Theorem pthhashvtx

Proof