Metamath Proof Explorer


Theorem climcn1

Description: Image of a limit under a continuous map. (Contributed by Mario Carneiro, 31-Jan-2014)

Ref Expression
Hypotheses climcn1.1 Z=M
climcn1.2 φM
climcn1.3 φAB
climcn1.4 φzBFz
climcn1.5 φGA
climcn1.6 φHW
climcn1.7 φx+y+zBzA<yFzFA<x
climcn1.8 φkZGkB
climcn1.9 φkZHk=FGk
Assertion climcn1 φHFA

Proof

Step Hyp Ref Expression
1 climcn1.1 Z=M
2 climcn1.2 φM
3 climcn1.3 φAB
4 climcn1.4 φzBFz
5 climcn1.5 φGA
6 climcn1.6 φHW
7 climcn1.7 φx+y+zBzA<yFzFA<x
8 climcn1.8 φkZGkB
9 climcn1.9 φkZHk=FGk
10 2 adantr φy+M
11 simpr φy+y+
12 eqidd φy+kZGk=Gk
13 5 adantr φy+GA
14 1 10 11 12 13 climi2 φy+jZkjGkA<y
15 1 uztrn2 jZkjkZ
16 8 adantlr φy+kZGkB
17 fvoveq1 z=GkzA=GkA
18 17 breq1d z=GkzA<yGkA<y
19 18 imbrov2fvoveq z=GkzA<yFzFA<xGkA<yFGkFA<x
20 19 rspcva GkBzBzA<yFzFA<xGkA<yFGkFA<x
21 16 20 sylan φy+kZzBzA<yFzFA<xGkA<yFGkFA<x
22 21 an32s φy+zBzA<yFzFA<xkZGkA<yFGkFA<x
23 15 22 sylan2 φy+zBzA<yFzFA<xjZkjGkA<yFGkFA<x
24 23 anassrs φy+zBzA<yFzFA<xjZkjGkA<yFGkFA<x
25 24 ralimdva φy+zBzA<yFzFA<xjZkjGkA<ykjFGkFA<x
26 25 reximdva φy+zBzA<yFzFA<xjZkjGkA<yjZkjFGkFA<x
27 26 ex φy+zBzA<yFzFA<xjZkjGkA<yjZkjFGkFA<x
28 14 27 mpid φy+zBzA<yFzFA<xjZkjFGkFA<x
29 28 rexlimdva φy+zBzA<yFzFA<xjZkjFGkFA<x
30 29 adantr φx+y+zBzA<yFzFA<xjZkjFGkFA<x
31 7 30 mpd φx+jZkjFGkFA<x
32 31 ralrimiva φx+jZkjFGkFA<x
33 fveq2 z=AFz=FA
34 33 eleq1d z=AFzFA
35 4 ralrimiva φzBFz
36 34 35 3 rspcdva φFA
37 fveq2 z=GkFz=FGk
38 37 eleq1d z=GkFzFGk
39 35 adantr φkZzBFz
40 38 39 8 rspcdva φkZFGk
41 1 2 6 9 36 40 clim2c φHFAx+jZkjFGkFA<x
42 32 41 mpbird φHFA