Metamath Proof Explorer


Theorem limcmpt2

Description: Express the limit operator for a function defined by a mapping. (Contributed by Mario Carneiro, 25-Dec-2016)

Ref Expression
Hypotheses limcmpt2.a φ A
limcmpt2.b φ B A
limcmpt2.f φ z A z B D
limcmpt2.j J = K 𝑡 A
limcmpt2.k K = TopOpen fld
Assertion limcmpt2 φ C z A B D lim B z A if z = B C D J CnP K B

Proof

Step Hyp Ref Expression
1 limcmpt2.a φ A
2 limcmpt2.b φ B A
3 limcmpt2.f φ z A z B D
4 limcmpt2.j J = K 𝑡 A
5 limcmpt2.k K = TopOpen fld
6 1 ssdifssd φ A B
7 1 2 sseldd φ B
8 eldifsn z A B z A z B
9 8 3 sylan2b φ z A B D
10 eqid K 𝑡 A B B = K 𝑡 A B B
11 6 7 9 10 5 limcmpt φ C z A B D lim B z A B B if z = B C D K 𝑡 A B B CnP K B
12 undif1 A B B = A B
13 2 snssd φ B A
14 ssequn2 B A A B = A
15 13 14 sylib φ A B = A
16 12 15 syl5eq φ A B B = A
17 16 mpteq1d φ z A B B if z = B C D = z A if z = B C D
18 16 oveq2d φ K 𝑡 A B B = K 𝑡 A
19 18 4 eqtr4di φ K 𝑡 A B B = J
20 19 oveq1d φ K 𝑡 A B B CnP K = J CnP K
21 20 fveq1d φ K 𝑡 A B B CnP K B = J CnP K B
22 17 21 eleq12d φ z A B B if z = B C D K 𝑡 A B B CnP K B z A if z = B C D J CnP K B
23 11 22 bitrd φ C z A B D lim B z A if z = B C D J CnP K B