MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fseqenlem1 Unicode version

Theorem fseqenlem1 8426
Description: Lemma for fseqen 8429. (Contributed by Mario Carneiro, 17-May-2015.)
Hypotheses
Ref Expression
fseqenlem.a
fseqenlem.b
fseqenlem.f
fseqenlem.g
Assertion
Ref Expression
fseqenlem1
Distinct variable groups:   , , ,   , , ,   , ,

Proof of Theorem fseqenlem1
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 5871 . . . . . 6
2 f1eq1 5781 . . . . . 6
31, 2syl 16 . . . . 5
4 oveq2 6304 . . . . . 6
5 f1eq2 5782 . . . . . 6
64, 5syl 16 . . . . 5
73, 6bitrd 253 . . . 4
87imbi2d 316 . . 3
9 fveq2 5871 . . . . . . 7
10 snex 4693 . . . . . . . 8
11 fseqenlem.g . . . . . . . . 9
1211seqom0g 7140 . . . . . . . 8
1310, 12ax-mp 5 . . . . . . 7
149, 13syl6eq 2514 . . . . . 6
15 f1eq1 5781 . . . . . 6
1614, 15syl 16 . . . . 5
17 oveq2 6304 . . . . . 6
18 f1eq2 5782 . . . . . 6
1917, 18syl 16 . . . . 5
2016, 19bitrd 253 . . . 4
21 fveq2 5871 . . . . . 6
22 f1eq1 5781 . . . . . 6
2321, 22syl 16 . . . . 5
24 oveq2 6304 . . . . . 6
25 f1eq2 5782 . . . . . 6
2624, 25syl 16 . . . . 5
2723, 26bitrd 253 . . . 4
28 fveq2 5871 . . . . . 6
29 f1eq1 5781 . . . . . 6
3028, 29syl 16 . . . . 5
31 oveq2 6304 . . . . . 6
32 f1eq2 5782 . . . . . 6
3331, 32syl 16 . . . . 5
3430, 33bitrd 253 . . . 4
35 0ex 4582 . . . . . . . 8
36 fseqenlem.b . . . . . . . 8
37 f1osng 5859 . . . . . . . 8
3835, 36, 37sylancr 663 . . . . . . 7
39 f1of1 5820 . . . . . . 7
4038, 39syl 16 . . . . . 6
4136snssd 4175 . . . . . 6
42 f1ss 5791 . . . . . 6
4340, 41, 42syl2anc 661 . . . . 5
44 fseqenlem.a . . . . . . . 8
45 map0e 7476 . . . . . . . 8
4644, 45syl 16 . . . . . . 7
47 df1o2 7161 . . . . . . 7
4846, 47syl6eq 2514 . . . . . 6
49 f1eq2 5782 . . . . . 6
5048, 49syl 16 . . . . 5
5143, 50mpbird 232 . . . 4
52 fseqenlem.f . . . . . . . . . . . 12
5352ad2antrr 725 . . . . . . . . . . 11
54 f1of 5821 . . . . . . . . . . 11
5553, 54syl 16 . . . . . . . . . 10
56 f1f 5786 . . . . . . . . . . . . 13
5756ad2antll 728 . . . . . . . . . . . 12
5857adantr 465 . . . . . . . . . . 11
59 elmapi 7460 . . . . . . . . . . . . . 14
6059adantl 466 . . . . . . . . . . . . 13
61 sssucid 4960 . . . . . . . . . . . . 13
62 fssres 5756 . . . . . . . . . . . . 13
6360, 61, 62sylancl 662 . . . . . . . . . . . 12
6444ad2antrr 725 . . . . . . . . . . . . 13
65 vex 3112 . . . . . . . . . . . . 13
66 elmapg 7452 . . . . . . . . . . . . 13
6764, 65, 66sylancl 662 . . . . . . . . . . . 12
6863, 67mpbird 232 . . . . . . . . . . 11
6958, 68ffvelrnd 6032 . . . . . . . . . 10
7065sucid 4962 . . . . . . . . . . 11
71 ffvelrn 6029 . . . . . . . . . . 11
7260, 70, 71sylancl 662 . . . . . . . . . 10
7355, 69, 72fovrnd 6447 . . . . . . . . 9
74 eqid 2457 . . . . . . . . 9
7573, 74fmptd 6055 . . . . . . . 8
7611seqomsuc 7141 . . . . . . . . . . 11
7776ad2antrl 727 . . . . . . . . . 10
78 fvex 5881 . . . . . . . . . . 11
79 reseq1 5272 . . . . . . . . . . . . . . . 16
8079fveq2d 5875 . . . . . . . . . . . . . . 15
81 fveq1 5870 . . . . . . . . . . . . . . 15
8280, 81oveq12d 6314 . . . . . . . . . . . . . 14
8382cbvmptv 4543 . . . . . . . . . . . . 13
84 suceq 4948 . . . . . . . . . . . . . . . 16
8584adantr 465 . . . . . . . . . . . . . . 15
8685oveq2d 6312 . . . . . . . . . . . . . 14
87 simpr 461 . . . . . . . . . . . . . . . 16
88 reseq2 5273 . . . . . . . . . . . . . . . . 17
8988adantr 465 . . . . . . . . . . . . . . . 16
9087, 89fveq12d 5877 . . . . . . . . . . . . . . 15
91 simpl 457 . . . . . . . . . . . . . . . 16
9291fveq2d 5875 . . . . . . . . . . . . . . 15
9390, 92oveq12d 6314 . . . . . . . . . . . . . 14
9486, 93mpteq12dv 4530 . . . . . . . . . . . . 13
9583, 94syl5eq 2510 . . . . . . . . . . . 12
96 nfcv 2619 . . . . . . . . . . . . 13
97 nfcv 2619 . . . . . . . . . . . . 13
98 nfcv 2619 . . . . . . . . . . . . 13
99 nfcv 2619 . . . . . . . . . . . . 13
100 suceq 4948 . . . . . . . . . . . . . . . 16
101100adantr 465 . . . . . . . . . . . . . . 15
102101oveq2d 6312 . . . . . . . . . . . . . 14
103 simpr 461 . . . . . . . . . . . . . . . 16
104 reseq2 5273 . . . . . . . . . . . . . . . . 17
105104adantr 465 . . . . . . . . . . . . . . . 16
106103, 105fveq12d 5877 . . . . . . . . . . . . . . 15
107 simpl 457 . . . . . . . . . . . . . . . 16
108107fveq2d 5875 . . . . . . . . . . . . . . 15
109106, 108oveq12d 6314 . . . . . . . . . . . . . 14
110102, 109mpteq12dv 4530 . . . . . . . . . . . . 13
11196, 97, 98, 99, 110cbvmpt2 6376 . . . . . . . . . . . 12
112 ovex 6324 . . . . . . . . . . . . 13
113112mptex 6143 . . . . . . . . . . . 12
11495, 111, 113ovmpt2a 6433 . . . . . . . . . . 11
11565, 78, 114mp2an 672 . . . . . . . . . 10
11677, 115syl6eq 2514 . . . . . . . . 9
117116feq1d 5722 . . . . . . . 8
11875, 117mpbird 232 . . . . . . 7
119 elmapi 7460 . . . . . . . . . . . . . 14
120119ad2antrl 727 . . . . . . . . . . . . 13
121 ffn 5736 . . . . . . . . . . . . 13
122120, 121syl 16 . . . . . . . . . . . 12
123 elmapi 7460 . . . . . . . . . . . . . 14
124123ad2antll 728 . . . . . . . . . . . . 13
125 ffn 5736 . . . . . . . . . . . . 13
126124, 125syl 16 . . . . . . . . . . . 12
12761a1i 11 . . . . . . . . . . . 12
128 fvreseq 5989 . . . . . . . . . . . 12
129122, 126, 127, 128syl21anc 1227 . . . . . . . . . . 11
130 fveq2 5871 . . . . . . . . . . . . . . 15
131 fveq2 5871 . . . . . . . . . . . . . . 15
132130, 131eqeq12d 2479 . . . . . . . . . . . . . 14
13365, 132ralsn 4068 . . . . . . . . . . . . 13
134133bicomi 202 . . . . . . . . . . . 12
135134a1i 11 . . . . . . . . . . 11
136129, 135anbi12d 710 . . . . . . . . . 10
137116adantr 465 . . . . . . . . . . . . . . 15
138137fveq1d 5873 . . . . . . . . . . . . . 14
139 reseq1 5272 . . . . . . . . . . . . . . . . . 18
140139fveq2d 5875 . . . . . . . . . . . . . . . . 17
141 fveq1 5870 . . . . . . . . . . . . . . . . 17
142140, 141oveq12d 6314 . . . . . . . . . . . . . . . 16
143 ovex 6324 . . . . . . . . . . . . . . . 16
144142, 74, 143fvmpt 5956 . . . . . . . . . . . . . . 15
145144ad2antrl 727 . . . . . . . . . . . . . 14
146138, 145eqtrd 2498 . . . . . . . . . . . . 13
147 df-ov 6299 . . . . . . . . . . . . 13
148146, 147syl6eq 2514 . . . . . . . . . . . 12
149137fveq1d 5873 . . . . . . . . . . . . . 14
150 reseq1 5272 . . . . . . . . . . . . . . . . . 18
151150fveq2d 5875 . . . . . . . . . . . . . . . . 17
152 fveq1 5870 . . . . . . . . . . . . . . . . 17
153151, 152oveq12d 6314 . . . . . . . . . . . . . . . 16
154 ovex 6324 . . . . . . . . . . . . . . . 16
155153, 74, 154fvmpt 5956 . . . . . . . . . . . . . . 15
156155ad2antll 728 . . . . . . . . . . . . . 14
157149, 156eqtrd 2498 . . . . . . . . . . . . 13
158 df-ov 6299 . . . . . . . . . . . . 13
159157, 158syl6eq 2514 . . . . . . . . . . . 12
160148, 159eqeq12d 2479 . . . . . . . . . . 11
16152ad2antrr 725 . . . . . . . . . . . . . 14
162 f1of1 5820 . . . . . . . . . . . . . 14
163161, 162syl 16 . . . . . . . . . . . . 13
16457adantr 465 . . . . . . . . . . . . . . 15
165 fssres 5756 . . . . . . . . . . . . . . . . 17
166120, 61, 165sylancl 662 . . . . . . . . . . . . . . . 16
16744ad2antrr 725 . . . . . . . . . . . . . . . . 17
168 elmapg 7452 . . . . . . . . . . . . . . . . 17
169167, 65, 168sylancl 662 . . . . . . . . . . . . . . . 16
170166, 169mpbird 232 . . . . . . . . . . . . . . 15
171164, 170ffvelrnd 6032 . . . . . . . . . . . . . 14
172 ffvelrn 6029 . . . . . . . . . . . . . . 15
173120, 70, 172sylancl 662 . . . . . . . . . . . . . 14
174 opelxpi 5036 . . . . . . . . . . . . . 14
175171, 173, 174syl2anc 661 . . . . . . . . . . . . 13
176 fssres 5756 . . . . . . . . . . . . . . . . 17
177124, 61, 176sylancl 662 . . . . . . . . . . . . . . . 16
178 elmapg 7452 . . . . . . . . . . . . . . . . 17
179167, 65, 178sylancl 662 . . . . . . . . . . . . . . . 16
180177, 179mpbird 232 . . . . . . . . . . . . . . 15
181164, 180ffvelrnd 6032 . . . . . . . . . . . . . 14
182 ffvelrn 6029 . . . . . . . . . . . . . . 15
183124, 70, 182sylancl 662 . . . . . . . . . . . . . 14
184 opelxpi 5036 . . . . . . . . . . . . . 14
185181, 183, 184syl2anc 661 . . . . . . . . . . . . 13
186 f1fveq 6170 . . . . . . . . . . . . 13
187163, 175, 185, 186syl12anc 1226 . . . . . . . . . . . 12
188 fvex 5881 . . . . . . . . . . . . 13
189 fvex 5881 . . . . . . . . . . . . 13
190188, 189opth 4726 . . . . . . . . . . . 12