numclwlk2lem2f1o

Description: R is a 1-1 onto function. (Contributed by Alexander van der Vekens, 6-Oct-2018) (Revised by AV, 21-Jan-2022) (Proof shortened by AV, 17-Mar-2022) (Revised by AV, 1-Nov-2022)

	Ref	Expression
Hypotheses	numclwwlk.v	$⊢ V = Vtx (G)$
	numclwwlk.q	$⊢ Q = (v \in V, n \in ℕ ⟼ \{w \in (n WWalksN G) \| (w (0) = v \land lastS (w) \neq v)\})$
	numclwwlk.h	$⊢ H = (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) \neq v\})$
	numclwwlk.r	$⊢ R = (x \in (X H (N + 2)) ⟼ x prefix (N + 1))$
Assertion	numclwlk2lem2f1o	$⊢ (G \in FriendGraph \land X \in V \land N \in ℕ) \to R : X H (N + 2) \underset{1-1 onto}{⟶} X Q N$

Proof

Step	Hyp	Ref	Expression
1		numclwwlk.v	$⊢ V = Vtx (G)$
2		numclwwlk.q	$⊢ Q = (v \in V, n \in ℕ ⟼ \{w \in (n WWalksN G) \| (w (0) = v \land lastS (w) \neq v)\})$
3		numclwwlk.h	$⊢ H = (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) \neq v\})$
4		numclwwlk.r	$⊢ R = (x \in (X H (N + 2)) ⟼ x prefix (N + 1))$
5		eleq1w	$⊢ y = x \to (y \in (X H (N + 2)) \leftrightarrow x \in (X H (N + 2)))$
6		fveq2	$⊢ y = x \to R (y) = R (x)$
7		oveq1	$⊢ y = x \to y prefix (N + 1) = x prefix (N + 1)$
8	6 7	eqeq12d	$⊢ y = x \to (R (y) = y prefix (N + 1) \leftrightarrow R (x) = x prefix (N + 1))$
9	5 8	imbi12d	$⊢ y = x \to ((y \in (X H (N + 2)) \to R (y) = y prefix (N + 1)) \leftrightarrow (x \in (X H (N + 2)) \to R (x) = x prefix (N + 1)))$
10	9	imbi2d	$⊢ y = x \to (((X \in V \land N \in ℕ) \to (y \in (X H (N + 2)) \to R (y) = y prefix (N + 1))) \leftrightarrow ((X \in V \land N \in ℕ) \to (x \in (X H (N + 2)) \to R (x) = x prefix (N + 1))))$
11	1 2 3 4	numclwlk2lem2fv	$⊢ (X \in V \land N \in ℕ) \to (y \in (X H (N + 2)) \to R (y) = y prefix (N + 1))$
12	10 11	chvarvv	$⊢ (X \in V \land N \in ℕ) \to (x \in (X H (N + 2)) \to R (x) = x prefix (N + 1))$
13	12	3adant1	$⊢ (G \in FriendGraph \land X \in V \land N \in ℕ) \to (x \in (X H (N + 2)) \to R (x) = x prefix (N + 1))$
14	13	imp	$⊢ ((G \in FriendGraph \land X \in V \land N \in ℕ) \land x \in (X H (N + 2))) \to R (x) = x prefix (N + 1)$
15	1 2 3 4	numclwlk2lem2f	$⊢ (G \in FriendGraph \land X \in V \land N \in ℕ) \to R : X H (N + 2) ⟶ X Q N$
16	15	ffvelcdmda	$⊢ ((G \in FriendGraph \land X \in V \land N \in ℕ) \land x \in (X H (N + 2))) \to R (x) \in (X Q N)$
17	14 16	eqeltrrd	$⊢ ((G \in FriendGraph \land X \in V \land N \in ℕ) \land x \in (X H (N + 2))) \to x prefix (N + 1) \in (X Q N)$
18	17	ralrimiva	$⊢ (G \in FriendGraph \land X \in V \land N \in ℕ) \to \forall x \in (X H (N + 2)) x prefix (N + 1) \in (X Q N)$
19	1 2 3	numclwwlk2lem1	$⊢ (G \in FriendGraph \land X \in V \land N \in ℕ) \to (u \in (X Q N) \to \exists! v \in V u ++ ⟨“ v ”⟩ \in (X H (N + 2)))$
20	19	imp	$⊢ ((G \in FriendGraph \land X \in V \land N \in ℕ) \land u \in (X Q N)) \to \exists! v \in V u ++ ⟨“ v ”⟩ \in (X H (N + 2))$
21	1 2	numclwwlkovq	$⊢ (X \in V \land N \in ℕ) \to X Q N = \{w \in (N WWalksN G) \| (w (0) = X \land lastS (w) \neq X)\}$
22	21	eleq2d	$⊢ (X \in V \land N \in ℕ) \to (u \in (X Q N) \leftrightarrow u \in \{w \in (N WWalksN G) \| (w (0) = X \land lastS (w) \neq X)\})$
23	22	3adant1	$⊢ (G \in FriendGraph \land X \in V \land N \in ℕ) \to (u \in (X Q N) \leftrightarrow u \in \{w \in (N WWalksN G) \| (w (0) = X \land lastS (w) \neq X)\})$
24		fveq1	$⊢ w = u \to w (0) = u (0)$
25	24	eqeq1d	$⊢ w = u \to (w (0) = X \leftrightarrow u (0) = X)$
26		fveq2	$⊢ w = u \to lastS (w) = lastS (u)$
27	26	neeq1d	$⊢ w = u \to (lastS (w) \neq X \leftrightarrow lastS (u) \neq X)$
28	25 27	anbi12d	$⊢ w = u \to ((w (0) = X \land lastS (w) \neq X) \leftrightarrow (u (0) = X \land lastS (u) \neq X))$
29	28	elrab	$⊢ u \in \{w \in (N WWalksN G) \| (w (0) = X \land lastS (w) \neq X)\} \leftrightarrow (u \in (N WWalksN G) \land (u (0) = X \land lastS (u) \neq X))$
30	23 29	bitrdi	$⊢ (G \in FriendGraph \land X \in V \land N \in ℕ) \to (u \in (X Q N) \leftrightarrow (u \in (N WWalksN G) \land (u (0) = X \land lastS (u) \neq X)))$
31		wwlknbp1	$⊢ u \in (N WWalksN G) \to (N \in ℕ_{0} \land u \in Word Vtx (G) \land \|u\| = N + 1)$
32		3simpc	$⊢ (N \in ℕ_{0} \land u \in Word Vtx (G) \land \|u\| = N + 1) \to (u \in Word Vtx (G) \land \|u\| = N + 1)$
33	31 32	syl	$⊢ u \in (N WWalksN G) \to (u \in Word Vtx (G) \land \|u\| = N + 1)$
34	1	wrdeqi	$⊢ Word V = Word Vtx (G)$
35	34	eleq2i	$⊢ u \in Word V \leftrightarrow u \in Word Vtx (G)$
36	35	anbi1i	$⊢ (u \in Word V \land \|u\| = N + 1) \leftrightarrow (u \in Word Vtx (G) \land \|u\| = N + 1)$
37	33 36	sylibr	$⊢ u \in (N WWalksN G) \to (u \in Word V \land \|u\| = N + 1)$
38		simpll	$⊢ ((u \in Word V \land \|u\| = N + 1) \land (G \in FriendGraph \land X \in V \land N \in ℕ)) \to u \in Word V$
39		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
40		2nn	$⊢ 2 \in ℕ$
41	40	a1i	$⊢ N \in ℕ \to 2 \in ℕ$
42	41	nnzd	$⊢ N \in ℕ \to 2 \in ℤ$
43		nn0pzuz	$⊢ (N \in ℕ_{0} \land 2 \in ℤ) \to N + 2 \in ℤ_{\geq 2}$
44	39 42 43	syl2anc	$⊢ N \in ℕ \to N + 2 \in ℤ_{\geq 2}$
45	3	numclwwlkovh	$⊢ (X \in V \land N + 2 \in ℤ_{\geq 2}) \to X H (N + 2) = \{w \in ((N + 2) ClWWalksN G) \| (w (0) = X \land w (N + 2 - 2) \neq w (0))\}$
46	44 45	sylan2	$⊢ (X \in V \land N \in ℕ) \to X H (N + 2) = \{w \in ((N + 2) ClWWalksN G) \| (w (0) = X \land w (N + 2 - 2) \neq w (0))\}$
47	46	eleq2d	$⊢ (X \in V \land N \in ℕ) \to (x \in (X H (N + 2)) \leftrightarrow x \in \{w \in ((N + 2) ClWWalksN G) \| (w (0) = X \land w (N + 2 - 2) \neq w (0))\})$
48		fveq1	$⊢ w = x \to w (0) = x (0)$
49	48	eqeq1d	$⊢ w = x \to (w (0) = X \leftrightarrow x (0) = X)$
50		fveq1	$⊢ w = x \to w (N + 2 - 2) = x (N + 2 - 2)$
51	50 48	neeq12d	$⊢ w = x \to (w (N + 2 - 2) \neq w (0) \leftrightarrow x (N + 2 - 2) \neq x (0))$
52	49 51	anbi12d	$⊢ w = x \to ((w (0) = X \land w (N + 2 - 2) \neq w (0)) \leftrightarrow (x (0) = X \land x (N + 2 - 2) \neq x (0)))$
53	52	elrab	$⊢ x \in \{w \in ((N + 2) ClWWalksN G) \| (w (0) = X \land w (N + 2 - 2) \neq w (0))\} \leftrightarrow (x \in ((N + 2) ClWWalksN G) \land (x (0) = X \land x (N + 2 - 2) \neq x (0)))$
54	47 53	bitrdi	$⊢ (X \in V \land N \in ℕ) \to (x \in (X H (N + 2)) \leftrightarrow (x \in ((N + 2) ClWWalksN G) \land (x (0) = X \land x (N + 2 - 2) \neq x (0))))$
55	54	3adant1	$⊢ (G \in FriendGraph \land X \in V \land N \in ℕ) \to (x \in (X H (N + 2)) \leftrightarrow (x \in ((N + 2) ClWWalksN G) \land (x (0) = X \land x (N + 2 - 2) \neq x (0))))$
56	55	adantl	$⊢ ((u \in Word V \land \|u\| = N + 1) \land (G \in FriendGraph \land X \in V \land N \in ℕ)) \to (x \in (X H (N + 2)) \leftrightarrow (x \in ((N + 2) ClWWalksN G) \land (x (0) = X \land x (N + 2 - 2) \neq x (0))))$
57	1	clwwlknbp	$⊢ x \in ((N + 2) ClWWalksN G) \to (x \in Word V \land \|x\| = N + 2)$
58		lencl	$⊢ u \in Word V \to \|u\| \in ℕ_{0}$
59		simprr	$⊢ (((\|u\| \in ℕ_{0} \land \|u\| = N + 1) \land N \in ℕ) \land (\|x\| = N + 2 \land x \in Word V)) \to x \in Word V$
60		df-2	$⊢ 2 = 1 + 1$
61	60	a1i	$⊢ N \in ℕ \to 2 = 1 + 1$
62	61	oveq2d	$⊢ N \in ℕ \to N + 2 = N + 1 + 1$
63		nncn	$⊢ N \in ℕ \to N \in ℂ$
64		1cnd	$⊢ N \in ℕ \to 1 \in ℂ$
65	63 64 64	addassd	$⊢ N \in ℕ \to N + 1 + 1 = N + 1 + 1$
66	62 65	eqtr4d	$⊢ N \in ℕ \to N + 2 = N + 1 + 1$
67	66	adantl	$⊢ ((\|u\| \in ℕ_{0} \land \|u\| = N + 1) \land N \in ℕ) \to N + 2 = N + 1 + 1$
68	67	eqeq2d	$⊢ ((\|u\| \in ℕ_{0} \land \|u\| = N + 1) \land N \in ℕ) \to (\|x\| = N + 2 \leftrightarrow \|x\| = N + 1 + 1)$
69	68	biimpcd	$⊢ \|x\| = N + 2 \to (((\|u\| \in ℕ_{0} \land \|u\| = N + 1) \land N \in ℕ) \to \|x\| = N + 1 + 1)$
70	69	adantr	$⊢ (\|x\| = N + 2 \land x \in Word V) \to (((\|u\| \in ℕ_{0} \land \|u\| = N + 1) \land N \in ℕ) \to \|x\| = N + 1 + 1)$
71	70	impcom	$⊢ (((\|u\| \in ℕ_{0} \land \|u\| = N + 1) \land N \in ℕ) \land (\|x\| = N + 2 \land x \in Word V)) \to \|x\| = N + 1 + 1$
72		oveq1	$⊢ \|u\| = N + 1 \to \|u\| + 1 = N + 1 + 1$
73	72	ad3antlr	$⊢ (((\|u\| \in ℕ_{0} \land \|u\| = N + 1) \land N \in ℕ) \land (\|x\| = N + 2 \land x \in Word V)) \to \|u\| + 1 = N + 1 + 1$
74	71 73	eqtr4d	$⊢ (((\|u\| \in ℕ_{0} \land \|u\| = N + 1) \land N \in ℕ) \land (\|x\| = N + 2 \land x \in Word V)) \to \|x\| = \|u\| + 1$
75	59 74	jca	$⊢ (((\|u\| \in ℕ_{0} \land \|u\| = N + 1) \land N \in ℕ) \land (\|x\| = N + 2 \land x \in Word V)) \to (x \in Word V \land \|x\| = \|u\| + 1)$
76	75	exp31	$⊢ (\|u\| \in ℕ_{0} \land \|u\| = N + 1) \to (N \in ℕ \to ((\|x\| = N + 2 \land x \in Word V) \to (x \in Word V \land \|x\| = \|u\| + 1)))$
77	58 76	sylan	$⊢ (u \in Word V \land \|u\| = N + 1) \to (N \in ℕ \to ((\|x\| = N + 2 \land x \in Word V) \to (x \in Word V \land \|x\| = \|u\| + 1)))$
78	77	com12	$⊢ N \in ℕ \to ((u \in Word V \land \|u\| = N + 1) \to ((\|x\| = N + 2 \land x \in Word V) \to (x \in Word V \land \|x\| = \|u\| + 1)))$
79	78	3ad2ant3	$⊢ (G \in FriendGraph \land X \in V \land N \in ℕ) \to ((u \in Word V \land \|u\| = N + 1) \to ((\|x\| = N + 2 \land x \in Word V) \to (x \in Word V \land \|x\| = \|u\| + 1)))$
80	79	impcom	$⊢ ((u \in Word V \land \|u\| = N + 1) \land (G \in FriendGraph \land X \in V \land N \in ℕ)) \to ((\|x\| = N + 2 \land x \in Word V) \to (x \in Word V \land \|x\| = \|u\| + 1))$
81	80	com12	$⊢ (\|x\| = N + 2 \land x \in Word V) \to (((u \in Word V \land \|u\| = N + 1) \land (G \in FriendGraph \land X \in V \land N \in ℕ)) \to (x \in Word V \land \|x\| = \|u\| + 1))$
82	81	ancoms	$⊢ (x \in Word V \land \|x\| = N + 2) \to (((u \in Word V \land \|u\| = N + 1) \land (G \in FriendGraph \land X \in V \land N \in ℕ)) \to (x \in Word V \land \|x\| = \|u\| + 1))$
83	57 82	syl	$⊢ x \in ((N + 2) ClWWalksN G) \to (((u \in Word V \land \|u\| = N + 1) \land (G \in FriendGraph \land X \in V \land N \in ℕ)) \to (x \in Word V \land \|x\| = \|u\| + 1))$
84	83	adantr	$⊢ (x \in ((N + 2) ClWWalksN G) \land (x (0) = X \land x (N + 2 - 2) \neq x (0))) \to (((u \in Word V \land \|u\| = N + 1) \land (G \in FriendGraph \land X \in V \land N \in ℕ)) \to (x \in Word V \land \|x\| = \|u\| + 1))$
85	84	com12	$⊢ ((u \in Word V \land \|u\| = N + 1) \land (G \in FriendGraph \land X \in V \land N \in ℕ)) \to ((x \in ((N + 2) ClWWalksN G) \land (x (0) = X \land x (N + 2 - 2) \neq x (0))) \to (x \in Word V \land \|x\| = \|u\| + 1))$
86	56 85	sylbid	$⊢ ((u \in Word V \land \|u\| = N + 1) \land (G \in FriendGraph \land X \in V \land N \in ℕ)) \to (x \in (X H (N + 2)) \to (x \in Word V \land \|x\| = \|u\| + 1))$
87	86	ralrimiv	$⊢ ((u \in Word V \land \|u\| = N + 1) \land (G \in FriendGraph \land X \in V \land N \in ℕ)) \to \forall x \in (X H (N + 2)) (x \in Word V \land \|x\| = \|u\| + 1)$
88	38 87	jca	$⊢ ((u \in Word V \land \|u\| = N + 1) \land (G \in FriendGraph \land X \in V \land N \in ℕ)) \to (u \in Word V \land \forall x \in (X H (N + 2)) (x \in Word V \land \|x\| = \|u\| + 1))$
89	88	ex	$⊢ (u \in Word V \land \|u\| = N + 1) \to ((G \in FriendGraph \land X \in V \land N \in ℕ) \to (u \in Word V \land \forall x \in (X H (N + 2)) (x \in Word V \land \|x\| = \|u\| + 1)))$
90	37 89	syl	$⊢ u \in (N WWalksN G) \to ((G \in FriendGraph \land X \in V \land N \in ℕ) \to (u \in Word V \land \forall x \in (X H (N + 2)) (x \in Word V \land \|x\| = \|u\| + 1)))$
91	90	adantr	$⊢ (u \in (N WWalksN G) \land (u (0) = X \land lastS (u) \neq X)) \to ((G \in FriendGraph \land X \in V \land N \in ℕ) \to (u \in Word V \land \forall x \in (X H (N + 2)) (x \in Word V \land \|x\| = \|u\| + 1)))$
92	91	imp	$⊢ ((u \in (N WWalksN G) \land (u (0) = X \land lastS (u) \neq X)) \land (G \in FriendGraph \land X \in V \land N \in ℕ)) \to (u \in Word V \land \forall x \in (X H (N + 2)) (x \in Word V \land \|x\| = \|u\| + 1))$
93		nfcv	$⊢ \underline{Ⅎ} v X$
94		nfmpo1	$⊢ \underline{Ⅎ} v (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) \neq v\})$
95	3 94	nfcxfr	$⊢ \underline{Ⅎ} v H$
96		nfcv	$⊢ \underline{Ⅎ} v (N + 2)$
97	93 95 96	nfov	$⊢ \underline{Ⅎ} v (X H (N + 2))$
98	97	reuccatpfxs1	$⊢ (u \in Word V \land \forall x \in (X H (N + 2)) (x \in Word V \land \|x\| = \|u\| + 1)) \to (\exists! v \in V u ++ ⟨“ v ”⟩ \in (X H (N + 2)) \to \exists! x \in (X H (N + 2)) u = x prefix \|u\|)$
99	92 98	syl	$⊢ ((u \in (N WWalksN G) \land (u (0) = X \land lastS (u) \neq X)) \land (G \in FriendGraph \land X \in V \land N \in ℕ)) \to (\exists! v \in V u ++ ⟨“ v ”⟩ \in (X H (N + 2)) \to \exists! x \in (X H (N + 2)) u = x prefix \|u\|)$
100	99	imp	$⊢ (((u \in (N WWalksN G) \land (u (0) = X \land lastS (u) \neq X)) \land (G \in FriendGraph \land X \in V \land N \in ℕ)) \land \exists! v \in V u ++ ⟨“ v ”⟩ \in (X H (N + 2))) \to \exists! x \in (X H (N + 2)) u = x prefix \|u\|$
101	31	simp3d	$⊢ u \in (N WWalksN G) \to \|u\| = N + 1$
102	101	eqcomd	$⊢ u \in (N WWalksN G) \to N + 1 = \|u\|$
103	102	ad4antr	$⊢ ((((u \in (N WWalksN G) \land (u (0) = X \land lastS (u) \neq X)) \land (G \in FriendGraph \land X \in V \land N \in ℕ)) \land \exists! v \in V u ++ ⟨“ v ”⟩ \in (X H (N + 2))) \land x \in (X H (N + 2))) \to N + 1 = \|u\|$
104	103	oveq2d	$⊢ ((((u \in (N WWalksN G) \land (u (0) = X \land lastS (u) \neq X)) \land (G \in FriendGraph \land X \in V \land N \in ℕ)) \land \exists! v \in V u ++ ⟨“ v ”⟩ \in (X H (N + 2))) \land x \in (X H (N + 2))) \to x prefix (N + 1) = x prefix \|u\|$
105	104	eqeq2d	$⊢ ((((u \in (N WWalksN G) \land (u (0) = X \land lastS (u) \neq X)) \land (G \in FriendGraph \land X \in V \land N \in ℕ)) \land \exists! v \in V u ++ ⟨“ v ”⟩ \in (X H (N + 2))) \land x \in (X H (N + 2))) \to (u = x prefix (N + 1) \leftrightarrow u = x prefix \|u\|)$
106	105	reubidva	$⊢ (((u \in (N WWalksN G) \land (u (0) = X \land lastS (u) \neq X)) \land (G \in FriendGraph \land X \in V \land N \in ℕ)) \land \exists! v \in V u ++ ⟨“ v ”⟩ \in (X H (N + 2))) \to (\exists! x \in (X H (N + 2)) u = x prefix (N + 1) \leftrightarrow \exists! x \in (X H (N + 2)) u = x prefix \|u\|)$
107	100 106	mpbird	$⊢ (((u \in (N WWalksN G) \land (u (0) = X \land lastS (u) \neq X)) \land (G \in FriendGraph \land X \in V \land N \in ℕ)) \land \exists! v \in V u ++ ⟨“ v ”⟩ \in (X H (N + 2))) \to \exists! x \in (X H (N + 2)) u = x prefix (N + 1)$
108	107	exp31	$⊢ (u \in (N WWalksN G) \land (u (0) = X \land lastS (u) \neq X)) \to ((G \in FriendGraph \land X \in V \land N \in ℕ) \to (\exists! v \in V u ++ ⟨“ v ”⟩ \in (X H (N + 2)) \to \exists! x \in (X H (N + 2)) u = x prefix (N + 1)))$
109	108	com12	$⊢ (G \in FriendGraph \land X \in V \land N \in ℕ) \to ((u \in (N WWalksN G) \land (u (0) = X \land lastS (u) \neq X)) \to (\exists! v \in V u ++ ⟨“ v ”⟩ \in (X H (N + 2)) \to \exists! x \in (X H (N + 2)) u = x prefix (N + 1)))$
110	30 109	sylbid	$⊢ (G \in FriendGraph \land X \in V \land N \in ℕ) \to (u \in (X Q N) \to (\exists! v \in V u ++ ⟨“ v ”⟩ \in (X H (N + 2)) \to \exists! x \in (X H (N + 2)) u = x prefix (N + 1)))$
111	110	imp	$⊢ ((G \in FriendGraph \land X \in V \land N \in ℕ) \land u \in (X Q N)) \to (\exists! v \in V u ++ ⟨“ v ”⟩ \in (X H (N + 2)) \to \exists! x \in (X H (N + 2)) u = x prefix (N + 1))$
112	20 111	mpd	$⊢ ((G \in FriendGraph \land X \in V \land N \in ℕ) \land u \in (X Q N)) \to \exists! x \in (X H (N + 2)) u = x prefix (N + 1)$
113	112	ralrimiva	$⊢ (G \in FriendGraph \land X \in V \land N \in ℕ) \to \forall u \in (X Q N) \exists! x \in (X H (N + 2)) u = x prefix (N + 1)$
114	4	f1ompt	$⊢ R : X H (N + 2) \underset{1-1 onto}{⟶} X Q N \leftrightarrow (\forall x \in (X H (N + 2)) x prefix (N + 1) \in (X Q N) \land \forall u \in (X Q N) \exists! x \in (X H (N + 2)) u = x prefix (N + 1))$
115	18 113 114	sylanbrc	$⊢ (G \in FriendGraph \land X \in V \land N \in ℕ) \to R : X H (N + 2) \underset{1-1 onto}{⟶} X Q N$

Metamath Proof Explorer

Theorem numclwlk2lem2f1o

Proof