clwlkclwwlklem2

		Ref	Expression
	Assertion	clwlkclwwlklem2	$⊢ ((E : dom E \underset{1-1}{⟶} R \land F \in Word dom E) \land (P : (0 \dots \|F\|) ⟶ V \land 2 \leq \|P\|) \land (\forall i \in (0 ..^\|F\|) E (F (i)) = \{P (i), P (i + 1)\} \land P (0) = P (\|F\|))) \to (lastS (P) = P (0) \land \forall i \in (0 ..^\|F\| - 1) \{P (i), P (i + 1)\} \in ran E \land \{P (\|F\| - 1), P (0)\} \in ran E)$

Proof

Step	Hyp	Ref	Expression
1		f1fn	$⊢ E : dom E \underset{1-1}{⟶} R \to E Fn dom E$
2		dffn3	$⊢ E Fn dom E \leftrightarrow E : dom E ⟶ ran E$
3	1 2	sylib	$⊢ E : dom E \underset{1-1}{⟶} R \to E : dom E ⟶ ran E$
4		lencl	$⊢ F \in Word dom E \to \|F\| \in ℕ_{0}$
5		ffn	$⊢ P : (0 \dots \|F\|) ⟶ V \to P Fn (0 \dots \|F\|)$
6		fnfz0hash	$⊢ (\|F\| \in ℕ_{0} \land P Fn (0 \dots \|F\|)) \to \|P\| = \|F\| + 1$
7	4 5 6	syl2an	$⊢ (F \in Word dom E \land P : (0 \dots \|F\|) ⟶ V) \to \|P\| = \|F\| + 1$
8		ffz0iswrd	$⊢ P : (0 \dots \|F\|) ⟶ V \to P \in Word V$
9		lsw	$⊢ P \in Word V \to lastS (P) = P (\|P\| - 1)$
10	9	ad6antr	$⊢ ((((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \land (\forall i \in (0 ..^\|F\|) E (F (i)) = \{P (i), P (i + 1)\} \land P (0) = P (\|F\|))) \to lastS (P) = P (\|P\| - 1)$
11		fvoveq1	$⊢ \|P\| = \|F\| + 1 \to P (\|P\| - 1) = P (\|F\| + 1 - 1)$
12	11	ad4antlr	$⊢ ((((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \land (\forall i \in (0 ..^\|F\|) E (F (i)) = \{P (i), P (i + 1)\} \land P (0) = P (\|F\|))) \to P (\|P\| - 1) = P (\|F\| + 1 - 1)$
13		eqcom	$⊢ P (0) = P (\|F\|) \leftrightarrow P (\|F\|) = P (0)$
14		nn0cn	$⊢ \|F\| \in ℕ_{0} \to \|F\| \in ℂ$
15		1cnd	$⊢ \|F\| \in ℕ_{0} \to 1 \in ℂ$
16	14 15	pncand	$⊢ \|F\| \in ℕ_{0} \to \|F\| + 1 - 1 = \|F\|$
17	16	eqcomd	$⊢ \|F\| \in ℕ_{0} \to \|F\| = \|F\| + 1 - 1$
18	17	ad4antlr	$⊢ (((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \to \|F\| = \|F\| + 1 - 1$
19	18	fveqeq2d	$⊢ (((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \to (P (\|F\|) = P (0) \leftrightarrow P (\|F\| + 1 - 1) = P (0))$
20	19	biimpd	$⊢ (((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \to (P (\|F\|) = P (0) \to P (\|F\| + 1 - 1) = P (0))$
21	13 20	syl5bi	$⊢ (((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \to (P (0) = P (\|F\|) \to P (\|F\| + 1 - 1) = P (0))$
22	21	adantld	$⊢ (((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \to ((\forall i \in (0 ..^\|F\|) E (F (i)) = \{P (i), P (i + 1)\} \land P (0) = P (\|F\|)) \to P (\|F\| + 1 - 1) = P (0))$
23	22	imp	$⊢ ((((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \land (\forall i \in (0 ..^\|F\|) E (F (i)) = \{P (i), P (i + 1)\} \land P (0) = P (\|F\|))) \to P (\|F\| + 1 - 1) = P (0)$
24	10 12 23	3eqtrd	$⊢ ((((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \land (\forall i \in (0 ..^\|F\|) E (F (i)) = \{P (i), P (i + 1)\} \land P (0) = P (\|F\|))) \to lastS (P) = P (0)$
25		nn0z	$⊢ \|F\| \in ℕ_{0} \to \|F\| \in ℤ$
26		peano2zm	$⊢ \|F\| \in ℤ \to \|F\| - 1 \in ℤ$
27	25 26	syl	$⊢ \|F\| \in ℕ_{0} \to \|F\| - 1 \in ℤ$
28		nn0re	$⊢ \|F\| \in ℕ_{0} \to \|F\| \in ℝ$
29	28	lem1d	$⊢ \|F\| \in ℕ_{0} \to \|F\| - 1 \leq \|F\|$
30		eluz2	$⊢ \|F\| \in ℤ_{\geq (\|F\| - 1)} \leftrightarrow (\|F\| - 1 \in ℤ \land \|F\| \in ℤ \land \|F\| - 1 \leq \|F\|)$
31	27 25 29 30	syl3anbrc	$⊢ \|F\| \in ℕ_{0} \to \|F\| \in ℤ_{\geq (\|F\| - 1)}$
32	31	ad4antlr	$⊢ (((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \to \|F\| \in ℤ_{\geq (\|F\| - 1)}$
33		fzoss2	$⊢ \|F\| \in ℤ_{\geq (\|F\| - 1)} \to (0 ..^\|F\| - 1) \subseteq (0 ..^\|F\|)$
34		ssralv	$⊢ (0 ..^\|F\| - 1) \subseteq (0 ..^\|F\|) \to (\forall i \in (0 ..^\|F\|) E (F (i)) = \{P (i), P (i + 1)\} \to \forall i \in (0 ..^\|F\| - 1) E (F (i)) = \{P (i), P (i + 1)\})$
35	32 33 34	3syl	$⊢ (((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \to (\forall i \in (0 ..^\|F\|) E (F (i)) = \{P (i), P (i + 1)\} \to \forall i \in (0 ..^\|F\| - 1) E (F (i)) = \{P (i), P (i + 1)\})$
36		simpr	$⊢ (((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \to E : dom E ⟶ ran E$
37	36	adantr	$⊢ ((((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \land i \in (0 ..^\|F\| - 1)) \to E : dom E ⟶ ran E$
38		wrdf	$⊢ F \in Word dom E \to F : (0 ..^\|F\|) ⟶ dom E$
39		simpll	$⊢ ((F : (0 ..^\|F\|) ⟶ dom E \land \|F\| \in ℕ_{0}) \land i \in (0 ..^\|F\| - 1)) \to F : (0 ..^\|F\|) ⟶ dom E$
40		fzossrbm1	$⊢ \|F\| \in ℤ \to (0 ..^\|F\| - 1) \subseteq (0 ..^\|F\|)$
41	25 40	syl	$⊢ \|F\| \in ℕ_{0} \to (0 ..^\|F\| - 1) \subseteq (0 ..^\|F\|)$
42	41	adantl	$⊢ (F : (0 ..^\|F\|) ⟶ dom E \land \|F\| \in ℕ_{0}) \to (0 ..^\|F\| - 1) \subseteq (0 ..^\|F\|)$
43	42	sselda	$⊢ ((F : (0 ..^\|F\|) ⟶ dom E \land \|F\| \in ℕ_{0}) \land i \in (0 ..^\|F\| - 1)) \to i \in (0 ..^\|F\|)$
44	39 43	ffvelrnd	$⊢ ((F : (0 ..^\|F\|) ⟶ dom E \land \|F\| \in ℕ_{0}) \land i \in (0 ..^\|F\| - 1)) \to F (i) \in dom E$
45	44	exp31	$⊢ F : (0 ..^\|F\|) ⟶ dom E \to (\|F\| \in ℕ_{0} \to (i \in (0 ..^\|F\| - 1) \to F (i) \in dom E))$
46	38 45	syl	$⊢ F \in Word dom E \to (\|F\| \in ℕ_{0} \to (i \in (0 ..^\|F\| - 1) \to F (i) \in dom E))$
47	46	adantl	$⊢ (P \in Word V \land F \in Word dom E) \to (\|F\| \in ℕ_{0} \to (i \in (0 ..^\|F\| - 1) \to F (i) \in dom E))$
48	47	imp	$⊢ ((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \to (i \in (0 ..^\|F\| - 1) \to F (i) \in dom E)$
49	48	ad3antrrr	$⊢ (((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \to (i \in (0 ..^\|F\| - 1) \to F (i) \in dom E)$
50	49	imp	$⊢ ((((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \land i \in (0 ..^\|F\| - 1)) \to F (i) \in dom E$
51	37 50	ffvelrnd	$⊢ ((((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \land i \in (0 ..^\|F\| - 1)) \to E (F (i)) \in ran E$
52		eqcom	$⊢ E (F (i)) = \{P (i), P (i + 1)\} \leftrightarrow \{P (i), P (i + 1)\} = E (F (i))$
53	52	biimpi	$⊢ E (F (i)) = \{P (i), P (i + 1)\} \to \{P (i), P (i + 1)\} = E (F (i))$
54	53	eleq1d	$⊢ E (F (i)) = \{P (i), P (i + 1)\} \to (\{P (i), P (i + 1)\} \in ran E \leftrightarrow E (F (i)) \in ran E)$
55	51 54	syl5ibrcom	$⊢ ((((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \land i \in (0 ..^\|F\| - 1)) \to (E (F (i)) = \{P (i), P (i + 1)\} \to \{P (i), P (i + 1)\} \in ran E)$
56	55	ralimdva	$⊢ (((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \to (\forall i \in (0 ..^\|F\| - 1) E (F (i)) = \{P (i), P (i + 1)\} \to \forall i \in (0 ..^\|F\| - 1) \{P (i), P (i + 1)\} \in ran E)$
57	35 56	syldc	$⊢ \forall i \in (0 ..^\|F\|) E (F (i)) = \{P (i), P (i + 1)\} \to ((((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \to \forall i \in (0 ..^\|F\| - 1) \{P (i), P (i + 1)\} \in ran E)$
58	57	adantr	$⊢ (\forall i \in (0 ..^\|F\|) E (F (i)) = \{P (i), P (i + 1)\} \land P (0) = P (\|F\|)) \to ((((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \to \forall i \in (0 ..^\|F\| - 1) \{P (i), P (i + 1)\} \in ran E)$
59	58	impcom	$⊢ ((((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \land (\forall i \in (0 ..^\|F\|) E (F (i)) = \{P (i), P (i + 1)\} \land P (0) = P (\|F\|))) \to \forall i \in (0 ..^\|F\| - 1) \{P (i), P (i + 1)\} \in ran E$
60		breq2	$⊢ \|P\| = \|F\| + 1 \to (2 \leq \|P\| \leftrightarrow 2 \leq \|F\| + 1)$
61	60	adantl	$⊢ (((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \to (2 \leq \|P\| \leftrightarrow 2 \leq \|F\| + 1)$
62		2re	$⊢ 2 \in ℝ$
63	62	a1i	$⊢ \|F\| \in ℕ_{0} \to 2 \in ℝ$
64		1red	$⊢ \|F\| \in ℕ_{0} \to 1 \in ℝ$
65	63 64 28	lesubaddd	$⊢ \|F\| \in ℕ_{0} \to (2 - 1 \leq \|F\| \leftrightarrow 2 \leq \|F\| + 1)$
66		2m1e1	$⊢ 2 - 1 = 1$
67	66	breq1i	$⊢ 2 - 1 \leq \|F\| \leftrightarrow 1 \leq \|F\|$
68		elnnnn0c	$⊢ \|F\| \in ℕ \leftrightarrow (\|F\| \in ℕ_{0} \land 1 \leq \|F\|)$
69	68	simplbi2	$⊢ \|F\| \in ℕ_{0} \to (1 \leq \|F\| \to \|F\| \in ℕ)$
70	67 69	syl5bi	$⊢ \|F\| \in ℕ_{0} \to (2 - 1 \leq \|F\| \to \|F\| \in ℕ)$
71	65 70	sylbird	$⊢ \|F\| \in ℕ_{0} \to (2 \leq \|F\| + 1 \to \|F\| \in ℕ)$
72	71	adantl	$⊢ ((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \to (2 \leq \|F\| + 1 \to \|F\| \in ℕ)$
73	72	adantr	$⊢ (((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \to (2 \leq \|F\| + 1 \to \|F\| \in ℕ)$
74	61 73	sylbid	$⊢ (((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \to (2 \leq \|P\| \to \|F\| \in ℕ)$
75	74	imp	$⊢ ((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \to \|F\| \in ℕ$
76	75	adantr	$⊢ (((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \to \|F\| \in ℕ$
77		lbfzo0	$⊢ 0 \in (0 ..^\|F\|) \leftrightarrow \|F\| \in ℕ$
78	76 77	sylibr	$⊢ (((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \to 0 \in (0 ..^\|F\|)$
79		fzoend	$⊢ 0 \in (0 ..^\|F\|) \to \|F\| - 1 \in (0 ..^\|F\|)$
80	78 79	syl	$⊢ (((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \to \|F\| - 1 \in (0 ..^\|F\|)$
81		2fveq3	$⊢ i = \|F\| - 1 \to E (F (i)) = E (F (\|F\| - 1))$
82		fveq2	$⊢ i = \|F\| - 1 \to P (i) = P (\|F\| - 1)$
83		fvoveq1	$⊢ i = \|F\| - 1 \to P (i + 1) = P (\|F\| - 1 + 1)$
84	82 83	preq12d	$⊢ i = \|F\| - 1 \to \{P (i), P (i + 1)\} = \{P (\|F\| - 1), P (\|F\| - 1 + 1)\}$
85	81 84	eqeq12d	$⊢ i = \|F\| - 1 \to (E (F (i)) = \{P (i), P (i + 1)\} \leftrightarrow E (F (\|F\| - 1)) = \{P (\|F\| - 1), P (\|F\| - 1 + 1)\})$
86	85	adantl	$⊢ ((((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \land i = \|F\| - 1) \to (E (F (i)) = \{P (i), P (i + 1)\} \leftrightarrow E (F (\|F\| - 1)) = \{P (\|F\| - 1), P (\|F\| - 1 + 1)\})$
87	80 86	rspcdv	$⊢ (((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \to (\forall i \in (0 ..^\|F\|) E (F (i)) = \{P (i), P (i + 1)\} \to E (F (\|F\| - 1)) = \{P (\|F\| - 1), P (\|F\| - 1 + 1)\})$
88	14 15	npcand	$⊢ \|F\| \in ℕ_{0} \to \|F\| - 1 + 1 = \|F\|$
89	88	ad4antlr	$⊢ (((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \to \|F\| - 1 + 1 = \|F\|$
90	89	fveq2d	$⊢ (((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \to P (\|F\| - 1 + 1) = P (\|F\|)$
91	90	preq2d	$⊢ (((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \to \{P (\|F\| - 1), P (\|F\| - 1 + 1)\} = \{P (\|F\| - 1), P (\|F\|)\}$
92	91	eqeq2d	$⊢ (((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \to (E (F (\|F\| - 1)) = \{P (\|F\| - 1), P (\|F\| - 1 + 1)\} \leftrightarrow E (F (\|F\| - 1)) = \{P (\|F\| - 1), P (\|F\|)\})$
93	38	ad4antlr	$⊢ ((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \to F : (0 ..^\|F\|) ⟶ dom E$
94	71	com12	$⊢ 2 \leq \|F\| + 1 \to (\|F\| \in ℕ_{0} \to \|F\| \in ℕ)$
95	60 94	syl6bi	$⊢ \|P\| = \|F\| + 1 \to (2 \leq \|P\| \to (\|F\| \in ℕ_{0} \to \|F\| \in ℕ))$
96	95	com3r	$⊢ \|F\| \in ℕ_{0} \to (\|P\| = \|F\| + 1 \to (2 \leq \|P\| \to \|F\| \in ℕ))$
97	96	adantl	$⊢ ((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \to (\|P\| = \|F\| + 1 \to (2 \leq \|P\| \to \|F\| \in ℕ))$
98	97	imp31	$⊢ ((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \to \|F\| \in ℕ$
99	98 77	sylibr	$⊢ ((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \to 0 \in (0 ..^\|F\|)$
100	99 79	syl	$⊢ ((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \to \|F\| - 1 \in (0 ..^\|F\|)$
101	93 100	ffvelrnd	$⊢ ((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \to F (\|F\| - 1) \in dom E$
102	101	adantr	$⊢ (((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \to F (\|F\| - 1) \in dom E$
103	36 102	ffvelrnd	$⊢ (((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \to E (F (\|F\| - 1)) \in ran E$
104		eqcom	$⊢ E (F (\|F\| - 1)) = \{P (\|F\| - 1), P (\|F\|)\} \leftrightarrow \{P (\|F\| - 1), P (\|F\|)\} = E (F (\|F\| - 1))$
105	104	biimpi	$⊢ E (F (\|F\| - 1)) = \{P (\|F\| - 1), P (\|F\|)\} \to \{P (\|F\| - 1), P (\|F\|)\} = E (F (\|F\| - 1))$
106	105	eleq1d	$⊢ E (F (\|F\| - 1)) = \{P (\|F\| - 1), P (\|F\|)\} \to (\{P (\|F\| - 1), P (\|F\|)\} \in ran E \leftrightarrow E (F (\|F\| - 1)) \in ran E)$
107	103 106	syl5ibrcom	$⊢ (((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \to (E (F (\|F\| - 1)) = \{P (\|F\| - 1), P (\|F\|)\} \to \{P (\|F\| - 1), P (\|F\|)\} \in ran E)$
108	92 107	sylbid	$⊢ (((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \to (E (F (\|F\| - 1)) = \{P (\|F\| - 1), P (\|F\| - 1 + 1)\} \to \{P (\|F\| - 1), P (\|F\|)\} \in ran E)$
109	87 108	syldc	$⊢ \forall i \in (0 ..^\|F\|) E (F (i)) = \{P (i), P (i + 1)\} \to ((((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \to \{P (\|F\| - 1), P (\|F\|)\} \in ran E)$
110	109	adantr	$⊢ (\forall i \in (0 ..^\|F\|) E (F (i)) = \{P (i), P (i + 1)\} \land P (0) = P (\|F\|)) \to ((((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \to \{P (\|F\| - 1), P (\|F\|)\} \in ran E)$
111	110	impcom	$⊢ ((((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \land (\forall i \in (0 ..^\|F\|) E (F (i)) = \{P (i), P (i + 1)\} \land P (0) = P (\|F\|))) \to \{P (\|F\| - 1), P (\|F\|)\} \in ran E$
112		preq2	$⊢ P (0) = P (\|F\|) \to \{P (\|F\| - 1), P (0)\} = \{P (\|F\| - 1), P (\|F\|)\}$
113	112	eleq1d	$⊢ P (0) = P (\|F\|) \to (\{P (\|F\| - 1), P (0)\} \in ran E \leftrightarrow \{P (\|F\| - 1), P (\|F\|)\} \in ran E)$
114	113	adantl	$⊢ (\forall i \in (0 ..^\|F\|) E (F (i)) = \{P (i), P (i + 1)\} \land P (0) = P (\|F\|)) \to (\{P (\|F\| - 1), P (0)\} \in ran E \leftrightarrow \{P (\|F\| - 1), P (\|F\|)\} \in ran E)$
115	114	adantl	$⊢ ((((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \land (\forall i \in (0 ..^\|F\|) E (F (i)) = \{P (i), P (i + 1)\} \land P (0) = P (\|F\|))) \to (\{P (\|F\| - 1), P (0)\} \in ran E \leftrightarrow \{P (\|F\| - 1), P (\|F\|)\} \in ran E)$
116	111 115	mpbird	$⊢ ((((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \land (\forall i \in (0 ..^\|F\|) E (F (i)) = \{P (i), P (i + 1)\} \land P (0) = P (\|F\|))) \to \{P (\|F\| - 1), P (0)\} \in ran E$
117	24 59 116	3jca	$⊢ ((((((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \land 2 \leq \|P\|) \land E : dom E ⟶ ran E) \land (\forall i \in (0 ..^\|F\|) E (F (i)) = \{P (i), P (i + 1)\} \land P (0) = P (\|F\|))) \to (lastS (P) = P (0) \land \forall i \in (0 ..^\|F\| - 1) \{P (i), P (i + 1)\} \in ran E \land \{P (\|F\| - 1), P (0)\} \in ran E)$
118	117	exp41	$⊢ (((P \in Word V \land F \in Word dom E) \land \|F\| \in ℕ_{0}) \land \|P\| = \|F\| + 1) \to (2 \leq \|P\| \to (E : dom E ⟶ ran E \to ((\forall i \in (0 ..^\|F\|) E (F (i)) = \{P (i), P (i + 1)\} \land P (0) = P (\|F\|)) \to (lastS (P) = P (0) \land \forall i \in (0 ..^\|F\| - 1) \{P (i), P (i + 1)\} \in ran E \land \{P (\|F\| - 1), P (0)\} \in ran E))))$
119	118	exp41	$⊢ P \in Word V \to (F \in Word dom E \to (\|F\| \in ℕ_{0} \to (\|P\| = \|F\| + 1 \to (2 \leq \|P\| \to (E : dom E ⟶ ran E \to ((\forall i \in (0 ..^\|F\|) E (F (i)) = \{P (i), P (i + 1)\} \land P (0) = P (\|F\|)) \to (lastS (P) = P (0) \land \forall i \in (0 ..^\|F\| - 1) \{P (i), P (i + 1)\} \in ran E \land \{P (\|F\| - 1), P (0)\} \in ran E)))))))$
120	8 119	syl	$⊢ P : (0 \dots \|F\|) ⟶ V \to (F \in Word dom E \to (\|F\| \in ℕ_{0} \to (\|P\| = \|F\| + 1 \to (2 \leq \|P\| \to (E : dom E ⟶ ran E \to ((\forall i \in (0 ..^\|F\|) E (F (i)) = \{P (i), P (i + 1)\} \land P (0) = P (\|F\|)) \to (lastS (P) = P (0) \land \forall i \in (0 ..^\|F\| - 1) \{P (i), P (i + 1)\} \in ran E \land \{P (\|F\| - 1), P (0)\} \in ran E)))))))$
121	120	com13	$⊢ \|F\| \in ℕ_{0} \to (F \in Word dom E \to (P : (0 \dots \|F\|) ⟶ V \to (\|P\| = \|F\| + 1 \to (2 \leq \|P\| \to (E : dom E ⟶ ran E \to ((\forall i \in (0 ..^\|F\|) E (F (i)) = \{P (i), P (i + 1)\} \land P (0) = P (\|F\|)) \to (lastS (P) = P (0) \land \forall i \in (0 ..^\|F\| - 1) \{P (i), P (i + 1)\} \in ran E \land \{P (\|F\| - 1), P (0)\} \in ran E)))))))$
122	4 121	mpcom	$⊢ F \in Word dom E \to (P : (0 \dots \|F\|) ⟶ V \to (\|P\| = \|F\| + 1 \to (2 \leq \|P\| \to (E : dom E ⟶ ran E \to ((\forall i \in (0 ..^\|F\|) E (F (i)) = \{P (i), P (i + 1)\} \land P (0) = P (\|F\|)) \to (lastS (P) = P (0) \land \forall i \in (0 ..^\|F\| - 1) \{P (i), P (i + 1)\} \in ran E \land \{P (\|F\| - 1), P (0)\} \in ran E))))))$
123	122	imp	$⊢ (F \in Word dom E \land P : (0 \dots \|F\|) ⟶ V) \to (\|P\| = \|F\| + 1 \to (2 \leq \|P\| \to (E : dom E ⟶ ran E \to ((\forall i \in (0 ..^\|F\|) E (F (i)) = \{P (i), P (i + 1)\} \land P (0) = P (\|F\|)) \to (lastS (P) = P (0) \land \forall i \in (0 ..^\|F\| - 1) \{P (i), P (i + 1)\} \in ran E \land \{P (\|F\| - 1), P (0)\} \in ran E)))))$
124	7 123	mpd	$⊢ (F \in Word dom E \land P : (0 \dots \|F\|) ⟶ V) \to (2 \leq \|P\| \to (E : dom E ⟶ ran E \to ((\forall i \in (0 ..^\|F\|) E (F (i)) = \{P (i), P (i + 1)\} \land P (0) = P (\|F\|)) \to (lastS (P) = P (0) \land \forall i \in (0 ..^\|F\| - 1) \{P (i), P (i + 1)\} \in ran E \land \{P (\|F\| - 1), P (0)\} \in ran E))))$
125	124	expcom	$⊢ P : (0 \dots \|F\|) ⟶ V \to (F \in Word dom E \to (2 \leq \|P\| \to (E : dom E ⟶ ran E \to ((\forall i \in (0 ..^\|F\|) E (F (i)) = \{P (i), P (i + 1)\} \land P (0) = P (\|F\|)) \to (lastS (P) = P (0) \land \forall i \in (0 ..^\|F\| - 1) \{P (i), P (i + 1)\} \in ran E \land \{P (\|F\| - 1), P (0)\} \in ran E)))))$
126	125	com14	$⊢ E : dom E ⟶ ran E \to (F \in Word dom E \to (2 \leq \|P\| \to (P : (0 \dots \|F\|) ⟶ V \to ((\forall i \in (0 ..^\|F\|) E (F (i)) = \{P (i), P (i + 1)\} \land P (0) = P (\|F\|)) \to (lastS (P) = P (0) \land \forall i \in (0 ..^\|F\| - 1) \{P (i), P (i + 1)\} \in ran E \land \{P (\|F\| - 1), P (0)\} \in ran E)))))$
127	126	imp	$⊢ (E : dom E ⟶ ran E \land F \in Word dom E) \to (2 \leq \|P\| \to (P : (0 \dots \|F\|) ⟶ V \to ((\forall i \in (0 ..^\|F\|) E (F (i)) = \{P (i), P (i + 1)\} \land P (0) = P (\|F\|)) \to (lastS (P) = P (0) \land \forall i \in (0 ..^\|F\| - 1) \{P (i), P (i + 1)\} \in ran E \land \{P (\|F\| - 1), P (0)\} \in ran E))))$
128	127	impcomd	$⊢ (E : dom E ⟶ ran E \land F \in Word dom E) \to ((P : (0 \dots \|F\|) ⟶ V \land 2 \leq \|P\|) \to ((\forall i \in (0 ..^\|F\|) E (F (i)) = \{P (i), P (i + 1)\} \land P (0) = P (\|F\|)) \to (lastS (P) = P (0) \land \forall i \in (0 ..^\|F\| - 1) \{P (i), P (i + 1)\} \in ran E \land \{P (\|F\| - 1), P (0)\} \in ran E)))$
129	3 128	sylan	$⊢ (E : dom E \underset{1-1}{⟶} R \land F \in Word dom E) \to ((P : (0 \dots \|F\|) ⟶ V \land 2 \leq \|P\|) \to ((\forall i \in (0 ..^\|F\|) E (F (i)) = \{P (i), P (i + 1)\} \land P (0) = P (\|F\|)) \to (lastS (P) = P (0) \land \forall i \in (0 ..^\|F\| - 1) \{P (i), P (i + 1)\} \in ran E \land \{P (\|F\| - 1), P (0)\} \in ran E)))$
130	129	3imp	$⊢ ((E : dom E \underset{1-1}{⟶} R \land F \in Word dom E) \land (P : (0 \dots \|F\|) ⟶ V \land 2 \leq \|P\|) \land (\forall i \in (0 ..^\|F\|) E (F (i)) = \{P (i), P (i + 1)\} \land P (0) = P (\|F\|))) \to (lastS (P) = P (0) \land \forall i \in (0 ..^\|F\| - 1) \{P (i), P (i + 1)\} \in ran E \land \{P (\|F\| - 1), P (0)\} \in ran E)$

Metamath Proof Explorer

Theorem clwlkclwwlklem2

Proof