Metamath Proof Explorer


Theorem vdwlem13

Description: Lemma for vdw . Main induction on K ; K = 0 , K = 1 base cases. (Contributed by Mario Carneiro, 18-Aug-2014)

Ref Expression
Hypotheses vdw.r φ R Fin
vdw.k φ K 0
Assertion vdwlem13 φ n f R 1 n K MonoAP f

Proof

Step Hyp Ref Expression
1 vdw.r φ R Fin
2 vdw.k φ K 0
3 elnn1uz2 K K = 1 K 2
4 ovex 1 1 V
5 elmapg R Fin 1 1 V f R 1 1 f : 1 1 R
6 1 4 5 sylancl φ f R 1 1 f : 1 1 R
7 6 biimpa φ f R 1 1 f : 1 1 R
8 1nn 1
9 vdwap1 1 1 1 AP 1 1 = 1
10 8 8 9 mp2an 1 AP 1 1 = 1
11 1z 1
12 elfz3 1 1 1 1
13 11 12 mp1i φ f : 1 1 R 1 1 1
14 eqidd φ f : 1 1 R f 1 = f 1
15 ffn f : 1 1 R f Fn 1 1
16 15 adantl φ f : 1 1 R f Fn 1 1
17 fniniseg f Fn 1 1 1 f -1 f 1 1 1 1 f 1 = f 1
18 16 17 syl φ f : 1 1 R 1 f -1 f 1 1 1 1 f 1 = f 1
19 13 14 18 mpbir2and φ f : 1 1 R 1 f -1 f 1
20 19 snssd φ f : 1 1 R 1 f -1 f 1
21 10 20 eqsstrid φ f : 1 1 R 1 AP 1 1 f -1 f 1
22 7 21 syldan φ f R 1 1 1 AP 1 1 f -1 f 1
23 22 ralrimiva φ f R 1 1 1 AP 1 1 f -1 f 1
24 fveq2 K = 1 AP K = AP 1
25 24 oveqd K = 1 1 AP K 1 = 1 AP 1 1
26 25 sseq1d K = 1 1 AP K 1 f -1 f 1 1 AP 1 1 f -1 f 1
27 26 ralbidv K = 1 f R 1 1 1 AP K 1 f -1 f 1 f R 1 1 1 AP 1 1 f -1 f 1
28 23 27 syl5ibrcom φ K = 1 f R 1 1 1 AP K 1 f -1 f 1
29 oveq1 a = 1 a AP K d = 1 AP K d
30 29 sseq1d a = 1 a AP K d f -1 f 1 1 AP K d f -1 f 1
31 oveq2 d = 1 1 AP K d = 1 AP K 1
32 31 sseq1d d = 1 1 AP K d f -1 f 1 1 AP K 1 f -1 f 1
33 30 32 rspc2ev 1 1 1 AP K 1 f -1 f 1 a d a AP K d f -1 f 1
34 8 8 33 mp3an12 1 AP K 1 f -1 f 1 a d a AP K d f -1 f 1
35 fvex f 1 V
36 sneq c = f 1 c = f 1
37 36 imaeq2d c = f 1 f -1 c = f -1 f 1
38 37 sseq2d c = f 1 a AP K d f -1 c a AP K d f -1 f 1
39 38 2rexbidv c = f 1 a d a AP K d f -1 c a d a AP K d f -1 f 1
40 35 39 spcev a d a AP K d f -1 f 1 c a d a AP K d f -1 c
41 34 40 syl 1 AP K 1 f -1 f 1 c a d a AP K d f -1 c
42 2 adantr φ f R 1 1 K 0
43 4 42 7 vdwmc φ f R 1 1 K MonoAP f c a d a AP K d f -1 c
44 41 43 syl5ibr φ f R 1 1 1 AP K 1 f -1 f 1 K MonoAP f
45 44 ralimdva φ f R 1 1 1 AP K 1 f -1 f 1 f R 1 1 K MonoAP f
46 oveq2 n = 1 1 n = 1 1
47 46 oveq2d n = 1 R 1 n = R 1 1
48 47 raleqdv n = 1 f R 1 n K MonoAP f f R 1 1 K MonoAP f
49 48 rspcev 1 f R 1 1 K MonoAP f n f R 1 n K MonoAP f
50 8 49 mpan f R 1 1 K MonoAP f n f R 1 n K MonoAP f
51 45 50 syl6 φ f R 1 1 1 AP K 1 f -1 f 1 n f R 1 n K MonoAP f
52 28 51 syld φ K = 1 n f R 1 n K MonoAP f
53 breq1 x = 2 x MonoAP f 2 MonoAP f
54 53 rexralbidv x = 2 n f r 1 n x MonoAP f n f r 1 n 2 MonoAP f
55 54 ralbidv x = 2 r Fin n f r 1 n x MonoAP f r Fin n f r 1 n 2 MonoAP f
56 breq1 x = k x MonoAP f k MonoAP f
57 56 rexralbidv x = k n f r 1 n x MonoAP f n f r 1 n k MonoAP f
58 57 ralbidv x = k r Fin n f r 1 n x MonoAP f r Fin n f r 1 n k MonoAP f
59 breq1 x = k + 1 x MonoAP f k + 1 MonoAP f
60 59 rexralbidv x = k + 1 n f r 1 n x MonoAP f n f r 1 n k + 1 MonoAP f
61 60 ralbidv x = k + 1 r Fin n f r 1 n x MonoAP f r Fin n f r 1 n k + 1 MonoAP f
62 breq1 x = K x MonoAP f K MonoAP f
63 62 rexralbidv x = K n f r 1 n x MonoAP f n f r 1 n K MonoAP f
64 63 ralbidv x = K r Fin n f r 1 n x MonoAP f r Fin n f r 1 n K MonoAP f
65 hashcl r Fin r 0
66 nn0p1nn r 0 r + 1
67 65 66 syl r Fin r + 1
68 simpll r Fin f r 1 r + 1 ¬ 2 MonoAP f r Fin
69 simplr r Fin f r 1 r + 1 ¬ 2 MonoAP f f r 1 r + 1
70 vex r V
71 ovex 1 r + 1 V
72 70 71 elmap f r 1 r + 1 f : 1 r + 1 r
73 69 72 sylib r Fin f r 1 r + 1 ¬ 2 MonoAP f f : 1 r + 1 r
74 simpr r Fin f r 1 r + 1 ¬ 2 MonoAP f ¬ 2 MonoAP f
75 68 73 74 vdwlem12 ¬ r Fin f r 1 r + 1 ¬ 2 MonoAP f
76 iman r Fin f r 1 r + 1 2 MonoAP f ¬ r Fin f r 1 r + 1 ¬ 2 MonoAP f
77 75 76 mpbir r Fin f r 1 r + 1 2 MonoAP f
78 77 ralrimiva r Fin f r 1 r + 1 2 MonoAP f
79 oveq2 n = r + 1 1 n = 1 r + 1
80 79 oveq2d n = r + 1 r 1 n = r 1 r + 1
81 80 raleqdv n = r + 1 f r 1 n 2 MonoAP f f r 1 r + 1 2 MonoAP f
82 81 rspcev r + 1 f r 1 r + 1 2 MonoAP f n f r 1 n 2 MonoAP f
83 67 78 82 syl2anc r Fin n f r 1 n 2 MonoAP f
84 83 rgen r Fin n f r 1 n 2 MonoAP f
85 oveq1 r = s r 1 n = s 1 n
86 85 raleqdv r = s f r 1 n k MonoAP f f s 1 n k MonoAP f
87 86 rexbidv r = s n f r 1 n k MonoAP f n f s 1 n k MonoAP f
88 oveq2 n = m 1 n = 1 m
89 88 oveq2d n = m s 1 n = s 1 m
90 89 raleqdv n = m f s 1 n k MonoAP f f s 1 m k MonoAP f
91 breq2 f = g k MonoAP f k MonoAP g
92 91 cbvralvw f s 1 m k MonoAP f g s 1 m k MonoAP g
93 90 92 bitrdi n = m f s 1 n k MonoAP f g s 1 m k MonoAP g
94 93 cbvrexvw n f s 1 n k MonoAP f m g s 1 m k MonoAP g
95 87 94 bitrdi r = s n f r 1 n k MonoAP f m g s 1 m k MonoAP g
96 95 cbvralvw r Fin n f r 1 n k MonoAP f s Fin m g s 1 m k MonoAP g
97 simplr k 2 r Fin s Fin m g s 1 m k MonoAP g r Fin
98 simpll k 2 r Fin s Fin m g s 1 m k MonoAP g k 2
99 simpr k 2 r Fin s Fin m g s 1 m k MonoAP g s Fin m g s 1 m k MonoAP g
100 94 ralbii s Fin n f s 1 n k MonoAP f s Fin m g s 1 m k MonoAP g
101 99 100 sylibr k 2 r Fin s Fin m g s 1 m k MonoAP g s Fin n f s 1 n k MonoAP f
102 97 98 101 vdwlem11 k 2 r Fin s Fin m g s 1 m k MonoAP g n f r 1 n k + 1 MonoAP f
103 102 ex k 2 r Fin s Fin m g s 1 m k MonoAP g n f r 1 n k + 1 MonoAP f
104 103 ralrimdva k 2 s Fin m g s 1 m k MonoAP g r Fin n f r 1 n k + 1 MonoAP f
105 96 104 syl5bi k 2 r Fin n f r 1 n k MonoAP f r Fin n f r 1 n k + 1 MonoAP f
106 55 58 61 64 84 105 uzind4i K 2 r Fin n f r 1 n K MonoAP f
107 oveq1 r = R r 1 n = R 1 n
108 107 raleqdv r = R f r 1 n K MonoAP f f R 1 n K MonoAP f
109 108 rexbidv r = R n f r 1 n K MonoAP f n f R 1 n K MonoAP f
110 109 rspcv R Fin r Fin n f r 1 n K MonoAP f n f R 1 n K MonoAP f
111 1 106 110 syl2im φ K 2 n f R 1 n K MonoAP f
112 52 111 jaod φ K = 1 K 2 n f R 1 n K MonoAP f
113 3 112 syl5bi φ K n f R 1 n K MonoAP f
114 fveq2 K = 0 AP K = AP 0
115 114 oveqd K = 0 1 AP K 1 = 1 AP 0 1
116 vdwap0 1 1 1 AP 0 1 =
117 8 8 116 mp2an 1 AP 0 1 =
118 115 117 eqtrdi K = 0 1 AP K 1 =
119 0ss f -1 f 1
120 118 119 eqsstrdi K = 0 1 AP K 1 f -1 f 1
121 120 ralrimivw K = 0 f R 1 1 1 AP K 1 f -1 f 1
122 121 51 syl5 φ K = 0 n f R 1 n K MonoAP f
123 elnn0 K 0 K K = 0
124 2 123 sylib φ K K = 0
125 113 122 124 mpjaod φ n f R 1 n K MonoAP f