Metamath Proof Explorer

Theorem upgrwlkdvdelem

Description: Lemma for upgrwlkdvde . (Contributed by Alexander van der Vekens, 27-Oct-2017) (Proof shortened by AV, 17-Jan-2021)

Ref Expression
Assertion upgrwlkdvdelem 
|- ( ( P : ( 0 ... ( # ` F ) ) -1-1-> V /\ F e. Word dom I ) -> ( A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } -> Fun `' F ) )

Proof

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