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

Theorem 1stccnp 17478
 Description: A mapping is continuous at in a first-countable space iff it is sequentially continuous at , meaning that the image under of every sequence converging at converges to . This proof uses ax-cc 8271, but only via 1stcelcls 17477, so it could be refactored into a proof that continuity and sequential continuity are the same in sequential spaces. (Contributed by Mario Carneiro, 7-Sep-2015.)
Hypotheses
Ref Expression
1stccnp.1
1stccnp.2 TopOn
1stccnp.3 TopOn
1stccnp.4
Assertion
Ref Expression
1stccnp
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,

Proof of Theorem 1stccnp
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1stccnp.2 . . . . 5 TopOn
2 1stccnp.3 . . . . 5 TopOn
31, 2jca 519 . . . 4 TopOn TopOn
4 cnpf2 17268 . . . . 5 TopOn TopOn
543expa 1153 . . . 4 TopOn TopOn
63, 5sylan 458 . . 3
7 simprr 734 . . . . . 6
8 simplr 732 . . . . . 6
97, 8lmcnp 17322 . . . . 5
109ex 424 . . . 4
1110alrimiv 1638 . . 3
126, 11jca 519 . 2
13 simprl 733 . . 3
14 fal 1328 . . . . . . . . 9
15 19.29 1603 . . . . . . . . . . . . . 14
16 simprl 733 . . . . . . . . . . . . . . . . . . . . 21
17 difss 3434 . . . . . . . . . . . . . . . . . . . . 21
18 fss 5558 . . . . . . . . . . . . . . . . . . . . 21
1916, 17, 18sylancl 644 . . . . . . . . . . . . . . . . . . . 20
20 simprr 734 . . . . . . . . . . . . . . . . . . . 20
2119, 20jca 519 . . . . . . . . . . . . . . . . . . 19
22 nnuz 10477 . . . . . . . . . . . . . . . . . . . . . 22
23 simplrr 738 . . . . . . . . . . . . . . . . . . . . . 22
24 1z 10267 . . . . . . . . . . . . . . . . . . . . . . 23
2524a1i 11 . . . . . . . . . . . . . . . . . . . . . 22
26 simprr 734 . . . . . . . . . . . . . . . . . . . . . 22
27 simplrl 737 . . . . . . . . . . . . . . . . . . . . . 22
2822, 23, 25, 26, 27lmcvg 17280 . . . . . . . . . . . . . . . . . . . . 21
2922r19.2uz 12110 . . . . . . . . . . . . . . . . . . . . . 22
30 simprll 739 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
31 ffn 5550 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
3230, 31syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26
33 fvco2 5757 . . . . . . . . . . . . . . . . . . . . . . . . . 26
3432, 33sylan 458 . . . . . . . . . . . . . . . . . . . . . . . . 25
3534eleq1d 2470 . . . . . . . . . . . . . . . . . . . . . . . 24
3630ffvelrnda 5829 . . . . . . . . . . . . . . . . . . . . . . . . . 26
3736eldifad 3292 . . . . . . . . . . . . . . . . . . . . . . . . 25
38 simplr 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
3938ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
40 ffn 5550 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
41 elpreima 5809 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
4239, 40, 413syl 19 . . . . . . . . . . . . . . . . . . . . . . . . . 26
4336eldifbd 3293 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
4443pm2.21d 100 . . . . . . . . . . . . . . . . . . . . . . . . . 26
4542, 44sylbird 227 . . . . . . . . . . . . . . . . . . . . . . . . 25
4637, 45mpand 657 . . . . . . . . . . . . . . . . . . . . . . . 24
4735, 46sylbid 207 . . . . . . . . . . . . . . . . . . . . . . 23
4847rexlimdva 2790 . . . . . . . . . . . . . . . . . . . . . 22
4929, 48syl5 30 . . . . . . . . . . . . . . . . . . . . 21
5028, 49mpd 15 . . . . . . . . . . . . . . . . . . . 20
5150expr 599 . . . . . . . . . . . . . . . . . . 19
5221, 51embantd 52 . . . . . . . . . . . . . . . . . 18
5352ex 424 . . . . . . . . . . . . . . . . 17
5453com23 74 . . . . . . . . . . . . . . . 16
5554imp3a 421 . . . . . . . . . . . . . . 15
5655exlimdv 1643 . . . . . . . . . . . . . 14
5715, 56syl5 30 . . . . . . . . . . . . 13
5857exp4b 591 . . . . . . . . . . . 12
5958com23 74 . . . . . . . . . . 11
6059impr 603 . . . . . . . . . 10
6160imp 419 . . . . . . . . 9
6214, 61mtoi 171 . . . . . . . 8
63 1stccnp.1 . . . . . . . . . 10
6463ad2antrr 707 . . . . . . . . 9
651ad2antrr 707 . . . . . . . . . . 11 TopOn
66 toponuni 16947 . . . . . . . . . . 11 TopOn
6765, 66syl 16 . . . . . . . . . 10
6817, 67syl5sseq 3356 . . . . . . . . 9
69 eqid 2404 . . . . . . . . . 10
70691stcelcls 17477 . . . . . . . . 9
7164, 68, 70syl2anc 643 . . . . . . . 8
7262, 71mtbird 293 . . . . . . 7
73 topontop 16946 . . . . . . . . 9 TopOn
7465, 73syl 16 . . . . . . . 8
75 1stccnp.4 . . . . . . . . . 10
7675ad2antrr 707 . . . . . . . . 9
7776, 67eleqtrd 2480 . . . . . . . 8
7869elcls 17092 . . . . . . . 8
7974, 68, 77, 78syl3anc 1184 . . . . . . 7
8072, 79mtbid 292 . . . . . 6
8113ad2antrr 707 . . . . . . . . . . . . 13
82 ffun 5552 . . . . . . . . . . . . 13
8381, 82syl 16 . . . . . . . . . . . 12
84 toponss 16949 . . . . . . . . . . . . . 14 TopOn
8565, 84sylan 458 . . . . . . . . . . . . 13
86 fdm 5554 . . . . . . . . . . . . . 14
8781, 86syl 16 . . . . . . . . . . . . 13
8885, 87sseqtr4d 3345 . . . . . . . . . . . 12
89 funimass3 5805 . . . . . . . . . . . 12
9083, 88, 89syl2anc 643 . . . . . . . . . . 11
91 df-ss 3294 . . . . . . . . . . . . 13
9285, 91sylib 189 . . . . . . . . . . . 12
9392sseq1d 3335 . . . . . . . . . . 11
9490, 93bitr4d 248 . . . . . . . . . 10
95 nne 2571 . . . . . . . . . . 11
96 inssdif0 3655 . . . . . . . . . . 11
9795, 96bitr4i 244 . . . . . . . . . 10
9894, 97syl6bbr 255 . . . . . . . . 9
9998anbi2d 685 . . . . . . . 8
10099rexbidva 2683 . . . . . . 7
101 rexanali 2712 . . . . . . 7
102100, 101syl6bb 253 . . . . . 6
10380, 102mpbird 224 . . . . 5
104103expr 599 . . . 4
105104ralrimiva 2749 . . 3
106 iscnp 17255 . . . . 5 TopOn TopOn
1071, 2, 75, 106syl3anc 1184 . . . 4