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

Theorem limcfval 19708
 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 19702 . . . 4 lim fld t
21a1i 11 . . 3 lim fld t
3 fvex 5699 . . . . . 6 fld
43a1i 11 . . . . 5 fld
5 simplrl 737 . . . . . . . . . 10 fld
65dmeqd 5029 . . . . . . . . 9 fld
7 simpll1 996 . . . . . . . . . 10 fld
8 fdm 5552 . . . . . . . . . 10
97, 8syl 16 . . . . . . . . 9 fld
106, 9eqtrd 2434 . . . . . . . 8 fld
11 simplrr 738 . . . . . . . . 9 fld
1211sneqd 3785 . . . . . . . 8 fld
1310, 12uneq12d 3460 . . . . . . 7 fld
1411eqeq2d 2413 . . . . . . . 8 fld
155fveq1d 5687 . . . . . . . 8 fld
1614, 15ifbieq2d 3717 . . . . . . 7 fld
1713, 16mpteq12dv 4245 . . . . . 6 fld
18 simpr 448 . . . . . . . . . . 11 fld fld
19 limcval.k . . . . . . . . . . 11 fld
2018, 19syl6eqr 2452 . . . . . . . . . 10 fld
2120, 13oveq12d 6056 . . . . . . . . 9 fld t t
22 limcval.j . . . . . . . . 9 t
2321, 22syl6eqr 2452 . . . . . . . 8 fld t
2423, 20oveq12d 6056 . . . . . . 7 fld t
2524, 11fveq12d 5691 . . . . . 6 fld t
2617, 25eleq12d 2470 . . . . 5 fld t
274, 26sbcied 3155 . . . 4 fld t
2827abbidv 2516 . . 3 fld t
29 cnex 9025 . . . . 5
30 elpm2r 6991 . . . . 5
3129, 29, 30mpanl12 664 . . . 4