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

Theorem o1compt 12373
 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 2435 . . 3
53, 4fmptd 5885 . 2
6 o1compt.4 . 2
7 o1compt.5 . . 3
8 nfv 1629 . . . . . . . 8
9 nfcv 2571 . . . . . . . . 9
10 nfcv 2571 . . . . . . . . 9
11 nffvmpt1 5728 . . . . . . . . 9
129, 10, 11nfbr 4248 . . . . . . . 8
138, 12nfim 1832 . . . . . . 7
14 nfv 1629 . . . . . . 7
15 breq2 4208 . . . . . . . 8
16 fveq2 5720 . . . . . . . . 9
1716breq2d 4216 . . . . . . . 8
1815, 17imbi12d 312 . . . . . . 7
1913, 14, 18cbvral 2920 . . . . . 6
20 simpr 448 . . . . . . . . . 10
214fvmpt2 5804 . . . . . . . . . 10
2220, 3, 21syl2anc 643 . . . . . . . . 9
2322breq2d 4216 . . . . . . . 8
2423imbi2d 308 . . . . . . 7
2524ralbidva 2713 . . . . . 6
2619, 25syl5bb 249 . . . . 5
2726rexbidv 2718 . . . 4