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

Metamath Proof Explorer

Theorem cyclnumvtx

Proof