numclwwlk1lem2f1

Description: T is a 1-1 function. (Contributed by AV, 26-Sep-2018) (Revised by AV, 29-May-2021) (Proof shortened by AV, 23-Feb-2022) (Revised by AV, 31-Oct-2022)

	Ref	Expression
Hypotheses	extwwlkfab.v	$⊢ V = Vtx (G)$
	extwwlkfab.c	$⊢ C = (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) = v\})$
	extwwlkfab.f	$⊢ F = X ClWWalksNOn (G) (N - 2)$
	numclwwlk.t	$⊢ T = (u \in (X C N) ⟼ ⟨u prefix (N - 2), u (N - 1)⟩)$
Assertion	numclwwlk1lem2f1	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to T : X C N \underset{1-1}{⟶} F \times (G NeighbVtx X)$

Proof

Step	Hyp	Ref	Expression
1		extwwlkfab.v	$⊢ V = Vtx (G)$
2		extwwlkfab.c	$⊢ C = (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) = v\})$
3		extwwlkfab.f	$⊢ F = X ClWWalksNOn (G) (N - 2)$
4		numclwwlk.t	$⊢ T = (u \in (X C N) ⟼ ⟨u prefix (N - 2), u (N - 1)⟩)$
5	1 2 3 4	numclwwlk1lem2f	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to T : X C N ⟶ F \times (G NeighbVtx X)$
6	1 2 3 4	numclwwlk1lem2fv	$⊢ p \in (X C N) \to T (p) = ⟨p prefix (N - 2), p (N - 1)⟩$
7	6	ad2antrl	$⊢ ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land (p \in (X C N) \land a \in (X C N))) \to T (p) = ⟨p prefix (N - 2), p (N - 1)⟩$
8	1 2 3 4	numclwwlk1lem2fv	$⊢ a \in (X C N) \to T (a) = ⟨a prefix (N - 2), a (N - 1)⟩$
9	8	ad2antll	$⊢ ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land (p \in (X C N) \land a \in (X C N))) \to T (a) = ⟨a prefix (N - 2), a (N - 1)⟩$
10	7 9	eqeq12d	$⊢ ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land (p \in (X C N) \land a \in (X C N))) \to (T (p) = T (a) \leftrightarrow ⟨p prefix (N - 2), p (N - 1)⟩ = ⟨a prefix (N - 2), a (N - 1)⟩)$
11		ovex	$⊢ p prefix (N - 2) \in V$
12		fvex	$⊢ p (N - 1) \in V$
13	11 12	opth	$⊢ ⟨p prefix (N - 2), p (N - 1)⟩ = ⟨a prefix (N - 2), a (N - 1)⟩ \leftrightarrow (p prefix (N - 2) = a prefix (N - 2) \land p (N - 1) = a (N - 1))$
14		uzuzle23	$⊢ N \in ℤ_{\geq 3} \to N \in ℤ_{\geq 2}$
15	2	2clwwlkel	$⊢ (X \in V \land N \in ℤ_{\geq 2}) \to (p \in (X C N) \leftrightarrow (p \in (X ClWWalksNOn (G) N) \land p (N - 2) = X))$
16		isclwwlknon	$⊢ p \in (X ClWWalksNOn (G) N) \leftrightarrow (p \in (N ClWWalksN G) \land p (0) = X)$
17	16	anbi1i	$⊢ (p \in (X ClWWalksNOn (G) N) \land p (N - 2) = X) \leftrightarrow ((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X)$
18	15 17	bitrdi	$⊢ (X \in V \land N \in ℤ_{\geq 2}) \to (p \in (X C N) \leftrightarrow ((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X))$
19	2	2clwwlkel	$⊢ (X \in V \land N \in ℤ_{\geq 2}) \to (a \in (X C N) \leftrightarrow (a \in (X ClWWalksNOn (G) N) \land a (N - 2) = X))$
20		isclwwlknon	$⊢ a \in (X ClWWalksNOn (G) N) \leftrightarrow (a \in (N ClWWalksN G) \land a (0) = X)$
21	20	anbi1i	$⊢ (a \in (X ClWWalksNOn (G) N) \land a (N - 2) = X) \leftrightarrow ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)$
22	19 21	bitrdi	$⊢ (X \in V \land N \in ℤ_{\geq 2}) \to (a \in (X C N) \leftrightarrow ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X))$
23	18 22	anbi12d	$⊢ (X \in V \land N \in ℤ_{\geq 2}) \to ((p \in (X C N) \land a \in (X C N)) \leftrightarrow (((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)))$
24	14 23	sylan2	$⊢ (X \in V \land N \in ℤ_{\geq 3}) \to ((p \in (X C N) \land a \in (X C N)) \leftrightarrow (((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)))$
25	24	3adant1	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to ((p \in (X C N) \land a \in (X C N)) \leftrightarrow (((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)))$
26	1	clwwlknbp	$⊢ p \in (N ClWWalksN G) \to (p \in Word V \land \|p\| = N)$
27	26	adantr	$⊢ (p \in (N ClWWalksN G) \land p (0) = X) \to (p \in Word V \land \|p\| = N)$
28	27	adantr	$⊢ ((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \to (p \in Word V \land \|p\| = N)$
29		simpr	$⊢ (p \in (N ClWWalksN G) \land p (0) = X) \to p (0) = X$
30	29	adantr	$⊢ ((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \to p (0) = X$
31		simpr	$⊢ ((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \to p (N - 2) = X$
32	29	eqcomd	$⊢ (p \in (N ClWWalksN G) \land p (0) = X) \to X = p (0)$
33	32	adantr	$⊢ ((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \to X = p (0)$
34	31 33	eqtrd	$⊢ ((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \to p (N - 2) = p (0)$
35	28 30 34	jca32	$⊢ ((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \to ((p \in Word V \land \|p\| = N) \land (p (0) = X \land p (N - 2) = p (0)))$
36	1	clwwlknbp	$⊢ a \in (N ClWWalksN G) \to (a \in Word V \land \|a\| = N)$
37	36	adantr	$⊢ (a \in (N ClWWalksN G) \land a (0) = X) \to (a \in Word V \land \|a\| = N)$
38	37	adantr	$⊢ ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X) \to (a \in Word V \land \|a\| = N)$
39		simpr	$⊢ (a \in (N ClWWalksN G) \land a (0) = X) \to a (0) = X$
40	39	adantr	$⊢ ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X) \to a (0) = X$
41		simpr	$⊢ ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X) \to a (N - 2) = X$
42	39	eqcomd	$⊢ (a \in (N ClWWalksN G) \land a (0) = X) \to X = a (0)$
43	42	adantr	$⊢ ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X) \to X = a (0)$
44	41 43	eqtrd	$⊢ ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X) \to a (N - 2) = a (0)$
45	38 40 44	jca32	$⊢ ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X) \to ((a \in Word V \land \|a\| = N) \land (a (0) = X \land a (N - 2) = a (0)))$
46		eqtr3	$⊢ (\|p\| = N \land \|a\| = N) \to \|p\| = \|a\|$
47	46	expcom	$⊢ \|a\| = N \to (\|p\| = N \to \|p\| = \|a\|)$
48	47	ad2antlr	$⊢ ((a \in Word V \land \|a\| = N) \land (a (0) = X \land a (N - 2) = a (0))) \to (\|p\| = N \to \|p\| = \|a\|)$
49	48	com12	$⊢ \|p\| = N \to (((a \in Word V \land \|a\| = N) \land (a (0) = X \land a (N - 2) = a (0))) \to \|p\| = \|a\|)$
50	49	ad2antlr	$⊢ ((p \in Word V \land \|p\| = N) \land (p (0) = X \land p (N - 2) = p (0))) \to (((a \in Word V \land \|a\| = N) \land (a (0) = X \land a (N - 2) = a (0))) \to \|p\| = \|a\|)$
51	50	imp	$⊢ (((p \in Word V \land \|p\| = N) \land (p (0) = X \land p (N - 2) = p (0))) \land ((a \in Word V \land \|a\| = N) \land (a (0) = X \land a (N - 2) = a (0)))) \to \|p\| = \|a\|$
52	35 45 51	syl2an	$⊢ (((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)) \to \|p\| = \|a\|$
53	52	3ad2ant2	$⊢ (N \in ℤ_{\geq 3} \land (((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)) \land (p prefix (N - 2) = a prefix (N - 2) \land p (N - 1) = a (N - 1))) \to \|p\| = \|a\|$
54	27	simprd	$⊢ (p \in (N ClWWalksN G) \land p (0) = X) \to \|p\| = N$
55	54	adantr	$⊢ ((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \to \|p\| = N$
56	55	eqcomd	$⊢ ((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \to N = \|p\|$
57	56	adantr	$⊢ (((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)) \to N = \|p\|$
58	57	oveq1d	$⊢ (((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)) \to N - 2 = \|p\| - 2$
59	58	oveq2d	$⊢ (((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)) \to p prefix (N - 2) = p prefix (\|p\| - 2)$
60	58	oveq2d	$⊢ (((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)) \to a prefix (N - 2) = a prefix (\|p\| - 2)$
61	59 60	eqeq12d	$⊢ (((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)) \to (p prefix (N - 2) = a prefix (N - 2) \leftrightarrow p prefix (\|p\| - 2) = a prefix (\|p\| - 2))$
62	61	biimpcd	$⊢ p prefix (N - 2) = a prefix (N - 2) \to ((((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)) \to p prefix (\|p\| - 2) = a prefix (\|p\| - 2))$
63	62	adantr	$⊢ (p prefix (N - 2) = a prefix (N - 2) \land p (N - 1) = a (N - 1)) \to ((((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)) \to p prefix (\|p\| - 2) = a prefix (\|p\| - 2))$
64	63	impcom	$⊢ ((((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)) \land (p prefix (N - 2) = a prefix (N - 2) \land p (N - 1) = a (N - 1))) \to p prefix (\|p\| - 2) = a prefix (\|p\| - 2)$
65	55	oveq1d	$⊢ ((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \to \|p\| - 2 = N - 2$
66	65	fveq2d	$⊢ ((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \to p (\|p\| - 2) = p (N - 2)$
67	66 31	eqtrd	$⊢ ((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \to p (\|p\| - 2) = X$
68	67	adantr	$⊢ (((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)) \to p (\|p\| - 2) = X$
69	41	eqcomd	$⊢ ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X) \to X = a (N - 2)$
70	69	adantl	$⊢ (((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)) \to X = a (N - 2)$
71	58	fveq2d	$⊢ (((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)) \to a (N - 2) = a (\|p\| - 2)$
72	70 71	eqtrd	$⊢ (((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)) \to X = a (\|p\| - 2)$
73	68 72	eqtrd	$⊢ (((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)) \to p (\|p\| - 2) = a (\|p\| - 2)$
74	73	adantr	$⊢ ((((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)) \land (p prefix (N - 2) = a prefix (N - 2) \land p (N - 1) = a (N - 1))) \to p (\|p\| - 2) = a (\|p\| - 2)$
75		lsw	$⊢ p \in Word V \to lastS (p) = p (\|p\| - 1)$
76		fvoveq1	$⊢ \|p\| = N \to p (\|p\| - 1) = p (N - 1)$
77	75 76	sylan9eq	$⊢ (p \in Word V \land \|p\| = N) \to lastS (p) = p (N - 1)$
78	26 77	syl	$⊢ p \in (N ClWWalksN G) \to lastS (p) = p (N - 1)$
79	78	eqcomd	$⊢ p \in (N ClWWalksN G) \to p (N - 1) = lastS (p)$
80	79	ad3antrrr	$⊢ (((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)) \to p (N - 1) = lastS (p)$
81		lsw	$⊢ a \in Word V \to lastS (a) = a (\|a\| - 1)$
82	81	adantr	$⊢ (a \in Word V \land \|a\| = N) \to lastS (a) = a (\|a\| - 1)$
83		oveq1	$⊢ N = \|a\| \to N - 1 = \|a\| - 1$
84	83	eqcoms	$⊢ \|a\| = N \to N - 1 = \|a\| - 1$
85	84	fveq2d	$⊢ \|a\| = N \to a (N - 1) = a (\|a\| - 1)$
86	85	eqeq2d	$⊢ \|a\| = N \to (lastS (a) = a (N - 1) \leftrightarrow lastS (a) = a (\|a\| - 1))$
87	86	adantl	$⊢ (a \in Word V \land \|a\| = N) \to (lastS (a) = a (N - 1) \leftrightarrow lastS (a) = a (\|a\| - 1))$
88	82 87	mpbird	$⊢ (a \in Word V \land \|a\| = N) \to lastS (a) = a (N - 1)$
89	36 88	syl	$⊢ a \in (N ClWWalksN G) \to lastS (a) = a (N - 1)$
90	89	eqcomd	$⊢ a \in (N ClWWalksN G) \to a (N - 1) = lastS (a)$
91	90	adantr	$⊢ (a \in (N ClWWalksN G) \land a (0) = X) \to a (N - 1) = lastS (a)$
92	91	ad2antrl	$⊢ (((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)) \to a (N - 1) = lastS (a)$
93	80 92	eqeq12d	$⊢ (((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)) \to (p (N - 1) = a (N - 1) \leftrightarrow lastS (p) = lastS (a))$
94	93	biimpd	$⊢ (((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)) \to (p (N - 1) = a (N - 1) \to lastS (p) = lastS (a))$
95	94	adantld	$⊢ (((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)) \to ((p prefix (N - 2) = a prefix (N - 2) \land p (N - 1) = a (N - 1)) \to lastS (p) = lastS (a))$
96	95	imp	$⊢ ((((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)) \land (p prefix (N - 2) = a prefix (N - 2) \land p (N - 1) = a (N - 1))) \to lastS (p) = lastS (a)$
97	64 74 96	3jca	$⊢ ((((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)) \land (p prefix (N - 2) = a prefix (N - 2) \land p (N - 1) = a (N - 1))) \to (p prefix (\|p\| - 2) = a prefix (\|p\| - 2) \land p (\|p\| - 2) = a (\|p\| - 2) \land lastS (p) = lastS (a))$
98	97	3adant1	$⊢ (N \in ℤ_{\geq 3} \land (((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)) \land (p prefix (N - 2) = a prefix (N - 2) \land p (N - 1) = a (N - 1))) \to (p prefix (\|p\| - 2) = a prefix (\|p\| - 2) \land p (\|p\| - 2) = a (\|p\| - 2) \land lastS (p) = lastS (a))$
99	1	clwwlknwrd	$⊢ p \in (N ClWWalksN G) \to p \in Word V$
100	99	ad3antrrr	$⊢ (((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)) \to p \in Word V$
101	100	3ad2ant2	$⊢ (N \in ℤ_{\geq 3} \land (((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)) \land (p prefix (N - 2) = a prefix (N - 2) \land p (N - 1) = a (N - 1))) \to p \in Word V$
102	1	clwwlknwrd	$⊢ a \in (N ClWWalksN G) \to a \in Word V$
103	102	adantr	$⊢ (a \in (N ClWWalksN G) \land a (0) = X) \to a \in Word V$
104	103	ad2antrl	$⊢ (((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)) \to a \in Word V$
105	104	3ad2ant2	$⊢ (N \in ℤ_{\geq 3} \land (((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)) \land (p prefix (N - 2) = a prefix (N - 2) \land p (N - 1) = a (N - 1))) \to a \in Word V$
106		clwwlknlen	$⊢ p \in (N ClWWalksN G) \to \|p\| = N$
107		eluz2b1	$⊢ N \in ℤ_{\geq 2} \leftrightarrow (N \in ℤ \land 1 < N)$
108		breq2	$⊢ N = \|p\| \to (1 < N \leftrightarrow 1 < \|p\|)$
109	108	eqcoms	$⊢ \|p\| = N \to (1 < N \leftrightarrow 1 < \|p\|)$
110	109	biimpcd	$⊢ 1 < N \to (\|p\| = N \to 1 < \|p\|)$
111	107 110	simplbiim	$⊢ N \in ℤ_{\geq 2} \to (\|p\| = N \to 1 < \|p\|)$
112	14 106 111	syl2imc	$⊢ p \in (N ClWWalksN G) \to (N \in ℤ_{\geq 3} \to 1 < \|p\|)$
113	112	ad3antrrr	$⊢ (((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)) \to (N \in ℤ_{\geq 3} \to 1 < \|p\|)$
114	113	impcom	$⊢ (N \in ℤ_{\geq 3} \land (((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X))) \to 1 < \|p\|$
115	114	3adant3	$⊢ (N \in ℤ_{\geq 3} \land (((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)) \land (p prefix (N - 2) = a prefix (N - 2) \land p (N - 1) = a (N - 1))) \to 1 < \|p\|$
116		2swrd2eqwrdeq	$⊢ (p \in Word V \land a \in Word V \land 1 < \|p\|) \to (p = a \leftrightarrow (\|p\| = \|a\| \land (p prefix (\|p\| - 2) = a prefix (\|p\| - 2) \land p (\|p\| - 2) = a (\|p\| - 2) \land lastS (p) = lastS (a))))$
117	101 105 115 116	syl3anc	$⊢ (N \in ℤ_{\geq 3} \land (((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)) \land (p prefix (N - 2) = a prefix (N - 2) \land p (N - 1) = a (N - 1))) \to (p = a \leftrightarrow (\|p\| = \|a\| \land (p prefix (\|p\| - 2) = a prefix (\|p\| - 2) \land p (\|p\| - 2) = a (\|p\| - 2) \land lastS (p) = lastS (a))))$
118	53 98 117	mpbir2and	$⊢ (N \in ℤ_{\geq 3} \land (((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)) \land (p prefix (N - 2) = a prefix (N - 2) \land p (N - 1) = a (N - 1))) \to p = a$
119	118	3exp	$⊢ N \in ℤ_{\geq 3} \to ((((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)) \to ((p prefix (N - 2) = a prefix (N - 2) \land p (N - 1) = a (N - 1)) \to p = a))$
120	119	3ad2ant3	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to ((((p \in (N ClWWalksN G) \land p (0) = X) \land p (N - 2) = X) \land ((a \in (N ClWWalksN G) \land a (0) = X) \land a (N - 2) = X)) \to ((p prefix (N - 2) = a prefix (N - 2) \land p (N - 1) = a (N - 1)) \to p = a))$
121	25 120	sylbid	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to ((p \in (X C N) \land a \in (X C N)) \to ((p prefix (N - 2) = a prefix (N - 2) \land p (N - 1) = a (N - 1)) \to p = a))$
122	121	imp	$⊢ ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land (p \in (X C N) \land a \in (X C N))) \to ((p prefix (N - 2) = a prefix (N - 2) \land p (N - 1) = a (N - 1)) \to p = a)$
123	13 122	syl5bi	$⊢ ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land (p \in (X C N) \land a \in (X C N))) \to (⟨p prefix (N - 2), p (N - 1)⟩ = ⟨a prefix (N - 2), a (N - 1)⟩ \to p = a)$
124	10 123	sylbid	$⊢ ((G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \land (p \in (X C N) \land a \in (X C N))) \to (T (p) = T (a) \to p = a)$
125	124	ralrimivva	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to \forall p \in (X C N) \forall a \in (X C N) (T (p) = T (a) \to p = a)$
126		dff13	$⊢ T : X C N \underset{1-1}{⟶} F \times (G NeighbVtx X) \leftrightarrow (T : X C N ⟶ F \times (G NeighbVtx X) \land \forall p \in (X C N) \forall a \in (X C N) (T (p) = T (a) \to p = a))$
127	5 125 126	sylanbrc	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to T : X C N \underset{1-1}{⟶} F \times (G NeighbVtx X)$

Metamath Proof Explorer

Theorem numclwwlk1lem2f1

Proof