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

Theorem o1compt 12157
 Description: Sufficient condition for transforming the index set of an eventually bounded function. (Contributed by Mario Carneiro, 12-May-2016.)
Hypotheses
Ref Expression
o1compt.1
o1compt.2
o1compt.3
o1compt.4
o1compt.5
Assertion
Ref Expression
o1compt
Distinct variable groups:   ,,,   ,,,   ,,   ,,,   ,,
Allowed substitution hints:   ()   ()

Proof of Theorem o1compt
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 o1compt.1 . 2
2 o1compt.2 . 2
3 o1compt.3 . . 3
4 eqid 2358 . . 3
53, 4fmptd 5767 . 2
6 o1compt.4 . 2
7 o1compt.5 . . 3
8 nfv 1619 . . . . . . . 8
9 nfcv 2494 . . . . . . . . 9
10 nfcv 2494 . . . . . . . . 9
11 nfmpt1 4190 . . . . . . . . . 10
12 nfcv 2494 . . . . . . . . . 10
1311, 12nffv 5615 . . . . . . . . 9
149, 10, 13nfbr 4148 . . . . . . . 8
158, 14nfim 1815 . . . . . . 7
16 nfv 1619 . . . . . . 7
17 breq2 4108 . . . . . . . 8
18 fveq2 5608 . . . . . . . . 9
1918breq2d 4116 . . . . . . . 8
2017, 19imbi12d 311 . . . . . . 7
2115, 16, 20cbvral 2836 . . . . . 6
22 simpr 447 . . . . . . . . . 10
234fvmpt2 5691 . . . . . . . . . 10
2422, 3, 23syl2anc 642 . . . . . . . . 9
2524breq2d 4116 . . . . . . . 8
2625imbi2d 307 . . . . . . 7
2726ralbidva 2635 . . . . . 6
2821, 27syl5bb 248 . . . . 5
2928rexbidv 2640 . . . 4