cyclnumvtx - Metamath Proof Explorer

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

Theorem cyclnumvtx 30115

Description: The number of vertices of a (non-trivial) cycle is the number of edges in the cycle. (Contributed by AV, 5-Oct-2025.)

**Assertion**
Ref	Expression
cyclnumvtx	⊢ ((1 ≤ (♯‘𝐹) ∧ 𝐹(Cycles‘𝐺)𝑃) → (♯‘ran 𝑃) = (♯‘𝐹))

**Proof of Theorem cyclnumvtx**
Step	Hyp	Ref	Expression
1		iscycl 30106	. . . . 5 ⊢ (𝐹(Cycles‘𝐺)𝑃 ↔ (𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))))
2		pthiswlk 30040	. . . . . . 7 ⊢ (𝐹(Paths‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
3		eqid 2761	. . . . . . . . 9 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
4	3	wlkp 29932	. . . . . . . 8 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺))
5		wlkcl 29931	. . . . . . . 8 ⊢ (𝐹(Walks‘𝐺)𝑃 → (♯‘𝐹) ∈ ℕ₀)
6		elnnnn0c 12548	. . . . . . . . . . 11 ⊢ ((♯‘𝐹) ∈ ℕ ↔ ((♯‘𝐹) ∈ ℕ₀ ∧ 1 ≤ (♯‘𝐹)))
7		fdm 6715	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) → dom 𝑃 = (0...(♯‘𝐹)))
8	7	3ad2ant1 1149	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ (♯‘𝐹) ∈ ℕ ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → dom 𝑃 = (0...(♯‘𝐹)))
9	8	difeq1d 4079	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ (♯‘𝐹) ∈ ℕ ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (dom 𝑃 ∖ (1...(♯‘𝐹))) = ((0...(♯‘𝐹)) ∖ (1...(♯‘𝐹))))
10		nnnn0 12510	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝐹) ∈ ℕ → (♯‘𝐹) ∈ ℕ₀)
11		fz0sn0fz1 13672	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝐹) ∈ ℕ₀ → (0...(♯‘𝐹)) = ({0} ∪ (1...(♯‘𝐹))))
12	10, 11	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘𝐹) ∈ ℕ → (0...(♯‘𝐹)) = ({0} ∪ (1...(♯‘𝐹))))
13	12	difeq1d 4079	. . . . . . . . . . . . . . . . . . 19 ⊢ ((♯‘𝐹) ∈ ℕ → ((0...(♯‘𝐹)) ∖ (1...(♯‘𝐹))) = (({0} ∪ (1...(♯‘𝐹))) ∖ (1...(♯‘𝐹))))
14		1e0p1 12757	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 = (0 + 1)
15	14	oveq1i 7420	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1...(♯‘𝐹)) = ((0 + 1)...(♯‘𝐹))
16	15	ineq2i 4169	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({0} ∩ (1...(♯‘𝐹))) = ({0} ∩ ((0 + 1)...(♯‘𝐹)))
17		elnn0uz 12902	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((♯‘𝐹) ∈ ℕ₀ ↔ (♯‘𝐹) ∈ (ℤ_≥‘0))
18	10, 17	sylib 221	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((♯‘𝐹) ∈ ℕ → (♯‘𝐹) ∈ (ℤ_≥‘0))
19		fzpreddisj 13600	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((♯‘𝐹) ∈ (ℤ_≥‘0) → ({0} ∩ ((0 + 1)...(♯‘𝐹))) = ∅)
20	18, 19	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝐹) ∈ ℕ → ({0} ∩ ((0 + 1)...(♯‘𝐹))) = ∅)
21	16, 20	eqtrid 2808	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘𝐹) ∈ ℕ → ({0} ∩ (1...(♯‘𝐹))) = ∅)
22		undif5 4444	. . . . . . . . . . . . . . . . . . . 20 ⊢ (({0} ∩ (1...(♯‘𝐹))) = ∅ → (({0} ∪ (1...(♯‘𝐹))) ∖ (1...(♯‘𝐹))) = {0})
23	21, 22	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((♯‘𝐹) ∈ ℕ → (({0} ∪ (1...(♯‘𝐹))) ∖ (1...(♯‘𝐹))) = {0})
24	13, 23	eqtrd 2796	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝐹) ∈ ℕ → ((0...(♯‘𝐹)) ∖ (1...(♯‘𝐹))) = {0})
25	24	3ad2ant2 1150	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ (♯‘𝐹) ∈ ℕ ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((0...(♯‘𝐹)) ∖ (1...(♯‘𝐹))) = {0})
26	9, 25	eqtrd 2796	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ (♯‘𝐹) ∈ ℕ ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (dom 𝑃 ∖ (1...(♯‘𝐹))) = {0})
27	26	imaeq2d 6062	. . . . . . . . . . . . . . 15 ⊢ ((𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ (♯‘𝐹) ∈ ℕ ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝑃 “ (dom 𝑃 ∖ (1...(♯‘𝐹)))) = (𝑃 “ {0}))
28		ffn 6705	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) → 𝑃 Fn (0...(♯‘𝐹)))
29		0elfz 13651	. . . . . . . . . . . . . . . . . . 19 ⊢ ((♯‘𝐹) ∈ ℕ₀ → 0 ∈ (0...(♯‘𝐹)))
30	10, 29	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝐹) ∈ ℕ → 0 ∈ (0...(♯‘𝐹)))
31	28, 30	anim12i 624	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ (♯‘𝐹) ∈ ℕ) → (𝑃 Fn (0...(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹))))
32	31	3adant3 1148	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ (♯‘𝐹) ∈ ℕ ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝑃 Fn (0...(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹))))
33		fnsnfv 6960	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 Fn (0...(♯‘𝐹)) ∧ 0 ∈ (0...(♯‘𝐹))) → {(𝑃‘0)} = (𝑃 “ {0}))
34	32, 33	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ (♯‘𝐹) ∈ ℕ ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → {(𝑃‘0)} = (𝑃 “ {0}))
35	27, 34	eqtr4d 2799	. . . . . . . . . . . . . 14 ⊢ ((𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ (♯‘𝐹) ∈ ℕ ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝑃 “ (dom 𝑃 ∖ (1...(♯‘𝐹)))) = {(𝑃‘0)})
36		elfz1end 13581	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘𝐹) ∈ ℕ ↔ (♯‘𝐹) ∈ (1...(♯‘𝐹)))
37	36	biimpi 219	. . . . . . . . . . . . . . . . . . 19 ⊢ ((♯‘𝐹) ∈ ℕ → (♯‘𝐹) ∈ (1...(♯‘𝐹)))
38	37	3ad2ant2 1150	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ (♯‘𝐹) ∈ ℕ ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (♯‘𝐹) ∈ (1...(♯‘𝐹)))
39	38	fvresd 6901	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ (♯‘𝐹) ∈ ℕ ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((𝑃 ↾ (1...(♯‘𝐹)))‘(♯‘𝐹)) = (𝑃‘(♯‘𝐹)))
40		ffun 6708	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) → Fun 𝑃)
41	40	funresd 6579	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) → Fun (𝑃 ↾ (1...(♯‘𝐹))))
42	41	3ad2ant1 1149	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ (♯‘𝐹) ∈ ℕ ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → Fun (𝑃 ↾ (1...(♯‘𝐹))))
43		fz1ssfz0 13650	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1...(♯‘𝐹)) ⊆ (0...(♯‘𝐹))
44	43, 7	sseqtrrid 3979	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) → (1...(♯‘𝐹)) ⊆ dom 𝑃)
45	44	3ad2ant1 1149	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ (♯‘𝐹) ∈ ℕ ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (1...(♯‘𝐹)) ⊆ dom 𝑃)
46		ssdmres 6012	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1...(♯‘𝐹)) ⊆ dom 𝑃 ↔ dom (𝑃 ↾ (1...(♯‘𝐹))) = (1...(♯‘𝐹)))
47	45, 46	sylib 221	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ (♯‘𝐹) ∈ ℕ ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → dom (𝑃 ↾ (1...(♯‘𝐹))) = (1...(♯‘𝐹)))
48	38, 47	eleqtrrd 2864	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ (♯‘𝐹) ∈ ℕ ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (♯‘𝐹) ∈ dom (𝑃 ↾ (1...(♯‘𝐹))))
49		fvelrn 7071	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun (𝑃 ↾ (1...(♯‘𝐹))) ∧ (♯‘𝐹) ∈ dom (𝑃 ↾ (1...(♯‘𝐹)))) → ((𝑃 ↾ (1...(♯‘𝐹)))‘(♯‘𝐹)) ∈ ran (𝑃 ↾ (1...(♯‘𝐹))))
50	42, 48, 49	syl2anc 595	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ (♯‘𝐹) ∈ ℕ ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((𝑃 ↾ (1...(♯‘𝐹)))‘(♯‘𝐹)) ∈ ran (𝑃 ↾ (1...(♯‘𝐹))))
51	39, 50	eqeltrrd 2862	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ (♯‘𝐹) ∈ ℕ ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝑃‘(♯‘𝐹)) ∈ ran (𝑃 ↾ (1...(♯‘𝐹))))
52		eleq1 2849	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → ((𝑃‘0) ∈ ran (𝑃 ↾ (1...(♯‘𝐹))) ↔ (𝑃‘(♯‘𝐹)) ∈ ran (𝑃 ↾ (1...(♯‘𝐹)))))
53	52	3ad2ant3 1151	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ (♯‘𝐹) ∈ ℕ ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((𝑃‘0) ∈ ran (𝑃 ↾ (1...(♯‘𝐹))) ↔ (𝑃‘(♯‘𝐹)) ∈ ran (𝑃 ↾ (1...(♯‘𝐹)))))
54	51, 53	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ ((𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ (♯‘𝐹) ∈ ℕ ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝑃‘0) ∈ ran (𝑃 ↾ (1...(♯‘𝐹))))
55	54	snssd 4751	. . . . . . . . . . . . . 14 ⊢ ((𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ (♯‘𝐹) ∈ ℕ ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → {(𝑃‘0)} ⊆ ran (𝑃 ↾ (1...(♯‘𝐹))))
56	35, 55	eqsstrd 3970	. . . . . . . . . . . . 13 ⊢ ((𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) ∧ (♯‘𝐹) ∈ ℕ ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝑃 “ (dom 𝑃 ∖ (1...(♯‘𝐹)))) ⊆ ran (𝑃 ↾ (1...(♯‘𝐹))))
57	56	3exp 1135	. . . . . . . . . . . 12 ⊢ (𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) → ((♯‘𝐹) ∈ ℕ → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝑃 “ (dom 𝑃 ∖ (1...(♯‘𝐹)))) ⊆ ran (𝑃 ↾ (1...(♯‘𝐹))))))
58	57	com3l 90	. . . . . . . . . . 11 ⊢ ((♯‘𝐹) ∈ ℕ → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) → (𝑃 “ (dom 𝑃 ∖ (1...(♯‘𝐹)))) ⊆ ran (𝑃 ↾ (1...(♯‘𝐹))))))
59	6, 58	sylbir 238	. . . . . . . . . 10 ⊢ (((♯‘𝐹) ∈ ℕ₀ ∧ 1 ≤ (♯‘𝐹)) → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) → (𝑃 “ (dom 𝑃 ∖ (1...(♯‘𝐹)))) ⊆ ran (𝑃 ↾ (1...(♯‘𝐹))))))
60	59	expcom 418	. . . . . . . . 9 ⊢ (1 ≤ (♯‘𝐹) → ((♯‘𝐹) ∈ ℕ₀ → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) → (𝑃 “ (dom 𝑃 ∖ (1...(♯‘𝐹)))) ⊆ ran (𝑃 ↾ (1...(♯‘𝐹)))))))
61	60	com14 97	. . . . . . . 8 ⊢ (𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺) → ((♯‘𝐹) ∈ ℕ₀ → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (1 ≤ (♯‘𝐹) → (𝑃 “ (dom 𝑃 ∖ (1...(♯‘𝐹)))) ⊆ ran (𝑃 ↾ (1...(♯‘𝐹)))))))
62	4, 5, 61	sylc 66	. . . . . . 7 ⊢ (𝐹(Walks‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (1 ≤ (♯‘𝐹) → (𝑃 “ (dom 𝑃 ∖ (1...(♯‘𝐹)))) ⊆ ran (𝑃 ↾ (1...(♯‘𝐹))))))
63	2, 62	syl 18	. . . . . 6 ⊢ (𝐹(Paths‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (1 ≤ (♯‘𝐹) → (𝑃 “ (dom 𝑃 ∖ (1...(♯‘𝐹)))) ⊆ ran (𝑃 ↾ (1...(♯‘𝐹))))))
64	63	imp 411	. . . . 5 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (1 ≤ (♯‘𝐹) → (𝑃 “ (dom 𝑃 ∖ (1...(♯‘𝐹)))) ⊆ ran (𝑃 ↾ (1...(♯‘𝐹)))))
65	1, 64	sylbi 220	. . . 4 ⊢ (𝐹(Cycles‘𝐺)𝑃 → (1 ≤ (♯‘𝐹) → (𝑃 “ (dom 𝑃 ∖ (1...(♯‘𝐹)))) ⊆ ran (𝑃 ↾ (1...(♯‘𝐹)))))
66	65	impcom 412	. . 3 ⊢ ((1 ≤ (♯‘𝐹) ∧ 𝐹(Cycles‘𝐺)𝑃) → (𝑃 “ (dom 𝑃 ∖ (1...(♯‘𝐹)))) ⊆ ran (𝑃 ↾ (1...(♯‘𝐹))))
67		imadifssran 6202	. . . 4 ⊢ ((𝑃 “ (dom 𝑃 ∖ (1...(♯‘𝐹)))) ⊆ ran (𝑃 ↾ (1...(♯‘𝐹))) → ran 𝑃 = ran (𝑃 ↾ (1...(♯‘𝐹))))
68	67	fveq2d 6885	. . 3 ⊢ ((𝑃 “ (dom 𝑃 ∖ (1...(♯‘𝐹)))) ⊆ ran (𝑃 ↾ (1...(♯‘𝐹))) → (♯‘ran 𝑃) = (♯‘ran (𝑃 ↾ (1...(♯‘𝐹)))))
69	66, 68	syl 18	. 2 ⊢ ((1 ≤ (♯‘𝐹) ∧ 𝐹(Cycles‘𝐺)𝑃) → (♯‘ran 𝑃) = (♯‘ran (𝑃 ↾ (1...(♯‘𝐹)))))
70		cyclispth 30112	. . . 4 ⊢ (𝐹(Cycles‘𝐺)𝑃 → 𝐹(Paths‘𝐺)𝑃)
71		pthdifv 30045	. . . 4 ⊢ (𝐹(Paths‘𝐺)𝑃 → (𝑃 ↾ (1...(♯‘𝐹))):(1...(♯‘𝐹))–1-1→(Vtx‘𝐺))
72	40	adantl 486	. . . . . . . . . 10 ⊢ (((♯‘𝐹) ∈ ℕ₀ ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) → Fun 𝑃)
73		fzfid 14008	. . . . . . . . . . 11 ⊢ ((♯‘𝐹) ∈ ℕ₀ → (0...(♯‘𝐹)) ∈ Fin)
74		fnfi 9161	. . . . . . . . . . 11 ⊢ ((𝑃 Fn (0...(♯‘𝐹)) ∧ (0...(♯‘𝐹)) ∈ Fin) → 𝑃 ∈ Fin)
75	28, 73, 74	syl2anr 608	. . . . . . . . . 10 ⊢ (((♯‘𝐹) ∈ ℕ₀ ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) → 𝑃 ∈ Fin)
76		1eluzge0 12903	. . . . . . . . . . . 12 ⊢ 1 ∈ (ℤ_≥‘0)
77		fzss1 13590	. . . . . . . . . . . 12 ⊢ (1 ∈ (ℤ_≥‘0) → (1...(♯‘𝐹)) ⊆ (0...(♯‘𝐹)))
78	76, 77	mp1i 14	. . . . . . . . . . 11 ⊢ (((♯‘𝐹) ∈ ℕ₀ ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) → (1...(♯‘𝐹)) ⊆ (0...(♯‘𝐹)))
79	7	adantl 486	. . . . . . . . . . 11 ⊢ (((♯‘𝐹) ∈ ℕ₀ ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) → dom 𝑃 = (0...(♯‘𝐹)))
80	78, 79	sseqtrrd 3973	. . . . . . . . . 10 ⊢ (((♯‘𝐹) ∈ ℕ₀ ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) → (1...(♯‘𝐹)) ⊆ dom 𝑃)
81	72, 75, 80	3jca 1144	. . . . . . . . 9 ⊢ (((♯‘𝐹) ∈ ℕ₀ ∧ 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺)) → (Fun 𝑃 ∧ 𝑃 ∈ Fin ∧ (1...(♯‘𝐹)) ⊆ dom 𝑃))
82	5, 4, 81	syl2anc 595	. . . . . . . 8 ⊢ (𝐹(Walks‘𝐺)𝑃 → (Fun 𝑃 ∧ 𝑃 ∈ Fin ∧ (1...(♯‘𝐹)) ⊆ dom 𝑃))
83	2, 82	syl 18	. . . . . . 7 ⊢ (𝐹(Paths‘𝐺)𝑃 → (Fun 𝑃 ∧ 𝑃 ∈ Fin ∧ (1...(♯‘𝐹)) ⊆ dom 𝑃))
84	83	adantr 485	. . . . . 6 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃 ↾ (1...(♯‘𝐹))):(1...(♯‘𝐹))–1-1→(Vtx‘𝐺)) → (Fun 𝑃 ∧ 𝑃 ∈ Fin ∧ (1...(♯‘𝐹)) ⊆ dom 𝑃))
85		hashres 14474	. . . . . 6 ⊢ ((Fun 𝑃 ∧ 𝑃 ∈ Fin ∧ (1...(♯‘𝐹)) ⊆ dom 𝑃) → (♯‘(𝑃 ↾ (1...(♯‘𝐹)))) = (♯‘(1...(♯‘𝐹))))
86	84, 85	syl 18	. . . . 5 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃 ↾ (1...(♯‘𝐹))):(1...(♯‘𝐹))–1-1→(Vtx‘𝐺)) → (♯‘(𝑃 ↾ (1...(♯‘𝐹)))) = (♯‘(1...(♯‘𝐹))))
87		ovexd 7445	. . . . . 6 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃 ↾ (1...(♯‘𝐹))):(1...(♯‘𝐹))–1-1→(Vtx‘𝐺)) → (1...(♯‘𝐹)) ∈ V)
88		hashf1rn 14387	. . . . . 6 ⊢ (((1...(♯‘𝐹)) ∈ V ∧ (𝑃 ↾ (1...(♯‘𝐹))):(1...(♯‘𝐹))–1-1→(Vtx‘𝐺)) → (♯‘(𝑃 ↾ (1...(♯‘𝐹)))) = (♯‘ran (𝑃 ↾ (1...(♯‘𝐹)))))
89	87, 88	sylancom 599	. . . . 5 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃 ↾ (1...(♯‘𝐹))):(1...(♯‘𝐹))–1-1→(Vtx‘𝐺)) → (♯‘(𝑃 ↾ (1...(♯‘𝐹)))) = (♯‘ran (𝑃 ↾ (1...(♯‘𝐹)))))
90	2, 5	syl 18	. . . . . . 7 ⊢ (𝐹(Paths‘𝐺)𝑃 → (♯‘𝐹) ∈ ℕ₀)
91		hashfz1 14381	. . . . . . 7 ⊢ ((♯‘𝐹) ∈ ℕ₀ → (♯‘(1...(♯‘𝐹))) = (♯‘𝐹))
92	90, 91	syl 18	. . . . . 6 ⊢ (𝐹(Paths‘𝐺)𝑃 → (♯‘(1...(♯‘𝐹))) = (♯‘𝐹))
93	92	adantr 485	. . . . 5 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃 ↾ (1...(♯‘𝐹))):(1...(♯‘𝐹))–1-1→(Vtx‘𝐺)) → (♯‘(1...(♯‘𝐹))) = (♯‘𝐹))
94	86, 89, 93	3eqtr3d 2804	. . . 4 ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃 ↾ (1...(♯‘𝐹))):(1...(♯‘𝐹))–1-1→(Vtx‘𝐺)) → (♯‘ran (𝑃 ↾ (1...(♯‘𝐹)))) = (♯‘𝐹))
95	70, 71, 94	syl2anc2 596	. . 3 ⊢ (𝐹(Cycles‘𝐺)𝑃 → (♯‘ran (𝑃 ↾ (1...(♯‘𝐹)))) = (♯‘𝐹))
96	95	adantl 486	. 2 ⊢ ((1 ≤ (♯‘𝐹) ∧ 𝐹(Cycles‘𝐺)𝑃) → (♯‘ran (𝑃 ↾ (1...(♯‘𝐹)))) = (♯‘𝐹))
97	69, 96	eqtrd 2796	1 ⊢ ((1 ≤ (♯‘𝐹) ∧ 𝐹(Cycles‘𝐺)𝑃) → (♯‘ran 𝑃) = (♯‘𝐹))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1101 = wceq 1568 ∈ wcel 2141 Vcvv 3453 ∖ cdif 3901 ∪ cun 3902 ∩ cin 3903 ⊆ wss 3904 ∅c0 4285 {csn 4588 class class class wbr 5108 dom cdm 5661 ran crn 5662 ↾ cres 5663 “ cima 5664 Fun wfun 6530 Fn wfn 6531 ⟶wf 6532 –1-1→wf1 6533 ‘cfv 6536 (class class class)co 7410 Fincfn 8942 0cc0 11099 1c1 11100 + caddc 11102 ≤ cle 11243 ℕcn 12232 ℕ₀cn0 12503 ℤ_≥cuz 12861 ...cfz 13534 ♯chash 14365 Vtxcvtx 29312 Walkscwlks 29912 Pathscpths 30025 Cyclesccycls 30100

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1823 ax-4 1837 ax-5 1938 ax-6 1995 ax-7 2036 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5237 ax-sep 5256 ax-nul 5268 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-cnex 11155 ax-resscn 11156 ax-1cn 11157 ax-icn 11158 ax-addcl 11159 ax-addrcl 11160 ax-mulcl 11161 ax-mulrcl 11162 ax-mulcom 11163 ax-addass 11164 ax-mulass 11165 ax-distr 11166 ax-i2m1 11167 ax-1ne0 11168 ax-1rid 11169 ax-rnegex 11170 ax-rrecex 11171 ax-cnre 11172 ax-pre-lttri 11173 ax-pre-lttrn 11174 ax-pre-ltadd 11175 ax-pre-mulgt0 11176

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-ifp 1077 df-3or 1102 df-3an 1103 df-tru 1571 df-fal 1581 df-ex 1808 df-nf 1812 df-sb 2095 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-op 4595 df-uni 4872 df-int 4912 df-iun 4957 df-br 5109 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7862 df-1st 7985 df-2nd 7986 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8452 df-2o 8453 df-oadd 8456 df-er 8693 df-map 8825 df-en 8943 df-dom 8944 df-sdom 8945 df-fin 8946 df-dju 9886 df-card 9924 df-pnf 11244 df-mnf 11245 df-xr 11246 df-ltxr 11247 df-le 11248 df-sub 11442 df-neg 11443 df-nn 12233 df-2 12302 df-n0 12504 df-xnn0 12577 df-z 12591 df-uz 12862 df-fz 13535 df-fzo 13682 df-hash 14366 df-word 14550 df-wlks 29915 df-trls 30006 df-pths 30029 df-cycls 30102

This theorem is referenced by: cycl3grtri 48657

W3C validator