Metamath Proof Explorer


Theorem o1compt

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 φF:A
o1compt.2 φF𝑂1
o1compt.3 φyBCA
o1compt.4 φB
o1compt.5 φmxyBxymC
Assertion o1compt φFyBC𝑂1

Proof

Step Hyp Ref Expression
1 o1compt.1 φF:A
2 o1compt.2 φF𝑂1
3 o1compt.3 φyBCA
4 o1compt.4 φB
5 o1compt.5 φmxyBxymC
6 3 fmpttd φyBC:BA
7 nfv yxz
8 nfcv _ym
9 nfcv _y
10 nffvmpt1 _yyBCz
11 8 9 10 nfbr ymyBCz
12 7 11 nfim yxzmyBCz
13 nfv zxymyBCy
14 breq2 z=yxzxy
15 fveq2 z=yyBCz=yBCy
16 15 breq2d z=ymyBCzmyBCy
17 14 16 imbi12d z=yxzmyBCzxymyBCy
18 12 13 17 cbvralw zBxzmyBCzyBxymyBCy
19 simpr φyByB
20 eqid yBC=yBC
21 20 fvmpt2 yBCAyBCy=C
22 19 3 21 syl2anc φyByBCy=C
23 22 breq2d φyBmyBCymC
24 23 imbi2d φyBxymyBCyxymC
25 24 ralbidva φyBxymyBCyyBxymC
26 18 25 syl5bb φzBxzmyBCzyBxymC
27 26 rexbidv φxzBxzmyBCzxyBxymC
28 27 adantr φmxzBxzmyBCzxyBxymC
29 5 28 mpbird φmxzBxzmyBCz
30 1 2 6 4 29 o1co φFyBC𝑂1