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 Word dom I k 0 ..^ F I F k = P k P k + 1 Fun F -1

Proof

Step Hyp Ref Expression
1 wrdfin F Word dom I F Fin
2 wrdf F Word dom I F : 0 ..^ F dom I
3 simpr F Fin F : 0 ..^ F dom I F : 0 ..^ F dom I
4 3 adantr F Fin F : 0 ..^ F dom I P : 0 F 1-1 V k 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 0 ..^ F k 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 0 ..^ F k 0 ..^ F I F k = P k P k + 1 I F y = P y P y + 1
17 10 16 anim12ii x 0 ..^ F y 0 ..^ F k 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 V
27 fvex P x + 1 V
28 fvex P y V
29 fvex P y + 1 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 0 F b 0 F P a = P b a = b
32 elfzofz x 0 ..^ F x 0 F
33 elfzofz y 0 ..^ F y 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 0 F y 0 F a 0 F b 0 F P a = P b a = b P x = P y x = y
42 32 33 41 syl2an x 0 ..^ F y 0 ..^ F a 0 F b 0 F P a = P b a = b P x = P y x = y
43 42 a1dd x 0 ..^ F y 0 ..^ F a 0 F b 0 F P a = P b a = b F Fin P x = P y x = y
44 43 com14 P x = P y a 0 F b 0 F P a = P b a = b F Fin x 0 ..^ F y 0 ..^ F x = y
45 44 adantr P x = P y P x + 1 = P y + 1 a 0 F b 0 F P a = P b a = b F Fin x 0 ..^ F y 0 ..^ F x = y
46 hashcl F Fin F 0
47 32 a1i F 0 x 0 ..^ F x 0 F
48 fzofzp1 y 0 ..^ F y + 1 0 F
49 47 48 anim12d1 F 0 x 0 ..^ F y 0 ..^ F x 0 F y + 1 0 F
50 49 imp F 0 x 0 ..^ F y 0 ..^ F x 0 F y + 1 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 0 F y + 1 0 F a 0 F b 0 F P a = P b a = b P x = P y + 1 x = y + 1
56 50 55 syl F 0 x 0 ..^ F y 0 ..^ F a 0 F b 0 F P a = P b a = b P x = P y + 1 x = y + 1
57 56 imp F 0 x 0 ..^ F y 0 ..^ F a 0 F b 0 F P a = P b a = b P x = P y + 1 x = y + 1
58 fzofzp1 x 0 ..^ F x + 1 0 F
59 58 a1i F 0 x 0 ..^ F x + 1 0 F
60 59 33 anim12d1 F 0 x 0 ..^ F y 0 ..^ F x + 1 0 F y 0 F
61 60 imp F 0 x 0 ..^ F y 0 ..^ F x + 1 0 F y 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 0 F y 0 F a 0 F b 0 F P a = P b a = b P x + 1 = P y x + 1 = y
69 61 68 syl F 0 x 0 ..^ F y 0 ..^ F a 0 F b 0 F P a = P b a = b P x + 1 = P y x + 1 = y
70 69 imp F 0 x 0 ..^ F y 0 ..^ F a 0 F b 0 F P a = P b a = b P x + 1 = P y x + 1 = y
71 57 70 anim12d F 0 x 0 ..^ F y 0 ..^ F a 0 F b 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 0 x 0 ..^ F y 0 ..^ F a 0 F b 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 0 ..^ F y 0 ..^ F x = y + 1 x + 1 = y y + 1 + 1 = y
76 elfzonn0 y 0 ..^ F y 0
77 nn0cn y 0 y
78 add1p1 y y + 1 + 1 = y + 2
79 77 78 syl y 0 y + 1 + 1 = y + 2
80 79 eqeq1d y 0 y + 1 + 1 = y y + 2 = y
81 2cnd y 0 2
82 2ne0 2 0
83 82 a1i y 0 2 0
84 addn0nid y 2 2 0 y + 2 y
85 77 81 83 84 syl3anc y 0 y + 2 y
86 eqneqall y + 2 = y y + 2 y x = y
87 85 86 syl5com y 0 y + 2 = y x = y
88 80 87 sylbid y 0 y + 1 + 1 = y x = y
89 76 88 syl y 0 ..^ F y + 1 + 1 = y x = y
90 89 adantl x 0 ..^ F y 0 ..^ F y + 1 + 1 = y x = y
91 90 adantr x 0 ..^ F y 0 ..^ F x = y + 1 y + 1 + 1 = y x = y
92 75 91 sylbid x 0 ..^ F y 0 ..^ F x = y + 1 x + 1 = y x = y
93 92 expimpd x 0 ..^ F y 0 ..^ F x = y + 1 x + 1 = y x = y
94 93 adantl F 0 x 0 ..^ F y 0 ..^ F x = y + 1 x + 1 = y x = y
95 72 94 syld F 0 x 0 ..^ F y 0 ..^ F a 0 F b 0 F P a = P b a = b P x = P y + 1 P x + 1 = P y x = y
96 95 ex F 0 x 0 ..^ F y 0 ..^ F a 0 F b 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 Fin x 0 ..^ F y 0 ..^ F a 0 F b 0 F P a = P b a = b P x = P y + 1 P x + 1 = P y x = y
98 97 com3l x 0 ..^ F y 0 ..^ F a 0 F b 0 F P a = P b a = b P x = P y + 1 P x + 1 = P y F Fin x = y
99 98 expd x 0 ..^ F y 0 ..^ F a 0 F b 0 F P a = P b a = b P x = P y + 1 P x + 1 = P y F Fin x = y
100 99 com34 x 0 ..^ F y 0 ..^ F a 0 F b 0 F P a = P b a = b F 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 0 F b 0 F P a = P b a = b F Fin x 0 ..^ F y 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 0 F b 0 F P a = P b a = b F Fin x 0 ..^ F y 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 0 F b 0 F P a = P b a = b F Fin x 0 ..^ F y 0 ..^ F x = y
104 31 103 syl5bi 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 Fin x 0 ..^ F y 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 Fin P : 0 F 1-1 V x 0 ..^ F y 0 ..^ F x = y
106 30 105 sylbi P x P x + 1 = P y P y + 1 F Fin P : 0 F 1-1 V x 0 ..^ F y 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 Fin P : 0 F 1-1 V x 0 ..^ F y 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 Fin P : 0 F 1-1 V x 0 ..^ F y 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 Fin P : 0 F 1-1 V x 0 ..^ F y 0 ..^ F x = y
110 109 com15 x 0 ..^ F y 0 ..^ F I F x = P x P x + 1 I F y = P y P y + 1 F Fin P : 0 F 1-1 V F x = F y x = y
111 17 110 syld x 0 ..^ F y 0 ..^ F k 0 ..^ F I F k = P k P k + 1 F Fin P : 0 F 1-1 V F x = F y x = y
112 111 com14 P : 0 F 1-1 V k 0 ..^ F I F k = P k P k + 1 F Fin x 0 ..^ F y 0 ..^ F F x = F y x = y
113 112 imp P : 0 F 1-1 V k 0 ..^ F I F k = P k P k + 1 F Fin x 0 ..^ F y 0 ..^ F F x = F y x = y
114 113 impcom F Fin P : 0 F 1-1 V k 0 ..^ F I F k = P k P k + 1 x 0 ..^ F y 0 ..^ F F x = F y x = y
115 114 ralrimivv F Fin P : 0 F 1-1 V k 0 ..^ F I F k = P k P k + 1 x 0 ..^ F y 0 ..^ F F x = F y x = y
116 115 adantlr F Fin F : 0 ..^ F dom I P : 0 F 1-1 V k 0 ..^ F I F k = P k P k + 1 x 0 ..^ F y 0 ..^ F F x = F y x = y
117 dff13 F : 0 ..^ F 1-1 dom I F : 0 ..^ F dom I x 0 ..^ F y 0 ..^ F F x = F y x = y
118 4 116 117 sylanbrc F Fin F : 0 ..^ F dom I P : 0 F 1-1 V k 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 -1
120 118 119 sylib F Fin F : 0 ..^ F dom I P : 0 F 1-1 V k 0 ..^ F I F k = P k P k + 1 F : 0 ..^ F dom I Fun F -1
121 simpr F : 0 ..^ F dom I Fun F -1 Fun F -1
122 120 121 syl F Fin F : 0 ..^ F dom I P : 0 F 1-1 V k 0 ..^ F I F k = P k P k + 1 Fun F -1
123 122 ex F Fin F : 0 ..^ F dom I P : 0 F 1-1 V k 0 ..^ F I F k = P k P k + 1 Fun F -1
124 123 expd F Fin F : 0 ..^ F dom I P : 0 F 1-1 V k 0 ..^ F I F k = P k P k + 1 Fun F -1
125 1 2 124 syl2anc F Word dom I P : 0 F 1-1 V k 0 ..^ F I F k = P k P k + 1 Fun F -1
126 125 impcom P : 0 F 1-1 V F Word dom I k 0 ..^ F I F k = P k P k + 1 Fun F -1