Description: Sufficient condition for transforming the index set of an eventually bounded function. (Contributed by Mario Carneiro, 12-May-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | o1compt.1 | |
|
o1compt.2 | |
||
o1compt.3 | |
||
o1compt.4 | |
||
o1compt.5 | |
||
Assertion | o1compt | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | o1compt.1 | |
|
2 | o1compt.2 | |
|
3 | o1compt.3 | |
|
4 | o1compt.4 | |
|
5 | o1compt.5 | |
|
6 | 3 | fmpttd | |
7 | nfv | |
|
8 | nfcv | |
|
9 | nfcv | |
|
10 | nffvmpt1 | |
|
11 | 8 9 10 | nfbr | |
12 | 7 11 | nfim | |
13 | nfv | |
|
14 | breq2 | |
|
15 | fveq2 | |
|
16 | 15 | breq2d | |
17 | 14 16 | imbi12d | |
18 | 12 13 17 | cbvralw | |
19 | simpr | |
|
20 | eqid | |
|
21 | 20 | fvmpt2 | |
22 | 19 3 21 | syl2anc | |
23 | 22 | breq2d | |
24 | 23 | imbi2d | |
25 | 24 | ralbidva | |
26 | 18 25 | syl5bb | |
27 | 26 | rexbidv | |
28 | 27 | adantr | |
29 | 5 28 | mpbird | |
30 | 1 2 6 4 29 | o1co | |