Description: Lemma for caucvgr . (Contributed by NM, 4-Apr-2005) (Proof shortened by Mario Carneiro, 8-May-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | caucvgr.1 | |
|
caucvgr.2 | |
||
caucvgr.3 | |
||
caucvgr.4 | |
||
caucvgrlem2.5 | |
||
caucvgrlem2.6 | |
||
Assertion | caucvgrlem2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | caucvgr.1 | |
|
2 | caucvgr.2 | |
|
3 | caucvgr.3 | |
|
4 | caucvgr.4 | |
|
5 | caucvgrlem2.5 | |
|
6 | caucvgrlem2.6 | |
|
7 | fcompt | |
|
8 | 5 2 7 | sylancr | |
9 | fco | |
|
10 | 5 2 9 | sylancr | |
11 | 2 | ad2antrr | |
12 | simprr | |
|
13 | 11 12 | ffvelrnd | |
14 | simprl | |
|
15 | 11 14 | ffvelrnd | |
16 | 13 15 6 | syl2anc | |
17 | 5 | ffvelrni | |
18 | 13 17 | syl | |
19 | 5 | ffvelrni | |
20 | 15 19 | syl | |
21 | 18 20 | resubcld | |
22 | 21 | recnd | |
23 | 22 | abscld | |
24 | 13 15 | subcld | |
25 | 24 | abscld | |
26 | rpre | |
|
27 | 26 | ad2antlr | |
28 | lelttr | |
|
29 | 23 25 27 28 | syl3anc | |
30 | 16 29 | mpand | |
31 | fvco3 | |
|
32 | 11 12 31 | syl2anc | |
33 | fvco3 | |
|
34 | 11 14 33 | syl2anc | |
35 | 32 34 | oveq12d | |
36 | 35 | fveq2d | |
37 | 36 | breq1d | |
38 | 30 37 | sylibrd | |
39 | 38 | imim2d | |
40 | 39 | anassrs | |
41 | 40 | ralimdva | |
42 | 41 | reximdva | |
43 | 42 | ralimdva | |
44 | 4 43 | mpd | |
45 | 1 10 3 44 | caurcvgr | |
46 | rlimrel | |
|
47 | 46 | releldmi | |
48 | 45 47 | syl | |
49 | ax-resscn | |
|
50 | fss | |
|
51 | 10 49 50 | sylancl | |
52 | 51 3 | rlimdm | |
53 | 48 52 | mpbid | |
54 | 8 53 | eqbrtrrd | |