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

Theorem limcfval 22566
 Description: Value and set bounds on the limit operator. (Contributed by Mario Carneiro, 25-Dec-2016.)
Hypotheses
Ref Expression
limcval.j t
limcval.k fld
Assertion
Ref Expression
limcfval lim lim
Distinct variable groups:   ,,   ,,   ,,   ,,   ,
Allowed substitution hint:   ()

Proof of Theorem limcfval
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-limc 22560 . . . 4 lim fld t
21a1i 11 . . 3 lim fld t
3 fvex 5858 . . . . . 6 fld
43a1i 11 . . . . 5 fld
5 simplrl 762 . . . . . . . . . 10 fld
65dmeqd 5025 . . . . . . . . 9 fld
7 simpll1 1036 . . . . . . . . . 10 fld
8 fdm 5717 . . . . . . . . . 10
97, 8syl 17 . . . . . . . . 9 fld
106, 9eqtrd 2443 . . . . . . . 8 fld
11 simplrr 763 . . . . . . . . 9 fld
1211sneqd 3983 . . . . . . . 8 fld
1310, 12uneq12d 3597 . . . . . . 7 fld
1411eqeq2d 2416 . . . . . . . 8 fld
155fveq1d 5850 . . . . . . . 8 fld
1614, 15ifbieq2d 3909 . . . . . . 7 fld
1713, 16mpteq12dv 4472 . . . . . 6 fld
18 simpr 459 . . . . . . . . . . 11 fld fld
19 limcval.k . . . . . . . . . . 11 fld
2018, 19syl6eqr 2461 . . . . . . . . . 10 fld
2120, 13oveq12d 6295 . . . . . . . . 9 fld t t
22 limcval.j . . . . . . . . 9 t
2321, 22syl6eqr 2461 . . . . . . . 8 fld t
2423, 20oveq12d 6295 . . . . . . 7 fld t
2524, 11fveq12d 5854 . . . . . 6 fld t
2617, 25eleq12d 2484 . . . . 5 fld t
274, 26sbcied 3313 . . . 4 fld t
2827abbidv 2538 . . 3 fld t
29 cnex 9602 . . . . 5
30 elpm2r 7473 . . . . 5
3129, 29, 30mpanl12 680 . . . 4