pthhashvtx - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > pthhashvtx		Structured version Visualization version GIF version

Theorem pthhashvtx 30348

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.)

**Hypothesis**
Ref	Expression
pthhashvtx.1	⊢ 𝑉 = (Vtx‘𝐺)

**Assertion**
Ref	Expression
pthhashvtx	⊢ (𝐹(Paths‘𝐺)𝑃 → (♯‘𝐹) ≤ (♯‘𝑉))

**Proof of Theorem pthhashvtx**
Step	Hyp	Ref	Expression
1		hashfz0 14607	. . . 4 ⊢ (((♯‘𝐹) − 1) ∈ ℕ₀ → (♯‘(0...((♯‘𝐹) − 1))) = (((♯‘𝐹) − 1) + 1))
2		pthiswlk 30343	. . . . . 6 ⊢ (𝐹(Paths‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
3		wlkcl 30229	. . . . . 6 ⊢ (𝐹(Walks‘𝐺)𝑃 → (♯‘𝐹) ∈ ℕ₀)
4	2, 3	syl 18	. . . . 5 ⊢ (𝐹(Paths‘𝐺)𝑃 → (♯‘𝐹) ∈ ℕ₀)
5		nn0cn 12646	. . . . 5 ⊢ ((♯‘𝐹) ∈ ℕ₀ → (♯‘𝐹) ∈ ℂ)
6		npcan1 11771	. . . . 5 ⊢ ((♯‘𝐹) ∈ ℂ → (((♯‘𝐹) − 1) + 1) = (♯‘𝐹))
7	4, 5, 6	3syl 19	. . . 4 ⊢ (𝐹(Paths‘𝐺)𝑃 → (((♯‘𝐹) − 1) + 1) = (♯‘𝐹))
8	1, 7	sylan9eqr 2820	. . 3 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ ((♯‘𝐹) − 1) ∈ ℕ₀) → (♯‘(0...((♯‘𝐹) − 1))) = (♯‘𝐹))
9		pthhashvtx.1	. . . . . . . 8 ⊢ 𝑉 = (Vtx‘𝐺)
10	9	wlkp 30230	. . . . . . 7 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉)
11	2, 10	syl 18	. . . . . 6 ⊢ (𝐹(Paths‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉)
12	11	ffnd 6735	. . . . 5 ⊢ (𝐹(Paths‘𝐺)𝑃 → 𝑃 Fn (0...(♯‘𝐹)))
13		fzfi 14145	. . . . 5 ⊢ (0...((♯‘𝐹) − 1)) ∈ Fin
14		resfnfinfin 9357	. . . . 5 ⊢ ((𝑃 Fn (0...(♯‘𝐹)) ∧ (0...((♯‘𝐹) − 1)) ∈ Fin) → (𝑃 ↾ (0...((♯‘𝐹) − 1))) ∈ Fin)
15	12, 13, 14	sylancl 598	. . . 4 ⊢ (𝐹(Paths‘𝐺)𝑃 → (𝑃 ↾ (0...((♯‘𝐹) − 1))) ∈ Fin)
16		simpr 490	. . . . 5 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ ((♯‘𝐹) − 1) ∈ ℕ₀) → ((♯‘𝐹) − 1) ∈ ℕ₀)
17		fzssp1 13731	. . . . . . . 8 ⊢ (0...((♯‘𝐹) − 1)) ⊆ (0...(((♯‘𝐹) − 1) + 1))
18	7	oveq2d 7462	. . . . . . . 8 ⊢ (𝐹(Paths‘𝐺)𝑃 → (0...(((♯‘𝐹) − 1) + 1)) = (0...(♯‘𝐹)))
19	17, 18	sseqtrid 3955	. . . . . . 7 ⊢ (𝐹(Paths‘𝐺)𝑃 → (0...((♯‘𝐹) − 1)) ⊆ (0...(♯‘𝐹)))
20	11, 19	fssresd 6774	. . . . . 6 ⊢ (𝐹(Paths‘𝐺)𝑃 → (𝑃 ↾ (0...((♯‘𝐹) − 1))):(0...((♯‘𝐹) − 1))⟶𝑉)
21	20	adantr 486	. . . . 5 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ ((♯‘𝐹) − 1) ∈ ℕ₀) → (𝑃 ↾ (0...((♯‘𝐹) − 1))):(0...((♯‘𝐹) − 1))⟶𝑉)
22		fz1ssfz0 13787	. . . . . . . . . 10 ⊢ (1...((♯‘𝐹) − 1)) ⊆ (0...((♯‘𝐹) − 1))
23	22	a1i 11	. . . . . . . . 9 ⊢ (𝐹(Paths‘𝐺)𝑃 → (1...((♯‘𝐹) − 1)) ⊆ (0...((♯‘𝐹) − 1)))
24	20, 23	fssresd 6774	. . . . . . . 8 ⊢ (𝐹(Paths‘𝐺)𝑃 → ((𝑃 ↾ (0...((♯‘𝐹) − 1))) ↾ (1...((♯‘𝐹) − 1))):(1...((♯‘𝐹) − 1))⟶𝑉)
25		ispth 30339	. . . . . . . . . 10 ⊢ (𝐹(Paths‘𝐺)𝑃 ↔ (𝐹(Trails‘𝐺)𝑃 ∧ Fun ^◡(𝑃 ↾ (1..^(♯‘𝐹))) ∧ ((𝑃 “ {0, (♯‘𝐹)}) ∩ (𝑃 “ (1..^(♯‘𝐹)))) = ∅))
26	25	simp2bi 1164	. . . . . . . . 9 ⊢ (𝐹(Paths‘𝐺)𝑃 → Fun ^◡(𝑃 ↾ (1..^(♯‘𝐹))))
27		nn0z 12747	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝐹) ∈ ℕ₀ → (♯‘𝐹) ∈ ℤ)
28		fzoval 13824	. . . . . . . . . . . . . . 15 ⊢ ((♯‘𝐹) ∈ ℤ → (1..^(♯‘𝐹)) = (1...((♯‘𝐹) − 1)))
29	27, 28	syl 18	. . . . . . . . . . . . . 14 ⊢ ((♯‘𝐹) ∈ ℕ₀ → (1..^(♯‘𝐹)) = (1...((♯‘𝐹) − 1)))
30	4, 29	syl 18	. . . . . . . . . . . . 13 ⊢ (𝐹(Paths‘𝐺)𝑃 → (1..^(♯‘𝐹)) = (1...((♯‘𝐹) − 1)))
31	30	reseq2d 5982	. . . . . . . . . . . 12 ⊢ (𝐹(Paths‘𝐺)𝑃 → (𝑃 ↾ (1..^(♯‘𝐹))) = (𝑃 ↾ (1...((♯‘𝐹) − 1))))
32		resabs1 6010	. . . . . . . . . . . . 13 ⊢ ((1...((♯‘𝐹) − 1)) ⊆ (0...((♯‘𝐹) − 1)) → ((𝑃 ↾ (0...((♯‘𝐹) − 1))) ↾ (1...((♯‘𝐹) − 1))) = (𝑃 ↾ (1...((♯‘𝐹) − 1))))
33	22, 32	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((𝑃 ↾ (0...((♯‘𝐹) − 1))) ↾ (1...((♯‘𝐹) − 1))) = (𝑃 ↾ (1...((♯‘𝐹) − 1)))
34	31, 33	eqtr4di 2816	. . . . . . . . . . 11 ⊢ (𝐹(Paths‘𝐺)𝑃 → (𝑃 ↾ (1..^(♯‘𝐹))) = ((𝑃 ↾ (0...((♯‘𝐹) − 1))) ↾ (1...((♯‘𝐹) − 1))))
35	34	cnveqd 5861	. . . . . . . . . 10 ⊢ (𝐹(Paths‘𝐺)𝑃 → ^◡(𝑃 ↾ (1..^(♯‘𝐹))) = ^◡((𝑃 ↾ (0...((♯‘𝐹) − 1))) ↾ (1...((♯‘𝐹) − 1))))
36	35	funeqd 6584	. . . . . . . . 9 ⊢ (𝐹(Paths‘𝐺)𝑃 → (Fun ^◡(𝑃 ↾ (1..^(♯‘𝐹))) ↔ Fun ^◡((𝑃 ↾ (0...((♯‘𝐹) − 1))) ↾ (1...((♯‘𝐹) − 1)))))
37	26, 36	mpbid 235	. . . . . . . 8 ⊢ (𝐹(Paths‘𝐺)𝑃 → Fun ^◡((𝑃 ↾ (0...((♯‘𝐹) − 1))) ↾ (1...((♯‘𝐹) − 1))))
38		df-f1 6566	. . . . . . . 8 ⊢ (((𝑃 ↾ (0...((♯‘𝐹) − 1))) ↾ (1...((♯‘𝐹) − 1))):(1...((♯‘𝐹) − 1))⟶1-1𝑉 ↔ (((𝑃 ↾ (0...((♯‘𝐹) − 1))) ↾ (1...((♯‘𝐹) − 1))):(1...((♯‘𝐹) − 1))⟶𝑉 ∧ Fun ^◡((𝑃 ↾ (0...((♯‘𝐹) − 1))) ↾ (1...((♯‘𝐹) − 1)))))
39	24, 37, 38	sylanbrc 595	. . . . . . 7 ⊢ (𝐹(Paths‘𝐺)𝑃 → ((𝑃 ↾ (0...((♯‘𝐹) − 1))) ↾ (1...((♯‘𝐹) − 1))):(1...((♯‘𝐹) − 1))⟶1-1𝑉)
40	39	adantr 486	. . . . . 6 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ ((♯‘𝐹) − 1) ∈ ℕ₀) → ((𝑃 ↾ (0...((♯‘𝐹) − 1))) ↾ (1...((♯‘𝐹) − 1))):(1...((♯‘𝐹) − 1))⟶1-1𝑉)
41	38	simprbi 503	. . . . . 6 ⊢ (((𝑃 ↾ (0...((♯‘𝐹) − 1))) ↾ (1...((♯‘𝐹) − 1))):(1...((♯‘𝐹) − 1))⟶1-1𝑉 → Fun ^◡((𝑃 ↾ (0...((♯‘𝐹) − 1))) ↾ (1...((♯‘𝐹) − 1))))
42	40, 41	syl 18	. . . . 5 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ ((♯‘𝐹) − 1) ∈ ℕ₀) → Fun ^◡((𝑃 ↾ (0...((♯‘𝐹) − 1))) ↾ (1...((♯‘𝐹) − 1))))
43		snsspr1 4773	. . . . . . . 8 ⊢ {0} ⊆ {0, (♯‘𝐹)}
44		imass2 6068	. . . . . . . 8 ⊢ ({0} ⊆ {0, (♯‘𝐹)} → (𝑃 “ {0}) ⊆ (𝑃 “ {0, (♯‘𝐹)}))
45	43, 44	ax-mp 5	. . . . . . 7 ⊢ (𝑃 “ {0}) ⊆ (𝑃 “ {0, (♯‘𝐹)})
46		0elfz 13788	. . . . . . . . 9 ⊢ (((♯‘𝐹) − 1) ∈ ℕ₀ → 0 ∈ (0...((♯‘𝐹) − 1)))
47	46	snssd 4747	. . . . . . . 8 ⊢ (((♯‘𝐹) − 1) ∈ ℕ₀ → {0} ⊆ (0...((♯‘𝐹) − 1)))
48		resima2 6070	. . . . . . . 8 ⊢ ({0} ⊆ (0...((♯‘𝐹) − 1)) → ((𝑃 ↾ (0...((♯‘𝐹) − 1))) “ {0}) = (𝑃 “ {0}))
49		sseq1 3938	. . . . . . . 8 ⊢ (((𝑃 ↾ (0...((♯‘𝐹) − 1))) “ {0}) = (𝑃 “ {0}) → (((𝑃 ↾ (0...((♯‘𝐹) − 1))) “ {0}) ⊆ (𝑃 “ {0, (♯‘𝐹)}) ↔ (𝑃 “ {0}) ⊆ (𝑃 “ {0, (♯‘𝐹)})))
50	47, 48, 49	3syl 19	. . . . . . 7 ⊢ (((♯‘𝐹) − 1) ∈ ℕ₀ → (((𝑃 ↾ (0...((♯‘𝐹) − 1))) “ {0}) ⊆ (𝑃 “ {0, (♯‘𝐹)}) ↔ (𝑃 “ {0}) ⊆ (𝑃 “ {0, (♯‘𝐹)})))
51	45, 50	mpbiri 261	. . . . . 6 ⊢ (((♯‘𝐹) − 1) ∈ ℕ₀ → ((𝑃 ↾ (0...((♯‘𝐹) − 1))) “ {0}) ⊆ (𝑃 “ {0, (♯‘𝐹)}))
52		resima2 6070	. . . . . . . . . 10 ⊢ ((1...((♯‘𝐹) − 1)) ⊆ (0...((♯‘𝐹) − 1)) → ((𝑃 ↾ (0...((♯‘𝐹) − 1))) “ (1...((♯‘𝐹) − 1))) = (𝑃 “ (1...((♯‘𝐹) − 1))))
53	22, 52	ax-mp 5	. . . . . . . . 9 ⊢ ((𝑃 ↾ (0...((♯‘𝐹) − 1))) “ (1...((♯‘𝐹) − 1))) = (𝑃 “ (1...((♯‘𝐹) − 1)))
54	30	imaeq2d 6065	. . . . . . . . 9 ⊢ (𝐹(Paths‘𝐺)𝑃 → (𝑃 “ (1..^(♯‘𝐹))) = (𝑃 “ (1...((♯‘𝐹) − 1))))
55	53, 54	eqtr4id 2817	. . . . . . . 8 ⊢ (𝐹(Paths‘𝐺)𝑃 → ((𝑃 ↾ (0...((♯‘𝐹) − 1))) “ (1...((♯‘𝐹) − 1))) = (𝑃 “ (1..^(♯‘𝐹))))
56	55	ineq2d 4120	. . . . . . 7 ⊢ (𝐹(Paths‘𝐺)𝑃 → ((𝑃 “ {0, (♯‘𝐹)}) ∩ ((𝑃 ↾ (0...((♯‘𝐹) − 1))) “ (1...((♯‘𝐹) − 1)))) = ((𝑃 “ {0, (♯‘𝐹)}) ∩ (𝑃 “ (1..^(♯‘𝐹)))))
57	25	simp3bi 1165	. . . . . . 7 ⊢ (𝐹(Paths‘𝐺)𝑃 → ((𝑃 “ {0, (♯‘𝐹)}) ∩ (𝑃 “ (1..^(♯‘𝐹)))) = ∅)
58	56, 57	eqtrd 2798	. . . . . 6 ⊢ (𝐹(Paths‘𝐺)𝑃 → ((𝑃 “ {0, (♯‘𝐹)}) ∩ ((𝑃 ↾ (0...((♯‘𝐹) − 1))) “ (1...((♯‘𝐹) − 1)))) = ∅)
59		ssdisj 4416	. . . . . 6 ⊢ ((((𝑃 ↾ (0...((♯‘𝐹) − 1))) “ {0}) ⊆ (𝑃 “ {0, (♯‘𝐹)}) ∧ ((𝑃 “ {0, (♯‘𝐹)}) ∩ ((𝑃 ↾ (0...((♯‘𝐹) − 1))) “ (1...((♯‘𝐹) − 1)))) = ∅) → (((𝑃 ↾ (0...((♯‘𝐹) − 1))) “ {0}) ∩ ((𝑃 ↾ (0...((♯‘𝐹) − 1))) “ (1...((♯‘𝐹) − 1)))) = ∅)
60	51, 58, 59	syl2anr 609	. . . . 5 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ ((♯‘𝐹) − 1) ∈ ℕ₀) → (((𝑃 ↾ (0...((♯‘𝐹) − 1))) “ {0}) ∩ ((𝑃 ↾ (0...((♯‘𝐹) − 1))) “ (1...((♯‘𝐹) − 1)))) = ∅)
61	16, 21, 42, 60	f1resfz0f1d 13957	. . . 4 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ ((♯‘𝐹) − 1) ∈ ℕ₀) → (𝑃 ↾ (0...((♯‘𝐹) − 1))):(0...((♯‘𝐹) − 1))⟶1-1𝑉)
62	9	fvexi 6925	. . . . 5 ⊢ 𝑉 ∈ V
63		hashf1dmcdm 14619	. . . . 5 ⊢ (((𝑃 ↾ (0...((♯‘𝐹) − 1))) ∈ Fin ∧ 𝑉 ∈ V ∧ (𝑃 ↾ (0...((♯‘𝐹) − 1))):(0...((♯‘𝐹) − 1))⟶1-1𝑉) → (♯‘(0...((♯‘𝐹) − 1))) ≤ (♯‘𝑉))
64	62, 63	mp3an2 1479	. . . 4 ⊢ (((𝑃 ↾ (0...((♯‘𝐹) − 1))) ∈ Fin ∧ (𝑃 ↾ (0...((♯‘𝐹) − 1))):(0...((♯‘𝐹) − 1))⟶1-1𝑉) → (♯‘(0...((♯‘𝐹) − 1))) ≤ (♯‘𝑉))
65	15, 61, 64	syl2an2r 698	. . 3 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ ((♯‘𝐹) − 1) ∈ ℕ₀) → (♯‘(0...((♯‘𝐹) − 1))) ≤ (♯‘𝑉))
66	8, 65	eqbrtrrd 5133	. 2 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ ((♯‘𝐹) − 1) ∈ ℕ₀) → (♯‘𝐹) ≤ (♯‘𝑉))
67		0nn0m1nnn0 12783	. . . . 5 ⊢ ((♯‘𝐹) = 0 ↔ ((♯‘𝐹) ∈ ℕ₀ ∧ ¬ ((♯‘𝐹) − 1) ∈ ℕ₀))
68	67	biimpri 231	. . . 4 ⊢ (((♯‘𝐹) ∈ ℕ₀ ∧ ¬ ((♯‘𝐹) − 1) ∈ ℕ₀) → (♯‘𝐹) = 0)
69	4, 68	sylan 592	. . 3 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ ¬ ((♯‘𝐹) − 1) ∈ ℕ₀) → (♯‘𝐹) = 0)
70		hashge0 14561	. . . 4 ⊢ (𝑉 ∈ V → 0 ≤ (♯‘𝑉))
71	62, 70	ax-mp 5	. . 3 ⊢ 0 ≤ (♯‘𝑉)
72	69, 71	eqbrtrdi 5148	. 2 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ ¬ ((♯‘𝐹) − 1) ∈ ℕ₀) → (♯‘𝐹) ≤ (♯‘𝑉))
73	66, 72	pm2.61dan 825	1 ⊢ (𝐹(Paths‘𝐺)𝑃 → (♯‘𝐹) ≤ (♯‘𝑉))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2147 Vcvv 3454 ⊆ wss 3900 ∩ cin 4092 ∅c0 4281 {csn 4588 {cpr 4590 class class class wbr 5106 ^◡ccnv 5655 ↾ cres 5658 “ cima 5659 Fun wfun 6555 Fn wfn 6556 ⟶wf 6557 ⟶1-1wf1 6558 ‘cfv 6561 (class class class)co 7446 Fincfn 9004 ℂcc 11228 0cc0 11230 1c1 11231 + caddc 11233 ≤ cle 11374 − cmin 11571 ℕ₀cn0 12636 ℤcz 12723 ...cfz 13669 ..^cfzo 13818 ♯chash 14504 Vtxcvtx 29607 Walkscwlks 30210 Trailsctrls 30306 Pathscpths 30328

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5236 ax-sep 5253 ax-nul 5264 ax-pow 5332 ax-pr 5396 ax-un 7778 ax-cnex 11286 ax-resscn 11287 ax-1cn 11288 ax-icn 11289 ax-addcl 11290 ax-addrcl 11291 ax-mulcl 11292 ax-mulrcl 11293 ax-mulcom 11294 ax-addass 11295 ax-mulass 11296 ax-distr 11297 ax-i2m1 11298 ax-1ne0 11299 ax-1rid 11300 ax-rnegex 11301 ax-rrecex 11302 ax-cnre 11303 ax-pre-lttri 11304 ax-pre-lttrn 11305 ax-pre-ltadd 11306 ax-pre-mulgt0 11307

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-ifp 1079 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-br 5107 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5551 df-eprel 5556 df-po 5564 df-so 5565 df-fr 5609 df-we 5611 df-xp 5662 df-rel 5663 df-cnv 5664 df-co 5665 df-dm 5666 df-rn 5667 df-res 5668 df-ima 5669 df-pred 6325 df-ord 6386 df-on 6387 df-lim 6388 df-suc 6389 df-iota 6515 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-riota 7403 df-ov 7449 df-oprab 7450 df-mpo 7451 df-om 7905 df-1st 8028 df-2nd 8029 df-frecs 8330 df-wrecs 8361 df-recs 8410 df-rdg 8449 df-1o 8507 df-2o 8508 df-oadd 8511 df-er 8748 df-map 8880 df-en 9005 df-dom 9006 df-sdom 9007 df-fin 9008 df-dju 10012 df-card 10050 df-pnf 11375 df-mnf 11376 df-xr 11377 df-ltxr 11378 df-le 11379 df-sub 11573 df-neg 11574 df-nn 12366 df-2 12435 df-n0 12637 df-xnn0 12710 df-z 12724 df-uz 12996 df-fz 13670 df-fzo 13819 df-hash 14505 df-word 14689 df-wlks 30213 df-trls 30308 df-pths 30332

This theorem is used by: usgrcyclgt2v 36080 acycgr1v 36084

W3C validator