clwwlkf1

Description: Lemma 3 for clwwlkf1o : F is a 1-1 function. (Contributed by AV, 28-Sep-2018) (Revised by AV, 26-Apr-2021) (Revised by AV, 1-Nov-2022)

	Ref	Expression
Hypotheses	clwwlkf1o.d	$⊢ D = \{w \in (N WWalksN G) \| lastS (w) = w (0)\}$
	clwwlkf1o.f	$⊢ F = (t \in D ⟼ t prefix N)$
Assertion	clwwlkf1	$⊢ N \in ℕ \to F : D \underset{1-1}{⟶} N ClWWalksN G$

Proof

Step	Hyp	Ref	Expression
1		clwwlkf1o.d	$⊢ D = \{w \in (N WWalksN G) \| lastS (w) = w (0)\}$
2		clwwlkf1o.f	$⊢ F = (t \in D ⟼ t prefix N)$
3	1 2	clwwlkf	$⊢ N \in ℕ \to F : D ⟶ N ClWWalksN G$
4	1 2	clwwlkfv	$⊢ x \in D \to F (x) = x prefix N$
5	1 2	clwwlkfv	$⊢ y \in D \to F (y) = y prefix N$
6	4 5	eqeqan12d	$⊢ (x \in D \land y \in D) \to (F (x) = F (y) \leftrightarrow x prefix N = y prefix N)$
7	6	adantl	$⊢ (N \in ℕ \land (x \in D \land y \in D)) \to (F (x) = F (y) \leftrightarrow x prefix N = y prefix N)$
8		fveq2	$⊢ w = x \to lastS (w) = lastS (x)$
9		fveq1	$⊢ w = x \to w (0) = x (0)$
10	8 9	eqeq12d	$⊢ w = x \to (lastS (w) = w (0) \leftrightarrow lastS (x) = x (0))$
11	10 1	elrab2	$⊢ x \in D \leftrightarrow (x \in (N WWalksN G) \land lastS (x) = x (0))$
12		fveq2	$⊢ w = y \to lastS (w) = lastS (y)$
13		fveq1	$⊢ w = y \to w (0) = y (0)$
14	12 13	eqeq12d	$⊢ w = y \to (lastS (w) = w (0) \leftrightarrow lastS (y) = y (0))$
15	14 1	elrab2	$⊢ y \in D \leftrightarrow (y \in (N WWalksN G) \land lastS (y) = y (0))$
16	11 15	anbi12i	$⊢ (x \in D \land y \in D) \leftrightarrow ((x \in (N WWalksN G) \land lastS (x) = x (0)) \land (y \in (N WWalksN G) \land lastS (y) = y (0)))$
17		eqid	$⊢ Vtx (G) = Vtx (G)$
18		eqid	$⊢ Edg (G) = Edg (G)$
19	17 18	wwlknp	$⊢ x \in (N WWalksN G) \to (x \in Word Vtx (G) \land \|x\| = N + 1 \land \forall i \in (0 ..^N) \{x (i), x (i + 1)\} \in Edg (G))$
20	17 18	wwlknp	$⊢ y \in (N WWalksN G) \to (y \in Word Vtx (G) \land \|y\| = N + 1 \land \forall i \in (0 ..^N) \{y (i), y (i + 1)\} \in Edg (G))$
21		simprlr	$⊢ (((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \land ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0))) \to \|x\| = N + 1$
22		simpllr	$⊢ (((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \land ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0))) \to \|y\| = N + 1$
23	21 22	eqtr4d	$⊢ (((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \land ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0))) \to \|x\| = \|y\|$
24	23	ad2antlr	$⊢ ((N \in ℕ \land (((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \land ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0)))) \land x prefix N = y prefix N) \to \|x\| = \|y\|$
25		nncn	$⊢ N \in ℕ \to N \in ℂ$
26		ax-1cn	$⊢ 1 \in ℂ$
27		pncan	$⊢ (N \in ℂ \land 1 \in ℂ) \to N + 1 - 1 = N$
28	27	eqcomd	$⊢ (N \in ℂ \land 1 \in ℂ) \to N = N + 1 - 1$
29	25 26 28	sylancl	$⊢ N \in ℕ \to N = N + 1 - 1$
30		oveq1	$⊢ \|x\| = N + 1 \to \|x\| - 1 = N + 1 - 1$
31	30	eqcomd	$⊢ \|x\| = N + 1 \to N + 1 - 1 = \|x\| - 1$
32	29 31	sylan9eqr	$⊢ (\|x\| = N + 1 \land N \in ℕ) \to N = \|x\| - 1$
33	32	oveq2d	$⊢ (\|x\| = N + 1 \land N \in ℕ) \to x prefix N = x prefix (\|x\| - 1)$
34	32	oveq2d	$⊢ (\|x\| = N + 1 \land N \in ℕ) \to y prefix N = y prefix (\|x\| - 1)$
35	33 34	eqeq12d	$⊢ (\|x\| = N + 1 \land N \in ℕ) \to (x prefix N = y prefix N \leftrightarrow x prefix (\|x\| - 1) = y prefix (\|x\| - 1))$
36	35	ex	$⊢ \|x\| = N + 1 \to (N \in ℕ \to (x prefix N = y prefix N \leftrightarrow x prefix (\|x\| - 1) = y prefix (\|x\| - 1)))$
37	36	ad2antlr	$⊢ ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0)) \to (N \in ℕ \to (x prefix N = y prefix N \leftrightarrow x prefix (\|x\| - 1) = y prefix (\|x\| - 1)))$
38	37	adantl	$⊢ (((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \land ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0))) \to (N \in ℕ \to (x prefix N = y prefix N \leftrightarrow x prefix (\|x\| - 1) = y prefix (\|x\| - 1)))$
39	38	impcom	$⊢ (N \in ℕ \land (((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \land ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0)))) \to (x prefix N = y prefix N \leftrightarrow x prefix (\|x\| - 1) = y prefix (\|x\| - 1))$
40	39	biimpa	$⊢ ((N \in ℕ \land (((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \land ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0)))) \land x prefix N = y prefix N) \to x prefix (\|x\| - 1) = y prefix (\|x\| - 1)$
41		simpll	$⊢ ((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \to y \in Word Vtx (G)$
42		simpll	$⊢ ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0)) \to x \in Word Vtx (G)$
43	41 42	anim12ci	$⊢ (((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \land ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0))) \to (x \in Word Vtx (G) \land y \in Word Vtx (G))$
44	43	adantl	$⊢ (N \in ℕ \land (((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \land ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0)))) \to (x \in Word Vtx (G) \land y \in Word Vtx (G))$
45		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
46		0nn0	$⊢ 0 \in ℕ_{0}$
47	45 46	jctil	$⊢ N \in ℕ \to (0 \in ℕ_{0} \land N \in ℕ_{0})$
48	47	adantr	$⊢ (N \in ℕ \land (((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \land ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0)))) \to (0 \in ℕ_{0} \land N \in ℕ_{0})$
49		nnre	$⊢ N \in ℕ \to N \in ℝ$
50	49	lep1d	$⊢ N \in ℕ \to N \leq N + 1$
51		breq2	$⊢ \|x\| = N + 1 \to (N \leq \|x\| \leftrightarrow N \leq N + 1)$
52	50 51	imbitrrid	$⊢ \|x\| = N + 1 \to (N \in ℕ \to N \leq \|x\|)$
53	52	ad2antlr	$⊢ ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0)) \to (N \in ℕ \to N \leq \|x\|)$
54	53	adantl	$⊢ (((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \land ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0))) \to (N \in ℕ \to N \leq \|x\|)$
55	54	impcom	$⊢ (N \in ℕ \land (((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \land ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0)))) \to N \leq \|x\|$
56		breq2	$⊢ \|y\| = N + 1 \to (N \leq \|y\| \leftrightarrow N \leq N + 1)$
57	50 56	imbitrrid	$⊢ \|y\| = N + 1 \to (N \in ℕ \to N \leq \|y\|)$
58	57	ad2antlr	$⊢ ((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \to (N \in ℕ \to N \leq \|y\|)$
59	58	adantr	$⊢ (((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \land ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0))) \to (N \in ℕ \to N \leq \|y\|)$
60	59	impcom	$⊢ (N \in ℕ \land (((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \land ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0)))) \to N \leq \|y\|$
61		pfxval	$⊢ (x \in Word Vtx (G) \land N \in ℕ_{0}) \to x prefix N = x substr ⟨0, N⟩$
62	61	ad2ant2rl	$⊢ ((x \in Word Vtx (G) \land y \in Word Vtx (G)) \land (0 \in ℕ_{0} \land N \in ℕ_{0})) \to x prefix N = x substr ⟨0, N⟩$
63		pfxval	$⊢ (y \in Word Vtx (G) \land N \in ℕ_{0}) \to y prefix N = y substr ⟨0, N⟩$
64	63	ad2ant2l	$⊢ ((x \in Word Vtx (G) \land y \in Word Vtx (G)) \land (0 \in ℕ_{0} \land N \in ℕ_{0})) \to y prefix N = y substr ⟨0, N⟩$
65	62 64	eqeq12d	$⊢ ((x \in Word Vtx (G) \land y \in Word Vtx (G)) \land (0 \in ℕ_{0} \land N \in ℕ_{0})) \to (x prefix N = y prefix N \leftrightarrow x substr ⟨0, N⟩ = y substr ⟨0, N⟩)$
66	65	3adant3	$⊢ ((x \in Word Vtx (G) \land y \in Word Vtx (G)) \land (0 \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|x\| \land N \leq \|y\|)) \to (x prefix N = y prefix N \leftrightarrow x substr ⟨0, N⟩ = y substr ⟨0, N⟩)$
67		swrdspsleq	$⊢ ((x \in Word Vtx (G) \land y \in Word Vtx (G)) \land (0 \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|x\| \land N \leq \|y\|)) \to (x substr ⟨0, N⟩ = y substr ⟨0, N⟩ \leftrightarrow \forall i \in (0 ..^N) x (i) = y (i))$
68	66 67	bitrd	$⊢ ((x \in Word Vtx (G) \land y \in Word Vtx (G)) \land (0 \in ℕ_{0} \land N \in ℕ_{0}) \land (N \leq \|x\| \land N \leq \|y\|)) \to (x prefix N = y prefix N \leftrightarrow \forall i \in (0 ..^N) x (i) = y (i))$
69	44 48 55 60 68	syl112anc	$⊢ (N \in ℕ \land (((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \land ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0)))) \to (x prefix N = y prefix N \leftrightarrow \forall i \in (0 ..^N) x (i) = y (i))$
70		lbfzo0	$⊢ 0 \in (0 ..^N) \leftrightarrow N \in ℕ$
71	70	biimpri	$⊢ N \in ℕ \to 0 \in (0 ..^N)$
72	71	adantr	$⊢ (N \in ℕ \land (((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \land ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0)))) \to 0 \in (0 ..^N)$
73		fveq2	$⊢ i = 0 \to x (i) = x (0)$
74		fveq2	$⊢ i = 0 \to y (i) = y (0)$
75	73 74	eqeq12d	$⊢ i = 0 \to (x (i) = y (i) \leftrightarrow x (0) = y (0))$
76	75	rspcv	$⊢ 0 \in (0 ..^N) \to (\forall i \in (0 ..^N) x (i) = y (i) \to x (0) = y (0))$
77	72 76	syl	$⊢ (N \in ℕ \land (((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \land ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0)))) \to (\forall i \in (0 ..^N) x (i) = y (i) \to x (0) = y (0))$
78	69 77	sylbid	$⊢ (N \in ℕ \land (((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \land ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0)))) \to (x prefix N = y prefix N \to x (0) = y (0))$
79	78	imp	$⊢ ((N \in ℕ \land (((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \land ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0)))) \land x prefix N = y prefix N) \to x (0) = y (0)$
80		simpr	$⊢ ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0)) \to lastS (x) = x (0)$
81		simpr	$⊢ ((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \to lastS (y) = y (0)$
82	80 81	eqeqan12rd	$⊢ (((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \land ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0))) \to (lastS (x) = lastS (y) \leftrightarrow x (0) = y (0))$
83	82	ad2antlr	$⊢ ((N \in ℕ \land (((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \land ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0)))) \land x prefix N = y prefix N) \to (lastS (x) = lastS (y) \leftrightarrow x (0) = y (0))$
84	79 83	mpbird	$⊢ ((N \in ℕ \land (((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \land ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0)))) \land x prefix N = y prefix N) \to lastS (x) = lastS (y)$
85	24 40 84	jca32	$⊢ ((N \in ℕ \land (((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \land ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0)))) \land x prefix N = y prefix N) \to (\|x\| = \|y\| \land (x prefix (\|x\| - 1) = y prefix (\|x\| - 1) \land lastS (x) = lastS (y)))$
86	42	adantl	$⊢ (((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \land ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0))) \to x \in Word Vtx (G)$
87	86	adantl	$⊢ (N \in ℕ \land (((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \land ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0)))) \to x \in Word Vtx (G)$
88	41	adantr	$⊢ (((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \land ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0))) \to y \in Word Vtx (G)$
89	88	adantl	$⊢ (N \in ℕ \land (((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \land ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0)))) \to y \in Word Vtx (G)$
90		1red	$⊢ N \in ℕ \to 1 \in ℝ$
91		nngt0	$⊢ N \in ℕ \to 0 < N$
92		0lt1	$⊢ 0 < 1$
93	92	a1i	$⊢ N \in ℕ \to 0 < 1$
94	49 90 91 93	addgt0d	$⊢ N \in ℕ \to 0 < N + 1$
95		breq2	$⊢ \|x\| = N + 1 \to (0 < \|x\| \leftrightarrow 0 < N + 1)$
96	94 95	imbitrrid	$⊢ \|x\| = N + 1 \to (N \in ℕ \to 0 < \|x\|)$
97	96	ad2antlr	$⊢ ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0)) \to (N \in ℕ \to 0 < \|x\|)$
98	97	adantl	$⊢ (((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \land ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0))) \to (N \in ℕ \to 0 < \|x\|)$
99	98	impcom	$⊢ (N \in ℕ \land (((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \land ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0)))) \to 0 < \|x\|$
100	87 89 99	3jca	$⊢ (N \in ℕ \land (((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \land ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0)))) \to (x \in Word Vtx (G) \land y \in Word Vtx (G) \land 0 < \|x\|)$
101	100	adantr	$⊢ ((N \in ℕ \land (((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \land ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0)))) \land x prefix N = y prefix N) \to (x \in Word Vtx (G) \land y \in Word Vtx (G) \land 0 < \|x\|)$
102		pfxsuff1eqwrdeq	$⊢ (x \in Word Vtx (G) \land y \in Word Vtx (G) \land 0 < \|x\|) \to (x = y \leftrightarrow (\|x\| = \|y\| \land (x prefix (\|x\| - 1) = y prefix (\|x\| - 1) \land lastS (x) = lastS (y))))$
103	101 102	syl	$⊢ ((N \in ℕ \land (((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \land ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0)))) \land x prefix N = y prefix N) \to (x = y \leftrightarrow (\|x\| = \|y\| \land (x prefix (\|x\| - 1) = y prefix (\|x\| - 1) \land lastS (x) = lastS (y))))$
104	85 103	mpbird	$⊢ ((N \in ℕ \land (((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \land ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0)))) \land x prefix N = y prefix N) \to x = y$
105	104	exp31	$⊢ N \in ℕ \to ((((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \land ((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0))) \to (x prefix N = y prefix N \to x = y))$
106	105	expdcom	$⊢ ((y \in Word Vtx (G) \land \|y\| = N + 1) \land lastS (y) = y (0)) \to (((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0)) \to (N \in ℕ \to (x prefix N = y prefix N \to x = y)))$
107	106	ex	$⊢ (y \in Word Vtx (G) \land \|y\| = N + 1) \to (lastS (y) = y (0) \to (((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0)) \to (N \in ℕ \to (x prefix N = y prefix N \to x = y))))$
108	107	3adant3	$⊢ (y \in Word Vtx (G) \land \|y\| = N + 1 \land \forall i \in (0 ..^N) \{y (i), y (i + 1)\} \in Edg (G)) \to (lastS (y) = y (0) \to (((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0)) \to (N \in ℕ \to (x prefix N = y prefix N \to x = y))))$
109	20 108	syl	$⊢ y \in (N WWalksN G) \to (lastS (y) = y (0) \to (((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0)) \to (N \in ℕ \to (x prefix N = y prefix N \to x = y))))$
110	109	imp	$⊢ (y \in (N WWalksN G) \land lastS (y) = y (0)) \to (((x \in Word Vtx (G) \land \|x\| = N + 1) \land lastS (x) = x (0)) \to (N \in ℕ \to (x prefix N = y prefix N \to x = y)))$
111	110	expdcom	$⊢ (x \in Word Vtx (G) \land \|x\| = N + 1) \to (lastS (x) = x (0) \to ((y \in (N WWalksN G) \land lastS (y) = y (0)) \to (N \in ℕ \to (x prefix N = y prefix N \to x = y))))$
112	111	3adant3	$⊢ (x \in Word Vtx (G) \land \|x\| = N + 1 \land \forall i \in (0 ..^N) \{x (i), x (i + 1)\} \in Edg (G)) \to (lastS (x) = x (0) \to ((y \in (N WWalksN G) \land lastS (y) = y (0)) \to (N \in ℕ \to (x prefix N = y prefix N \to x = y))))$
113	19 112	syl	$⊢ x \in (N WWalksN G) \to (lastS (x) = x (0) \to ((y \in (N WWalksN G) \land lastS (y) = y (0)) \to (N \in ℕ \to (x prefix N = y prefix N \to x = y))))$
114	113	imp31	$⊢ ((x \in (N WWalksN G) \land lastS (x) = x (0)) \land (y \in (N WWalksN G) \land lastS (y) = y (0))) \to (N \in ℕ \to (x prefix N = y prefix N \to x = y))$
115	114	com12	$⊢ N \in ℕ \to (((x \in (N WWalksN G) \land lastS (x) = x (0)) \land (y \in (N WWalksN G) \land lastS (y) = y (0))) \to (x prefix N = y prefix N \to x = y))$
116	16 115	biimtrid	$⊢ N \in ℕ \to ((x \in D \land y \in D) \to (x prefix N = y prefix N \to x = y))$
117	116	imp	$⊢ (N \in ℕ \land (x \in D \land y \in D)) \to (x prefix N = y prefix N \to x = y)$
118	7 117	sylbid	$⊢ (N \in ℕ \land (x \in D \land y \in D)) \to (F (x) = F (y) \to x = y)$
119	118	ralrimivva	$⊢ N \in ℕ \to \forall x \in D \forall y \in D (F (x) = F (y) \to x = y)$
120		dff13	$⊢ F : D \underset{1-1}{⟶} N ClWWalksN G \leftrightarrow (F : D ⟶ N ClWWalksN G \land \forall x \in D \forall y \in D (F (x) = F (y) \to x = y))$
121	3 119 120	sylanbrc	$⊢ N \in ℕ \to F : D \underset{1-1}{⟶} N ClWWalksN G$

Metamath Proof Explorer

Theorem clwwlkf1

Proof