Theorem lmcnp 20369

Description: The image of a convergent sequence under a continuous map is convergent to the image of the original point. (Contributed by Mario Carneiro, 3-May-2014.)

Hypotheses

Ref	Expression
lmcnp.3	|- ( ph -> F ( ~~> t ` J ) P )
lmcnp.4	|- ( ph -> G e. ( ( J CnP K ) ` P ) )

Assertion

Ref	Expression
lmcnp	|- ( ph -> ( G o. F ) ( ~~> t ` K ) ( G ` P ) )

Proof of Theorem lmcnp

Dummy variables j k u v are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		lmcnp.4	. . . . . 6 |- ( ph -> G e. ( ( J CnP K ) ` P ) )
2		eqid 2462	. . . . . . 7 |- U. J = U. J
3		eqid 2462	. . . . . . 7 |- U. K = U. K
4	2, 3	cnpf 20312	. . . . . 6 |- ( G e. ( ( J CnP K ) ` P ) -> G : U. J --> U. K )
5	1, 4	syl 17	. . . . 5 |- ( ph -> G : U. J --> U. K )
6		lmcnp.3	. . . . . . . . 9 |- ( ph -> F ( ~~> t ` J ) P )
7		cnptop1 20307	. . . . . . . . . . . 12 |- ( G e. ( ( J CnP K ) ` P ) -> J e. Top )
8	1, 7	syl 17	. . . . . . . . . . 11 |- ( ph -> J e. Top )
9	2	toptopon 19997	. . . . . . . . . . 11 |- ( J e. Top <-> J e. (TopOn ` U. J ) )
10	8, 9	sylib 201	. . . . . . . . . 10 |- ( ph -> J e. (TopOn ` U. J ) )
11		nnuz 11223	. . . . . . . . . 10 |- NN = ( ZZ>= ` 1 )
12		1zzd 10997	. . . . . . . . . 10 |- ( ph -> 1 e. ZZ )
13	10, 11, 12	lmbr2 20324	. . . . . . . . 9 |- ( ph -> ( F ( ~~> t ` J ) P <-> ( F e. ( U. J ^pm CC ) /\ P e. U. J /\ A. v e. J ( P e. v -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) ) ) ) )
14	6, 13	mpbid 215	. . . . . . . 8 |- ( ph -> ( F e. ( U. J ^pm CC ) /\ P e. U. J /\ A. v e. J ( P e. v -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) ) ) )
15	14	simp1d 1026	. . . . . . 7 |- ( ph -> F e. ( U. J ^pm CC ) )
16		uniexg 6615	. . . . . . . . 9 |- ( J e. Top -> U. J e. _V )
17	8, 16	syl 17	. . . . . . . 8 |- ( ph -> U. J e. _V )
18		cnex 9646	. . . . . . . 8 |- CC e. _V
19		elpm2g 7514	. . . . . . . 8 |- ( ( U. J e. _V /\ CC e. _V ) -> ( F e. ( U. J ^pm CC ) <-> ( F : dom F --> U. J /\ dom F C_ CC ) ) )
20	17, 18, 19	sylancl 673	. . . . . . 7 |- ( ph -> ( F e. ( U. J ^pm CC ) <-> ( F : dom F --> U. J /\ dom F C_ CC ) ) )
21	15, 20	mpbid 215	. . . . . 6 |- ( ph -> ( F : dom F --> U. J /\ dom F C_ CC ) )
22	21	simpld 465	. . . . 5 |- ( ph -> F : dom F --> U. J )
23		fco 5762	. . . . 5 |- ( ( G : U. J --> U. K /\ F : dom F --> U. J ) -> ( G o. F ) : dom F --> U. K )
24	5, 22, 23	syl2anc 671	. . . 4 |- ( ph -> ( G o. F ) : dom F --> U. K )
25		fdm 5756	. . . . . 6 |- ( ( G o. F ) : dom F --> U. K -> dom ( G o. F ) = dom F )
26	24, 25	syl 17	. . . . 5 |- ( ph -> dom ( G o. F ) = dom F )
27	26	feq2d 5737	. . . 4 |- ( ph -> ( ( G o. F ) : dom ( G o. F ) --> U. K <-> ( G o. F ) : dom F --> U. K ) )
28	24, 27	mpbird 240	. . 3 |- ( ph -> ( G o. F ) : dom ( G o. F ) --> U. K )
29	21	simprd 469	. . . 4 |- ( ph -> dom F C_ CC )
30	26, 29	eqsstrd 3478	. . 3 |- ( ph -> dom ( G o. F ) C_ CC )
31		cnptop2 20308	. . . . . 6 |- ( G e. ( ( J CnP K ) ` P ) -> K e. Top )
32	1, 31	syl 17	. . . . 5 |- ( ph -> K e. Top )
33		uniexg 6615	. . . . 5 |- ( K e. Top -> U. K e. _V )
34	32, 33	syl 17	. . . 4 |- ( ph -> U. K e. _V )
35		elpm2g 7514	. . . 4 |- ( ( U. K e. _V /\ CC e. _V ) -> ( ( G o. F ) e. ( U. K ^pm CC ) <-> ( ( G o. F ) : dom ( G o. F ) --> U. K /\ dom ( G o. F ) C_ CC ) ) )
36	34, 18, 35	sylancl 673	. . 3 |- ( ph -> ( ( G o. F ) e. ( U. K ^pm CC ) <-> ( ( G o. F ) : dom ( G o. F ) --> U. K /\ dom ( G o. F ) C_ CC ) ) )
37	28, 30, 36	mpbir2and 938	. 2 |- ( ph -> ( G o. F ) e. ( U. K ^pm CC ) )
38	14	simp2d 1027	. . 3 |- ( ph -> P e. U. J )
39	5, 38	ffvelrnd 6046	. 2 |- ( ph -> ( G ` P ) e. U. K )
40	14	simp3d 1028	. . . . . 6 |- ( ph -> A. v e. J ( P e. v -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) ) )
41	40	adantr 471	. . . . 5 |- ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) -> A. v e. J ( P e. v -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) ) )
42		cnpimaex 20321	. . . . . . 7 |- ( ( G e. ( ( J CnP K ) ` P ) /\ u e. K /\ ( G ` P ) e. u ) -> E. v e. J ( P e. v /\ ( G " v ) C_ u ) )
43	42	3expb 1216	. . . . . 6 |- ( ( G e. ( ( J CnP K ) ` P ) /\ ( u e. K /\ ( G ` P ) e. u ) ) -> E. v e. J ( P e. v /\ ( G " v ) C_ u ) )
44	1, 43	sylan 478	. . . . 5 |- ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) -> E. v e. J ( P e. v /\ ( G " v ) C_ u ) )
45		r19.29 2937	. . . . . . 7 |- ( ( A. v e. J ( P e. v -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) ) /\ E. v e. J ( P e. v /\ ( G " v ) C_ u ) ) -> E. v e. J ( ( P e. v -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) ) /\ ( P e. v /\ ( G " v ) C_ u ) ) )
46		pm3.45 850	. . . . . . . . 9 |- ( ( P e. v -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) ) -> ( ( P e. v /\ ( G " v ) C_ u ) -> ( E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) /\ ( G " v ) C_ u ) ) )
47	46	imp 435	. . . . . . . 8 |- ( ( ( P e. v -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) ) /\ ( P e. v /\ ( G " v ) C_ u ) ) -> ( E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) /\ ( G " v ) C_ u ) )
48	47	reximi 2867	. . . . . . 7 |- ( E. v e. J ( ( P e. v -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) ) /\ ( P e. v /\ ( G " v ) C_ u ) ) -> E. v e. J ( E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) /\ ( G " v ) C_ u ) )
49	45, 48	syl 17	. . . . . 6 |- ( ( A. v e. J ( P e. v -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) ) /\ E. v e. J ( P e. v /\ ( G " v ) C_ u ) ) -> E. v e. J ( E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) /\ ( G " v ) C_ u ) )
50	5	ad3antrrr 741	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) /\ k e. dom F ) -> G : U. J --> U. K )
51		ffn 5751	. . . . . . . . . . . . . . . . . 18 |- ( G : U. J --> U. K -> G Fn U. J )
52	50, 51	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) /\ k e. dom F ) -> G Fn U. J )
53		simplrl 775	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) /\ k e. dom F ) -> v e. J )
54		elssuni 4241	. . . . . . . . . . . . . . . . . 18 |- ( v e. J -> v C_ U. J )
55	53, 54	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) /\ k e. dom F ) -> v C_ U. J )
56		fnfvima 6168	. . . . . . . . . . . . . . . . . 18 |- ( ( G Fn U. J /\ v C_ U. J /\ ( F ` k ) e. v ) -> ( G ` ( F ` k ) ) e. ( G " v ) )
57	56	3expia 1217	. . . . . . . . . . . . . . . . 17 |- ( ( G Fn U. J /\ v C_ U. J ) -> ( ( F ` k ) e. v -> ( G ` ( F ` k ) ) e. ( G " v ) ) )
58	52, 55, 57	syl2anc 671	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) /\ k e. dom F ) -> ( ( F ` k ) e. v -> ( G ` ( F ` k ) ) e. ( G " v ) ) )
59	22	ad2antrr 737	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) -> F : dom F --> U. J )
60		fvco3 5965	. . . . . . . . . . . . . . . . . 18 |- ( ( F : dom F --> U. J /\ k e. dom F ) -> ( ( G o. F ) ` k ) = ( G ` ( F ` k ) ) )
61	59, 60	sylan 478	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) /\ k e. dom F ) -> ( ( G o. F ) ` k ) = ( G ` ( F ` k ) ) )
62	61	eleq1d 2524	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) /\ k e. dom F ) -> ( ( ( G o. F ) ` k ) e. ( G " v ) <-> ( G ` ( F ` k ) ) e. ( G " v ) ) )
63	58, 62	sylibrd 242	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) /\ k e. dom F ) -> ( ( F ` k ) e. v -> ( ( G o. F ) ` k ) e. ( G " v ) ) )
64		simplrr 776	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) /\ k e. dom F ) -> ( G " v ) C_ u )
65	64	sseld 3443	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) /\ k e. dom F ) -> ( ( ( G o. F ) ` k ) e. ( G " v ) -> ( ( G o. F ) ` k ) e. u ) )
66	63, 65	syld 45	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) /\ k e. dom F ) -> ( ( F ` k ) e. v -> ( ( G o. F ) ` k ) e. u ) )
67		simpr 467	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) /\ k e. dom F ) -> k e. dom F )
68	26	ad3antrrr 741	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) /\ k e. dom F ) -> dom ( G o. F ) = dom F )
69	67, 68	eleqtrrd 2543	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) /\ k e. dom F ) -> k e. dom ( G o. F ) )
70	66, 69	jctild 550	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) /\ k e. dom F ) -> ( ( F ` k ) e. v -> ( k e. dom ( G o. F ) /\ ( ( G o. F ) ` k ) e. u ) ) )
71	70	expimpd 612	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) -> ( ( k e. dom F /\ ( F ` k ) e. v ) -> ( k e. dom ( G o. F ) /\ ( ( G o. F ) ` k ) e. u ) ) )
72	71	ralimdv 2810	. . . . . . . . . . 11 |- ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) -> A. k e. ( ZZ>= ` j ) ( k e. dom ( G o. F ) /\ ( ( G o. F ) ` k ) e. u ) ) )
73	72	reximdv 2873	. . . . . . . . . 10 |- ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ ( v e. J /\ ( G " v ) C_ u ) ) -> ( E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom ( G o. F ) /\ ( ( G o. F ) ` k ) e. u ) ) )
74	73	expr 624	. . . . . . . . 9 |- ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ v e. J ) -> ( ( G " v ) C_ u -> ( E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom ( G o. F ) /\ ( ( G o. F ) ` k ) e. u ) ) ) )
75	74	com23 81	. . . . . . . 8 |- ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ v e. J ) -> ( E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) -> ( ( G " v ) C_ u -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom ( G o. F ) /\ ( ( G o. F ) ` k ) e. u ) ) ) )
76	75	impd 437	. . . . . . 7 |- ( ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) /\ v e. J ) -> ( ( E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) /\ ( G " v ) C_ u ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom ( G o. F ) /\ ( ( G o. F ) ` k ) e. u ) ) )
77	76	rexlimdva 2891	. . . . . 6 |- ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) -> ( E. v e. J ( E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) /\ ( G " v ) C_ u ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom ( G o. F ) /\ ( ( G o. F ) ` k ) e. u ) ) )
78	49, 77	syl5 33	. . . . 5 |- ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) -> ( ( A. v e. J ( P e. v -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. v ) ) /\ E. v e. J ( P e. v /\ ( G " v ) C_ u ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom ( G o. F ) /\ ( ( G o. F ) ` k ) e. u ) ) )
79	41, 44, 78	mp2and 690	. . . 4 |- ( ( ph /\ ( u e. K /\ ( G ` P ) e. u ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom ( G o. F ) /\ ( ( G o. F ) ` k ) e. u ) )
80	79	expr 624	. . 3 |- ( ( ph /\ u e. K ) -> ( ( G ` P ) e. u -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom ( G o. F ) /\ ( ( G o. F ) ` k ) e. u ) ) )
81	80	ralrimiva 2814	. 2 |- ( ph -> A. u e. K ( ( G ` P ) e. u -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom ( G o. F ) /\ ( ( G o. F ) ` k ) e. u ) ) )
82	3	toptopon 19997	. . . 4 |- ( K e. Top <-> K e. (TopOn ` U. K ) )
83	32, 82	sylib 201	. . 3 |- ( ph -> K e. (TopOn ` U. K ) )
84	83, 11, 12	lmbr2 20324	. 2 |- ( ph -> ( ( G o. F ) ( ~~> t ` K ) ( G ` P ) <-> ( ( G o. F ) e. ( U. K ^pm CC ) /\ ( G ` P ) e. U. K /\ A. u e. K ( ( G ` P ) e. u -> E. j e. NN A. k e. ( ZZ>= ` j ) ( k e. dom ( G o. F ) /\ ( ( G o. F ) ` k ) e. u ) ) ) ) )
85	37, 39, 81, 84	mpbir3and 1197	1 |- ( ph -> ( G o. F ) ( ~~> t ` K ) ( G ` P ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375   /\ w3a 991   = wceq 1455   e. wcel 1898   A.wral 2749   E.wrex 2750   _Vcvv 3057   C_ wss 3416   U.cuni 4212   class class class wbr 4416   dom cdm 4853   "cima 4856   o. ccom 4857   Fn wfn 5596   -->wf 5597   ` cfv 5601  (class class class)co 6315   ^pm cpm 7499   CCcc 9563   1c1 9566   NNcn 10637   ZZ>=cuz 11188   Topctop 19966  TopOnctopon 19967   CnP ccnp 20290   ~~> tclm 20291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-cnex 9621  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-mulcom 9629  ax-addass 9630  ax-mulass 9631  ax-distr 9632  ax-i2m1 9633  ax-1ne0 9634  ax-1rid 9635  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638  ax-pre-lttri 9639  ax-pre-lttrn 9640  ax-pre-ltadd 9641  ax-pre-mulgt0 9642

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-iun 4294  df-br 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-om 6720  df-1st 6820  df-2nd 6821  df-wrecs 7054  df-recs 7116  df-rdg 7154  df-er 7389  df-map 7500  df-pm 7501  df-en 7596  df-dom 7597  df-sdom 7598  df-pnf 9703  df-mnf 9704  df-xr 9705  df-ltxr 9706  df-le 9707  df-sub 9888  df-neg 9889  df-nn 10638  df-z 10967  df-uz 11189  df-top 19970  df-topon 19972  df-cnp 20293  df-lm 20294

This theorem is referenced by:  lmcn  20370  1stccnp  20526