upgrwlkdvdelem

		Ref	Expression
	Assertion	upgrwlkdvdelem	$⊢ (P : (0 \dots \|F\|) \underset{1-1}{⟶} V \land F \in Word dom I) \to (\forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\} \to Fun F^{-1})$

Proof

Step	Hyp	Ref	Expression
1		wrdfin	$⊢ F \in Word dom I \to F \in Fin$
2		wrdf	$⊢ F \in Word dom I \to F : (0 ..^\|F\|) ⟶ dom I$
3		simpr	$⊢ (F \in Fin \land F : (0 ..^\|F\|) ⟶ dom I) \to F : (0 ..^\|F\|) ⟶ dom I$
4	3	adantr	$⊢ ((F \in Fin \land F : (0 ..^\|F\|) ⟶ dom I) \land (P : (0 \dots \|F\|) \underset{1-1}{⟶} V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\})) \to F : (0 ..^\|F\|) ⟶ dom I$
5		2fveq3	$⊢ k = x \to I (F (k)) = I (F (x))$
6		fveq2	$⊢ k = x \to P (k) = P (x)$
7		fvoveq1	$⊢ k = x \to P (k + 1) = P (x + 1)$
8	6 7	preq12d	$⊢ k = x \to \{P (k), P (k + 1)\} = \{P (x), P (x + 1)\}$
9	5 8	eqeq12d	$⊢ k = x \to (I (F (k)) = \{P (k), P (k + 1)\} \leftrightarrow I (F (x)) = \{P (x), P (x + 1)\})$
10	9	rspcv	$⊢ x \in (0 ..^\|F\|) \to (\forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\} \to I (F (x)) = \{P (x), P (x + 1)\})$
11		2fveq3	$⊢ k = y \to I (F (k)) = I (F (y))$
12		fveq2	$⊢ k = y \to P (k) = P (y)$
13		fvoveq1	$⊢ k = y \to P (k + 1) = P (y + 1)$
14	12 13	preq12d	$⊢ k = y \to \{P (k), P (k + 1)\} = \{P (y), P (y + 1)\}$
15	11 14	eqeq12d	$⊢ k = y \to (I (F (k)) = \{P (k), P (k + 1)\} \leftrightarrow I (F (y)) = \{P (y), P (y + 1)\})$
16	15	rspcv	$⊢ y \in (0 ..^\|F\|) \to (\forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\} \to I (F (y)) = \{P (y), P (y + 1)\})$
17	10 16	anim12ii	$⊢ (x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|)) \to (\forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\} \to (I (F (x)) = \{P (x), P (x + 1)\} \land I (F (y)) = \{P (y), P (y + 1)\}))$
18		fveq2	$⊢ F (x) = F (y) \to I (F (x)) = I (F (y))$
19		simpl	$⊢ (I (F (x)) = \{P (x), P (x + 1)\} \land I (F (y)) = \{P (y), P (y + 1)\}) \to I (F (x)) = \{P (x), P (x + 1)\}$
20	19	eqcomd	$⊢ (I (F (x)) = \{P (x), P (x + 1)\} \land I (F (y)) = \{P (y), P (y + 1)\}) \to \{P (x), P (x + 1)\} = I (F (x))$
21	20	adantl	$⊢ (I (F (x)) = I (F (y)) \land (I (F (x)) = \{P (x), P (x + 1)\} \land I (F (y)) = \{P (y), P (y + 1)\})) \to \{P (x), P (x + 1)\} = I (F (x))$
22		simpl	$⊢ (I (F (x)) = I (F (y)) \land (I (F (x)) = \{P (x), P (x + 1)\} \land I (F (y)) = \{P (y), P (y + 1)\})) \to I (F (x)) = I (F (y))$
23		simpr	$⊢ (I (F (x)) = \{P (x), P (x + 1)\} \land I (F (y)) = \{P (y), P (y + 1)\}) \to I (F (y)) = \{P (y), P (y + 1)\}$
24	23	adantl	$⊢ (I (F (x)) = I (F (y)) \land (I (F (x)) = \{P (x), P (x + 1)\} \land I (F (y)) = \{P (y), P (y + 1)\})) \to I (F (y)) = \{P (y), P (y + 1)\}$
25	21 22 24	3eqtrd	$⊢ (I (F (x)) = I (F (y)) \land (I (F (x)) = \{P (x), P (x + 1)\} \land I (F (y)) = \{P (y), P (y + 1)\})) \to \{P (x), P (x + 1)\} = \{P (y), P (y + 1)\}$
26		fvex	$⊢ P (x) \in V$
27		fvex	$⊢ P (x + 1) \in V$
28		fvex	$⊢ P (y) \in V$
29		fvex	$⊢ P (y + 1) \in V$
30	26 27 28 29	preq12b	$⊢ \{P (x), P (x + 1)\} = \{P (y), P (y + 1)\} \leftrightarrow ((P (x) = P (y) \land P (x + 1) = P (y + 1)) \lor (P (x) = P (y + 1) \land P (x + 1) = P (y)))$
31		dff13	$⊢ P : (0 \dots \|F\|) \underset{1-1}{⟶} V \leftrightarrow (P : (0 \dots \|F\|) ⟶ V \land \forall a \in (0 \dots \|F\|) \forall b \in (0 \dots \|F\|) (P (a) = P (b) \to a = b))$
32		elfzofz	$⊢ x \in (0 ..^\|F\|) \to x \in (0 \dots \|F\|)$
33		elfzofz	$⊢ y \in (0 ..^\|F\|) \to y \in (0 \dots \|F\|)$
34		fveqeq2	$⊢ a = x \to (P (a) = P (b) \leftrightarrow P (x) = P (b))$
35		eqeq1	$⊢ a = x \to (a = b \leftrightarrow x = b)$
36	34 35	imbi12d	$⊢ a = x \to ((P (a) = P (b) \to a = b) \leftrightarrow (P (x) = P (b) \to x = b))$
37		fveq2	$⊢ b = y \to P (b) = P (y)$
38	37	eqeq2d	$⊢ b = y \to (P (x) = P (b) \leftrightarrow P (x) = P (y))$
39		eqeq2	$⊢ b = y \to (x = b \leftrightarrow x = y)$
40	38 39	imbi12d	$⊢ b = y \to ((P (x) = P (b) \to x = b) \leftrightarrow (P (x) = P (y) \to x = y))$
41	36 40	rspc2v	$⊢ (x \in (0 \dots \|F\|) \land y \in (0 \dots \|F\|)) \to (\forall a \in (0 \dots \|F\|) \forall b \in (0 \dots \|F\|) (P (a) = P (b) \to a = b) \to (P (x) = P (y) \to x = y))$
42	32 33 41	syl2an	$⊢ (x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|)) \to (\forall a \in (0 \dots \|F\|) \forall b \in (0 \dots \|F\|) (P (a) = P (b) \to a = b) \to (P (x) = P (y) \to x = y))$
43	42	a1dd	$⊢ (x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|)) \to (\forall a \in (0 \dots \|F\|) \forall b \in (0 \dots \|F\|) (P (a) = P (b) \to a = b) \to (F \in Fin \to (P (x) = P (y) \to x = y)))$
44	43	com14	$⊢ P (x) = P (y) \to (\forall a \in (0 \dots \|F\|) \forall b \in (0 \dots \|F\|) (P (a) = P (b) \to a = b) \to (F \in Fin \to ((x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|)) \to x = y)))$
45	44	adantr	$⊢ (P (x) = P (y) \land P (x + 1) = P (y + 1)) \to (\forall a \in (0 \dots \|F\|) \forall b \in (0 \dots \|F\|) (P (a) = P (b) \to a = b) \to (F \in Fin \to ((x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|)) \to x = y)))$
46		hashcl	$⊢ F \in Fin \to \|F\| \in ℕ_{0}$
47	32	a1i	$⊢ \|F\| \in ℕ_{0} \to (x \in (0 ..^\|F\|) \to x \in (0 \dots \|F\|))$
48		fzofzp1	$⊢ y \in (0 ..^\|F\|) \to y + 1 \in (0 \dots \|F\|)$
49	47 48	anim12d1	$⊢ \|F\| \in ℕ_{0} \to ((x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|)) \to (x \in (0 \dots \|F\|) \land y + 1 \in (0 \dots \|F\|)))$
50	49	imp	$⊢ (\|F\| \in ℕ_{0} \land (x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|))) \to (x \in (0 \dots \|F\|) \land y + 1 \in (0 \dots \|F\|))$
51		fveq2	$⊢ b = y + 1 \to P (b) = P (y + 1)$
52	51	eqeq2d	$⊢ b = y + 1 \to (P (x) = P (b) \leftrightarrow P (x) = P (y + 1))$
53		eqeq2	$⊢ b = y + 1 \to (x = b \leftrightarrow x = y + 1)$
54	52 53	imbi12d	$⊢ b = y + 1 \to ((P (x) = P (b) \to x = b) \leftrightarrow (P (x) = P (y + 1) \to x = y + 1))$
55	36 54	rspc2v	$⊢ (x \in (0 \dots \|F\|) \land y + 1 \in (0 \dots \|F\|)) \to (\forall a \in (0 \dots \|F\|) \forall b \in (0 \dots \|F\|) (P (a) = P (b) \to a = b) \to (P (x) = P (y + 1) \to x = y + 1))$
56	50 55	syl	$⊢ (\|F\| \in ℕ_{0} \land (x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|))) \to (\forall a \in (0 \dots \|F\|) \forall b \in (0 \dots \|F\|) (P (a) = P (b) \to a = b) \to (P (x) = P (y + 1) \to x = y + 1))$
57	56	imp	$⊢ ((\|F\| \in ℕ_{0} \land (x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|))) \land \forall a \in (0 \dots \|F\|) \forall b \in (0 \dots \|F\|) (P (a) = P (b) \to a = b)) \to (P (x) = P (y + 1) \to x = y + 1)$
58		fzofzp1	$⊢ x \in (0 ..^\|F\|) \to x + 1 \in (0 \dots \|F\|)$
59	58	a1i	$⊢ \|F\| \in ℕ_{0} \to (x \in (0 ..^\|F\|) \to x + 1 \in (0 \dots \|F\|))$
60	59 33	anim12d1	$⊢ \|F\| \in ℕ_{0} \to ((x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|)) \to (x + 1 \in (0 \dots \|F\|) \land y \in (0 \dots \|F\|)))$
61	60	imp	$⊢ (\|F\| \in ℕ_{0} \land (x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|))) \to (x + 1 \in (0 \dots \|F\|) \land y \in (0 \dots \|F\|))$
62		fveqeq2	$⊢ a = x + 1 \to (P (a) = P (b) \leftrightarrow P (x + 1) = P (b))$
63		eqeq1	$⊢ a = x + 1 \to (a = b \leftrightarrow x + 1 = b)$
64	62 63	imbi12d	$⊢ a = x + 1 \to ((P (a) = P (b) \to a = b) \leftrightarrow (P (x + 1) = P (b) \to x + 1 = b))$
65	37	eqeq2d	$⊢ b = y \to (P (x + 1) = P (b) \leftrightarrow P (x + 1) = P (y))$
66		eqeq2	$⊢ b = y \to (x + 1 = b \leftrightarrow x + 1 = y)$
67	65 66	imbi12d	$⊢ b = y \to ((P (x + 1) = P (b) \to x + 1 = b) \leftrightarrow (P (x + 1) = P (y) \to x + 1 = y))$
68	64 67	rspc2v	$⊢ (x + 1 \in (0 \dots \|F\|) \land y \in (0 \dots \|F\|)) \to (\forall a \in (0 \dots \|F\|) \forall b \in (0 \dots \|F\|) (P (a) = P (b) \to a = b) \to (P (x + 1) = P (y) \to x + 1 = y))$
69	61 68	syl	$⊢ (\|F\| \in ℕ_{0} \land (x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|))) \to (\forall a \in (0 \dots \|F\|) \forall b \in (0 \dots \|F\|) (P (a) = P (b) \to a = b) \to (P (x + 1) = P (y) \to x + 1 = y))$
70	69	imp	$⊢ ((\|F\| \in ℕ_{0} \land (x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|))) \land \forall a \in (0 \dots \|F\|) \forall b \in (0 \dots \|F\|) (P (a) = P (b) \to a = b)) \to (P (x + 1) = P (y) \to x + 1 = y)$
71	57 70	anim12d	$⊢ ((\|F\| \in ℕ_{0} \land (x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|))) \land \forall a \in (0 \dots \|F\|) \forall b \in (0 \dots \|F\|) (P (a) = P (b) \to a = b)) \to ((P (x) = P (y + 1) \land P (x + 1) = P (y)) \to (x = y + 1 \land x + 1 = y))$
72	71	expimpd	$⊢ (\|F\| \in ℕ_{0} \land (x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|))) \to ((\forall a \in (0 \dots \|F\|) \forall b \in (0 \dots \|F\|) (P (a) = P (b) \to a = b) \land (P (x) = P (y + 1) \land P (x + 1) = P (y))) \to (x = y + 1 \land x + 1 = y))$
73		oveq1	$⊢ x = y + 1 \to x + 1 = y + 1 + 1$
74	73	eqeq1d	$⊢ x = y + 1 \to (x + 1 = y \leftrightarrow y + 1 + 1 = y)$
75	74	adantl	$⊢ ((x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|)) \land x = y + 1) \to (x + 1 = y \leftrightarrow y + 1 + 1 = y)$
76		elfzonn0	$⊢ y \in (0 ..^\|F\|) \to y \in ℕ_{0}$
77		nn0cn	$⊢ y \in ℕ_{0} \to y \in ℂ$
78		add1p1	$⊢ y \in ℂ \to y + 1 + 1 = y + 2$
79	77 78	syl	$⊢ y \in ℕ_{0} \to y + 1 + 1 = y + 2$
80	79	eqeq1d	$⊢ y \in ℕ_{0} \to (y + 1 + 1 = y \leftrightarrow y + 2 = y)$
81		2cnd	$⊢ y \in ℕ_{0} \to 2 \in ℂ$
82		2ne0	$⊢ 2 \neq 0$
83	82	a1i	$⊢ y \in ℕ_{0} \to 2 \neq 0$
84		addn0nid	$⊢ (y \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to y + 2 \neq y$
85	77 81 83 84	syl3anc	$⊢ y \in ℕ_{0} \to y + 2 \neq y$
86		eqneqall	$⊢ y + 2 = y \to (y + 2 \neq y \to x = y)$
87	85 86	syl5com	$⊢ y \in ℕ_{0} \to (y + 2 = y \to x = y)$
88	80 87	sylbid	$⊢ y \in ℕ_{0} \to (y + 1 + 1 = y \to x = y)$
89	76 88	syl	$⊢ y \in (0 ..^\|F\|) \to (y + 1 + 1 = y \to x = y)$
90	89	adantl	$⊢ (x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|)) \to (y + 1 + 1 = y \to x = y)$
91	90	adantr	$⊢ ((x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|)) \land x = y + 1) \to (y + 1 + 1 = y \to x = y)$
92	75 91	sylbid	$⊢ ((x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|)) \land x = y + 1) \to (x + 1 = y \to x = y)$
93	92	expimpd	$⊢ (x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|)) \to ((x = y + 1 \land x + 1 = y) \to x = y)$
94	93	adantl	$⊢ (\|F\| \in ℕ_{0} \land (x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|))) \to ((x = y + 1 \land x + 1 = y) \to x = y)$
95	72 94	syld	$⊢ (\|F\| \in ℕ_{0} \land (x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|))) \to ((\forall a \in (0 \dots \|F\|) \forall b \in (0 \dots \|F\|) (P (a) = P (b) \to a = b) \land (P (x) = P (y + 1) \land P (x + 1) = P (y))) \to x = y)$
96	95	ex	$⊢ \|F\| \in ℕ_{0} \to ((x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|)) \to ((\forall a \in (0 \dots \|F\|) \forall b \in (0 \dots \|F\|) (P (a) = P (b) \to a = b) \land (P (x) = P (y + 1) \land P (x + 1) = P (y))) \to x = y))$
97	46 96	syl	$⊢ F \in Fin \to ((x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|)) \to ((\forall a \in (0 \dots \|F\|) \forall b \in (0 \dots \|F\|) (P (a) = P (b) \to a = b) \land (P (x) = P (y + 1) \land P (x + 1) = P (y))) \to x = y))$
98	97	com3l	$⊢ (x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|)) \to ((\forall a \in (0 \dots \|F\|) \forall b \in (0 \dots \|F\|) (P (a) = P (b) \to a = b) \land (P (x) = P (y + 1) \land P (x + 1) = P (y))) \to (F \in Fin \to x = y))$
99	98	expd	$⊢ (x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|)) \to (\forall a \in (0 \dots \|F\|) \forall b \in (0 \dots \|F\|) (P (a) = P (b) \to a = b) \to ((P (x) = P (y + 1) \land P (x + 1) = P (y)) \to (F \in Fin \to x = y)))$
100	99	com34	$⊢ (x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|)) \to (\forall a \in (0 \dots \|F\|) \forall b \in (0 \dots \|F\|) (P (a) = P (b) \to a = b) \to (F \in Fin \to ((P (x) = P (y + 1) \land P (x + 1) = P (y)) \to x = y)))$
101	100	com14	$⊢ (P (x) = P (y + 1) \land P (x + 1) = P (y)) \to (\forall a \in (0 \dots \|F\|) \forall b \in (0 \dots \|F\|) (P (a) = P (b) \to a = b) \to (F \in Fin \to ((x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|)) \to x = y)))$
102	45 101	jaoi	$⊢ ((P (x) = P (y) \land P (x + 1) = P (y + 1)) \lor (P (x) = P (y + 1) \land P (x + 1) = P (y))) \to (\forall a \in (0 \dots \|F\|) \forall b \in (0 \dots \|F\|) (P (a) = P (b) \to a = b) \to (F \in Fin \to ((x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|)) \to x = y)))$
103	102	adantld	$⊢ ((P (x) = P (y) \land P (x + 1) = P (y + 1)) \lor (P (x) = P (y + 1) \land P (x + 1) = P (y))) \to ((P : (0 \dots \|F\|) ⟶ V \land \forall a \in (0 \dots \|F\|) \forall b \in (0 \dots \|F\|) (P (a) = P (b) \to a = b)) \to (F \in Fin \to ((x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|)) \to x = y)))$
104	31 103	biimtrid	$⊢ ((P (x) = P (y) \land P (x + 1) = P (y + 1)) \lor (P (x) = P (y + 1) \land P (x + 1) = P (y))) \to (P : (0 \dots \|F\|) \underset{1-1}{⟶} V \to (F \in Fin \to ((x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|)) \to x = y)))$
105	104	com23	$⊢ ((P (x) = P (y) \land P (x + 1) = P (y + 1)) \lor (P (x) = P (y + 1) \land P (x + 1) = P (y))) \to (F \in Fin \to (P : (0 \dots \|F\|) \underset{1-1}{⟶} V \to ((x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|)) \to x = y)))$
106	30 105	sylbi	$⊢ \{P (x), P (x + 1)\} = \{P (y), P (y + 1)\} \to (F \in Fin \to (P : (0 \dots \|F\|) \underset{1-1}{⟶} V \to ((x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|)) \to x = y)))$
107	25 106	syl	$⊢ (I (F (x)) = I (F (y)) \land (I (F (x)) = \{P (x), P (x + 1)\} \land I (F (y)) = \{P (y), P (y + 1)\})) \to (F \in Fin \to (P : (0 \dots \|F\|) \underset{1-1}{⟶} V \to ((x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|)) \to x = y)))$
108	107	ex	$⊢ I (F (x)) = I (F (y)) \to ((I (F (x)) = \{P (x), P (x + 1)\} \land I (F (y)) = \{P (y), P (y + 1)\}) \to (F \in Fin \to (P : (0 \dots \|F\|) \underset{1-1}{⟶} V \to ((x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|)) \to x = y))))$
109	18 108	syl	$⊢ F (x) = F (y) \to ((I (F (x)) = \{P (x), P (x + 1)\} \land I (F (y)) = \{P (y), P (y + 1)\}) \to (F \in Fin \to (P : (0 \dots \|F\|) \underset{1-1}{⟶} V \to ((x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|)) \to x = y))))$
110	109	com15	$⊢ (x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|)) \to ((I (F (x)) = \{P (x), P (x + 1)\} \land I (F (y)) = \{P (y), P (y + 1)\}) \to (F \in Fin \to (P : (0 \dots \|F\|) \underset{1-1}{⟶} V \to (F (x) = F (y) \to x = y))))$
111	17 110	syld	$⊢ (x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|)) \to (\forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\} \to (F \in Fin \to (P : (0 \dots \|F\|) \underset{1-1}{⟶} V \to (F (x) = F (y) \to x = y))))$
112	111	com14	$⊢ P : (0 \dots \|F\|) \underset{1-1}{⟶} V \to (\forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\} \to (F \in Fin \to ((x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|)) \to (F (x) = F (y) \to x = y))))$
113	112	imp	$⊢ (P : (0 \dots \|F\|) \underset{1-1}{⟶} V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\}) \to (F \in Fin \to ((x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|)) \to (F (x) = F (y) \to x = y)))$
114	113	impcom	$⊢ (F \in Fin \land (P : (0 \dots \|F\|) \underset{1-1}{⟶} V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\})) \to ((x \in (0 ..^\|F\|) \land y \in (0 ..^\|F\|)) \to (F (x) = F (y) \to x = y))$
115	114	ralrimivv	$⊢ (F \in Fin \land (P : (0 \dots \|F\|) \underset{1-1}{⟶} V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\})) \to \forall x \in (0 ..^\|F\|) \forall y \in (0 ..^\|F\|) (F (x) = F (y) \to x = y)$
116	115	adantlr	$⊢ ((F \in Fin \land F : (0 ..^\|F\|) ⟶ dom I) \land (P : (0 \dots \|F\|) \underset{1-1}{⟶} V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\})) \to \forall x \in (0 ..^\|F\|) \forall y \in (0 ..^\|F\|) (F (x) = F (y) \to x = y)$
117		dff13	$⊢ F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \leftrightarrow (F : (0 ..^\|F\|) ⟶ dom I \land \forall x \in (0 ..^\|F\|) \forall y \in (0 ..^\|F\|) (F (x) = F (y) \to x = y))$
118	4 116 117	sylanbrc	$⊢ ((F \in Fin \land F : (0 ..^\|F\|) ⟶ dom I) \land (P : (0 \dots \|F\|) \underset{1-1}{⟶} V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\})) \to F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I$
119		df-f1	$⊢ F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \leftrightarrow (F : (0 ..^\|F\|) ⟶ dom I \land Fun F^{-1})$
120	118 119	sylib	$⊢ ((F \in Fin \land F : (0 ..^\|F\|) ⟶ dom I) \land (P : (0 \dots \|F\|) \underset{1-1}{⟶} V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\})) \to (F : (0 ..^\|F\|) ⟶ dom I \land Fun F^{-1})$
121		simpr	$⊢ (F : (0 ..^\|F\|) ⟶ dom I \land Fun F^{-1}) \to Fun F^{-1}$
122	120 121	syl	$⊢ ((F \in Fin \land F : (0 ..^\|F\|) ⟶ dom I) \land (P : (0 \dots \|F\|) \underset{1-1}{⟶} V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\})) \to Fun F^{-1}$
123	122	ex	$⊢ (F \in Fin \land F : (0 ..^\|F\|) ⟶ dom I) \to ((P : (0 \dots \|F\|) \underset{1-1}{⟶} V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\}) \to Fun F^{-1})$
124	123	expd	$⊢ (F \in Fin \land F : (0 ..^\|F\|) ⟶ dom I) \to (P : (0 \dots \|F\|) \underset{1-1}{⟶} V \to (\forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\} \to Fun F^{-1}))$
125	1 2 124	syl2anc	$⊢ F \in Word dom I \to (P : (0 \dots \|F\|) \underset{1-1}{⟶} V \to (\forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\} \to Fun F^{-1}))$
126	125	impcom	$⊢ (P : (0 \dots \|F\|) \underset{1-1}{⟶} V \land F \in Word dom I) \to (\forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\} \to Fun F^{-1})$

Metamath Proof Explorer

Theorem upgrwlkdvdelem

Proof