cyclnumvtx

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

		Ref	Expression
	Assertion	cyclnumvtx	$⊢ (1 \leq \|F\| \land F Cycles (G) P) \to \|ran P\| = \|F\|$

Proof

Step	Hyp	Ref	Expression
1		iscycl	$⊢ F Cycles (G) P \leftrightarrow (F Paths (G) P \land P (0) = P (\|F\|))$
2		pthiswlk	$⊢ F Paths (G) P \to F Walks (G) P$
3		eqid	$⊢ Vtx (G) = Vtx (G)$
4	3	wlkp	$⊢ F Walks (G) P \to P : (0 \dots \|F\|) ⟶ Vtx (G)$
5		wlkcl	$⊢ F Walks (G) P \to \|F\| \in ℕ_{0}$
6		elnnnn0c	$⊢ \|F\| \in ℕ \leftrightarrow (\|F\| \in ℕ_{0} \land 1 \leq \|F\|)$
7		fdm	$⊢ P : (0 \dots \|F\|) ⟶ Vtx (G) \to dom P = (0 \dots \|F\|)$
8	7	3ad2ant1	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land \|F\| \in ℕ \land P (0) = P (\|F\|)) \to dom P = (0 \dots \|F\|)$
9	8	difeq1d	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land \|F\| \in ℕ \land P (0) = P (\|F\|)) \to dom P ∖ (1 \dots \|F\|) = (0 \dots \|F\|) ∖ (1 \dots \|F\|)$
10		nnnn0	$⊢ \|F\| \in ℕ \to \|F\| \in ℕ_{0}$
11		fz0sn0fz1	$⊢ \|F\| \in ℕ_{0} \to (0 \dots \|F\|) = \{0\} \cup (1 \dots \|F\|)$
12	10 11	syl	$⊢ \|F\| \in ℕ \to (0 \dots \|F\|) = \{0\} \cup (1 \dots \|F\|)$
13	12	difeq1d	$⊢ \|F\| \in ℕ \to (0 \dots \|F\|) ∖ (1 \dots \|F\|) = (\{0\} \cup (1 \dots \|F\|)) ∖ (1 \dots \|F\|)$
14		1e0p1	$⊢ 1 = 0 + 1$
15	14	oveq1i	$⊢ (1 \dots \|F\|) = (0 + 1 \dots \|F\|)$
16	15	ineq2i	$⊢ \{0\} \cap (1 \dots \|F\|) = \{0\} \cap (0 + 1 \dots \|F\|)$
17		elnn0uz	$⊢ \|F\| \in ℕ_{0} \leftrightarrow \|F\| \in ℤ_{\geq 0}$
18	10 17	sylib	$⊢ \|F\| \in ℕ \to \|F\| \in ℤ_{\geq 0}$
19		fzpreddisj	$⊢ \|F\| \in ℤ_{\geq 0} \to \{0\} \cap (0 + 1 \dots \|F\|) = \emptyset$
20	18 19	syl	$⊢ \|F\| \in ℕ \to \{0\} \cap (0 + 1 \dots \|F\|) = \emptyset$
21	16 20	eqtrid	$⊢ \|F\| \in ℕ \to \{0\} \cap (1 \dots \|F\|) = \emptyset$
22		undif5	$⊢ \{0\} \cap (1 \dots \|F\|) = \emptyset \to (\{0\} \cup (1 \dots \|F\|)) ∖ (1 \dots \|F\|) = \{0\}$
23	21 22	syl	$⊢ \|F\| \in ℕ \to (\{0\} \cup (1 \dots \|F\|)) ∖ (1 \dots \|F\|) = \{0\}$
24	13 23	eqtrd	$⊢ \|F\| \in ℕ \to (0 \dots \|F\|) ∖ (1 \dots \|F\|) = \{0\}$
25	24	3ad2ant2	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land \|F\| \in ℕ \land P (0) = P (\|F\|)) \to (0 \dots \|F\|) ∖ (1 \dots \|F\|) = \{0\}$
26	9 25	eqtrd	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land \|F\| \in ℕ \land P (0) = P (\|F\|)) \to dom P ∖ (1 \dots \|F\|) = \{0\}$
27	26	imaeq2d	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land \|F\| \in ℕ \land P (0) = P (\|F\|)) \to P [dom P ∖ (1 \dots \|F\|)] = P [\{0\}]$
28		ffn	$⊢ P : (0 \dots \|F\|) ⟶ Vtx (G) \to P Fn (0 \dots \|F\|)$
29		0elfz	$⊢ \|F\| \in ℕ_{0} \to 0 \in (0 \dots \|F\|)$
30	10 29	syl	$⊢ \|F\| \in ℕ \to 0 \in (0 \dots \|F\|)$
31	28 30	anim12i	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land \|F\| \in ℕ) \to (P Fn (0 \dots \|F\|) \land 0 \in (0 \dots \|F\|))$
32	31	3adant3	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land \|F\| \in ℕ \land P (0) = P (\|F\|)) \to (P Fn (0 \dots \|F\|) \land 0 \in (0 \dots \|F\|))$
33		fnsnfv	$⊢ (P Fn (0 \dots \|F\|) \land 0 \in (0 \dots \|F\|)) \to \{P (0)\} = P [\{0\}]$
34	32 33	syl	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land \|F\| \in ℕ \land P (0) = P (\|F\|)) \to \{P (0)\} = P [\{0\}]$
35	27 34	eqtr4d	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land \|F\| \in ℕ \land P (0) = P (\|F\|)) \to P [dom P ∖ (1 \dots \|F\|)] = \{P (0)\}$
36		elfz1end	$⊢ \|F\| \in ℕ \leftrightarrow \|F\| \in (1 \dots \|F\|)$
37	36	biimpi	$⊢ \|F\| \in ℕ \to \|F\| \in (1 \dots \|F\|)$
38	37	3ad2ant2	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land \|F\| \in ℕ \land P (0) = P (\|F\|)) \to \|F\| \in (1 \dots \|F\|)$
39	38	fvresd	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land \|F\| \in ℕ \land P (0) = P (\|F\|)) \to ({P ↾}_{(1 \dots \|F\|)}) (\|F\|) = P (\|F\|)$
40		ffun	$⊢ P : (0 \dots \|F\|) ⟶ Vtx (G) \to Fun P$
41	40	funresd	$⊢ P : (0 \dots \|F\|) ⟶ Vtx (G) \to Fun ({P ↾}_{(1 \dots \|F\|)})$
42	41	3ad2ant1	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land \|F\| \in ℕ \land P (0) = P (\|F\|)) \to Fun ({P ↾}_{(1 \dots \|F\|)})$
43		fz1ssfz0	$⊢ (1 \dots \|F\|) \subseteq (0 \dots \|F\|)$
44	43 7	sseqtrrid	$⊢ P : (0 \dots \|F\|) ⟶ Vtx (G) \to (1 \dots \|F\|) \subseteq dom P$
45	44	3ad2ant1	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land \|F\| \in ℕ \land P (0) = P (\|F\|)) \to (1 \dots \|F\|) \subseteq dom P$
46		ssdmres	$⊢ (1 \dots \|F\|) \subseteq dom P \leftrightarrow dom ({P ↾}_{(1 \dots \|F\|)}) = (1 \dots \|F\|)$
47	45 46	sylib	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land \|F\| \in ℕ \land P (0) = P (\|F\|)) \to dom ({P ↾}_{(1 \dots \|F\|)}) = (1 \dots \|F\|)$
48	38 47	eleqtrrd	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land \|F\| \in ℕ \land P (0) = P (\|F\|)) \to \|F\| \in dom ({P ↾}_{(1 \dots \|F\|)})$
49		fvelrn	$⊢ (Fun ({P ↾}_{(1 \dots \|F\|)}) \land \|F\| \in dom ({P ↾}_{(1 \dots \|F\|)})) \to ({P ↾}_{(1 \dots \|F\|)}) (\|F\|) \in ran ({P ↾}_{(1 \dots \|F\|)})$
50	42 48 49	syl2anc	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land \|F\| \in ℕ \land P (0) = P (\|F\|)) \to ({P ↾}_{(1 \dots \|F\|)}) (\|F\|) \in ran ({P ↾}_{(1 \dots \|F\|)})$
51	39 50	eqeltrrd	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land \|F\| \in ℕ \land P (0) = P (\|F\|)) \to P (\|F\|) \in ran ({P ↾}_{(1 \dots \|F\|)})$
52		eleq1	$⊢ P (0) = P (\|F\|) \to (P (0) \in ran ({P ↾}_{(1 \dots \|F\|)}) \leftrightarrow P (\|F\|) \in ran ({P ↾}_{(1 \dots \|F\|)}))$
53	52	3ad2ant3	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land \|F\| \in ℕ \land P (0) = P (\|F\|)) \to (P (0) \in ran ({P ↾}_{(1 \dots \|F\|)}) \leftrightarrow P (\|F\|) \in ran ({P ↾}_{(1 \dots \|F\|)}))$
54	51 53	mpbird	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land \|F\| \in ℕ \land P (0) = P (\|F\|)) \to P (0) \in ran ({P ↾}_{(1 \dots \|F\|)})$
55	54	snssd	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land \|F\| \in ℕ \land P (0) = P (\|F\|)) \to \{P (0)\} \subseteq ran ({P ↾}_{(1 \dots \|F\|)})$
56	35 55	eqsstrd	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land \|F\| \in ℕ \land P (0) = P (\|F\|)) \to P [dom P ∖ (1 \dots \|F\|)] \subseteq ran ({P ↾}_{(1 \dots \|F\|)})$
57	56	3exp	$⊢ P : (0 \dots \|F\|) ⟶ Vtx (G) \to (\|F\| \in ℕ \to (P (0) = P (\|F\|) \to P [dom P ∖ (1 \dots \|F\|)] \subseteq ran ({P ↾}_{(1 \dots \|F\|)})))$
58	57	com3l	$⊢ \|F\| \in ℕ \to (P (0) = P (\|F\|) \to (P : (0 \dots \|F\|) ⟶ Vtx (G) \to P [dom P ∖ (1 \dots \|F\|)] \subseteq ran ({P ↾}_{(1 \dots \|F\|)})))$
59	6 58	sylbir	$⊢ (\|F\| \in ℕ_{0} \land 1 \leq \|F\|) \to (P (0) = P (\|F\|) \to (P : (0 \dots \|F\|) ⟶ Vtx (G) \to P [dom P ∖ (1 \dots \|F\|)] \subseteq ran ({P ↾}_{(1 \dots \|F\|)})))$
60	59	expcom	$⊢ 1 \leq \|F\| \to (\|F\| \in ℕ_{0} \to (P (0) = P (\|F\|) \to (P : (0 \dots \|F\|) ⟶ Vtx (G) \to P [dom P ∖ (1 \dots \|F\|)] \subseteq ran ({P ↾}_{(1 \dots \|F\|)}))))$
61	60	com14	$⊢ P : (0 \dots \|F\|) ⟶ Vtx (G) \to (\|F\| \in ℕ_{0} \to (P (0) = P (\|F\|) \to (1 \leq \|F\| \to P [dom P ∖ (1 \dots \|F\|)] \subseteq ran ({P ↾}_{(1 \dots \|F\|)}))))$
62	4 5 61	sylc	$⊢ F Walks (G) P \to (P (0) = P (\|F\|) \to (1 \leq \|F\| \to P [dom P ∖ (1 \dots \|F\|)] \subseteq ran ({P ↾}_{(1 \dots \|F\|)})))$
63	2 62	syl	$⊢ F Paths (G) P \to (P (0) = P (\|F\|) \to (1 \leq \|F\| \to P [dom P ∖ (1 \dots \|F\|)] \subseteq ran ({P ↾}_{(1 \dots \|F\|)})))$
64	63	imp	$⊢ (F Paths (G) P \land P (0) = P (\|F\|)) \to (1 \leq \|F\| \to P [dom P ∖ (1 \dots \|F\|)] \subseteq ran ({P ↾}_{(1 \dots \|F\|)}))$
65	1 64	sylbi	$⊢ F Cycles (G) P \to (1 \leq \|F\| \to P [dom P ∖ (1 \dots \|F\|)] \subseteq ran ({P ↾}_{(1 \dots \|F\|)}))$
66	65	impcom	$⊢ (1 \leq \|F\| \land F Cycles (G) P) \to P [dom P ∖ (1 \dots \|F\|)] \subseteq ran ({P ↾}_{(1 \dots \|F\|)})$
67		imadifssran	$⊢ P [dom P ∖ (1 \dots \|F\|)] \subseteq ran ({P ↾}_{(1 \dots \|F\|)}) \to ran P = ran ({P ↾}_{(1 \dots \|F\|)})$
68	67	fveq2d	$⊢ P [dom P ∖ (1 \dots \|F\|)] \subseteq ran ({P ↾}_{(1 \dots \|F\|)}) \to \|ran P\| = \|ran ({P ↾}_{(1 \dots \|F\|)})\|$
69	66 68	syl	$⊢ (1 \leq \|F\| \land F Cycles (G) P) \to \|ran P\| = \|ran ({P ↾}_{(1 \dots \|F\|)})\|$
70		cyclispth	$⊢ F Cycles (G) P \to F Paths (G) P$
71		pthdifv	$⊢ F Paths (G) P \to ({P ↾}_{(1 \dots \|F\|)}) : (1 \dots \|F\|) \underset{1-1}{⟶} Vtx (G)$
72	40	adantl	$⊢ (\|F\| \in ℕ_{0} \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \to Fun P$
73		fzfid	$⊢ \|F\| \in ℕ_{0} \to (0 \dots \|F\|) \in Fin$
74		fnfi	$⊢ (P Fn (0 \dots \|F\|) \land (0 \dots \|F\|) \in Fin) \to P \in Fin$
75	28 73 74	syl2anr	$⊢ (\|F\| \in ℕ_{0} \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \to P \in Fin$
76		1eluzge0	$⊢ 1 \in ℤ_{\geq 0}$
77		fzss1	$⊢ 1 \in ℤ_{\geq 0} \to (1 \dots \|F\|) \subseteq (0 \dots \|F\|)$
78	76 77	mp1i	$⊢ (\|F\| \in ℕ_{0} \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \to (1 \dots \|F\|) \subseteq (0 \dots \|F\|)$
79	7	adantl	$⊢ (\|F\| \in ℕ_{0} \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \to dom P = (0 \dots \|F\|)$
80	78 79	sseqtrrd	$⊢ (\|F\| \in ℕ_{0} \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \to (1 \dots \|F\|) \subseteq dom P$
81	72 75 80	3jca	$⊢ (\|F\| \in ℕ_{0} \land P : (0 \dots \|F\|) ⟶ Vtx (G)) \to (Fun P \land P \in Fin \land (1 \dots \|F\|) \subseteq dom P)$
82	5 4 81	syl2anc	$⊢ F Walks (G) P \to (Fun P \land P \in Fin \land (1 \dots \|F\|) \subseteq dom P)$
83	2 82	syl	$⊢ F Paths (G) P \to (Fun P \land P \in Fin \land (1 \dots \|F\|) \subseteq dom P)$
84	83	adantr	$⊢ (F Paths (G) P \land ({P ↾}_{(1 \dots \|F\|)}) : (1 \dots \|F\|) \underset{1-1}{⟶} Vtx (G)) \to (Fun P \land P \in Fin \land (1 \dots \|F\|) \subseteq dom P)$
85		hashres	$⊢ (Fun P \land P \in Fin \land (1 \dots \|F\|) \subseteq dom P) \to \|{P ↾}_{(1 \dots \|F\|)}\| = \|(1 \dots \|F\|)\|$
86	84 85	syl	$⊢ (F Paths (G) P \land ({P ↾}_{(1 \dots \|F\|)}) : (1 \dots \|F\|) \underset{1-1}{⟶} Vtx (G)) \to \|{P ↾}_{(1 \dots \|F\|)}\| = \|(1 \dots \|F\|)\|$
87		ovexd	$⊢ (F Paths (G) P \land ({P ↾}_{(1 \dots \|F\|)}) : (1 \dots \|F\|) \underset{1-1}{⟶} Vtx (G)) \to (1 \dots \|F\|) \in V$
88		hashf1rn	$⊢ ((1 \dots \|F\|) \in V \land ({P ↾}_{(1 \dots \|F\|)}) : (1 \dots \|F\|) \underset{1-1}{⟶} Vtx (G)) \to \|{P ↾}_{(1 \dots \|F\|)}\| = \|ran ({P ↾}_{(1 \dots \|F\|)})\|$
89	87 88	sylancom	$⊢ (F Paths (G) P \land ({P ↾}_{(1 \dots \|F\|)}) : (1 \dots \|F\|) \underset{1-1}{⟶} Vtx (G)) \to \|{P ↾}_{(1 \dots \|F\|)}\| = \|ran ({P ↾}_{(1 \dots \|F\|)})\|$
90	2 5	syl	$⊢ F Paths (G) P \to \|F\| \in ℕ_{0}$
91		hashfz1	$⊢ \|F\| \in ℕ_{0} \to \|(1 \dots \|F\|)\| = \|F\|$
92	90 91	syl	$⊢ F Paths (G) P \to \|(1 \dots \|F\|)\| = \|F\|$
93	92	adantr	$⊢ (F Paths (G) P \land ({P ↾}_{(1 \dots \|F\|)}) : (1 \dots \|F\|) \underset{1-1}{⟶} Vtx (G)) \to \|(1 \dots \|F\|)\| = \|F\|$
94	86 89 93	3eqtr3d	$⊢ (F Paths (G) P \land ({P ↾}_{(1 \dots \|F\|)}) : (1 \dots \|F\|) \underset{1-1}{⟶} Vtx (G)) \to \|ran ({P ↾}_{(1 \dots \|F\|)})\| = \|F\|$
95	70 71 94	syl2anc2	$⊢ F Cycles (G) P \to \|ran ({P ↾}_{(1 \dots \|F\|)})\| = \|F\|$
96	95	adantl	$⊢ (1 \leq \|F\| \land F Cycles (G) P) \to \|ran ({P ↾}_{(1 \dots \|F\|)})\| = \|F\|$
97	69 96	eqtrd	$⊢ (1 \leq \|F\| \land F Cycles (G) P) \to \|ran P\| = \|F\|$

Metamath Proof Explorer

Theorem cyclnumvtx

Proof