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

Theorem 1stccnp 17556
 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 8346, but only via 1stcelcls 17555, 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 520 . . . 4 TopOn TopOn
4 cnpf2 17345 . . . . 5 TopOn TopOn
543expa 1154 . . . 4 TopOn TopOn
63, 5sylan 459 . . 3
7 simprr 735 . . . . . 6
8 simplr 733 . . . . . 6
97, 8lmcnp 17399 . . . . 5
109ex 425 . . . 4
1110alrimiv 1642 . . 3
126, 11jca 520 . 2
13 simprl 734 . . 3
14 fal 1332 . . . . . . . . 9
15 19.29 1607 . . . . . . . . . . . . . 14
16 simprl 734 . . . . . . . . . . . . . . . . . . . . 21
17 difss 3460 . . . . . . . . . . . . . . . . . . . . 21
18 fss 5628 . . . . . . . . . . . . . . . . . . . . 21
1916, 17, 18sylancl 645 . . . . . . . . . . . . . . . . . . . 20
20 simprr 735 . . . . . . . . . . . . . . . . . . . 20
2119, 20jca 520 . . . . . . . . . . . . . . . . . . 19
22 nnuz 10552 . . . . . . . . . . . . . . . . . . . . . 22
23 simplrr 739 . . . . . . . . . . . . . . . . . . . . . 22
24 1z 10342 . . . . . . . . . . . . . . . . . . . . . . 23
2524a1i 11 . . . . . . . . . . . . . . . . . . . . . 22
26 simprr 735 . . . . . . . . . . . . . . . . . . . . . 22
27 simplrl 738 . . . . . . . . . . . . . . . . . . . . . 22
2822, 23, 25, 26, 27lmcvg 17357 . . . . . . . . . . . . . . . . . . . . 21
2922r19.2uz 12186 . . . . . . . . . . . . . . . . . . . . . 22
30 simprll 740 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
31 ffn 5620 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
3230, 31syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26
33 fvco2 5827 . . . . . . . . . . . . . . . . . . . . . . . . . 26
3432, 33sylan 459 . . . . . . . . . . . . . . . . . . . . . . . . 25
3534eleq1d 2508 . . . . . . . . . . . . . . . . . . . . . . . 24
3630ffvelrnda 5899 . . . . . . . . . . . . . . . . . . . . . . . . . 26
3736eldifad 3318 . . . . . . . . . . . . . . . . . . . . . . . . 25
38 simplr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
3938ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
40 ffn 5620 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
41 elpreima 5879 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
4239, 40, 413syl 19 . . . . . . . . . . . . . . . . . . . . . . . . . 26
4336eldifbd 3319 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
4443pm2.21d 101 . . . . . . . . . . . . . . . . . . . . . . . . . 26
4542, 44sylbird 228 . . . . . . . . . . . . . . . . . . . . . . . . 25
4637, 45mpand 658 . . . . . . . . . . . . . . . . . . . . . . . 24
4735, 46sylbid 208 . . . . . . . . . . . . . . . . . . . . . . 23
4847rexlimdva 2836 . . . . . . . . . . . . . . . . . . . . . 22
4929, 48syl5 31 . . . . . . . . . . . . . . . . . . . . 21
5028, 49mpd 15 . . . . . . . . . . . . . . . . . . . 20
5150expr 600 . . . . . . . . . . . . . . . . . . 19
5221, 51embantd 53 . . . . . . . . . . . . . . . . . 18
5352ex 425 . . . . . . . . . . . . . . . . 17
5453com23 75 . . . . . . . . . . . . . . . 16
5554imp3a 422 . . . . . . . . . . . . . . 15
5655exlimdv 1647 . . . . . . . . . . . . . 14
5715, 56syl5 31 . . . . . . . . . . . . 13
5857exp4b 592 . . . . . . . . . . . 12
5958com23 75 . . . . . . . . . . 11
6059impr 604 . . . . . . . . . 10
6160imp 420 . . . . . . . . 9
6214, 61mtoi 172 . . . . . . . 8
63 1stccnp.1 . . . . . . . . . 10
6463ad2antrr 708 . . . . . . . . 9
651ad2antrr 708 . . . . . . . . . . 11 TopOn
66 toponuni 17023 . . . . . . . . . . 11 TopOn
6765, 66syl 16 . . . . . . . . . 10
6817, 67syl5sseq 3382 . . . . . . . . 9
69 eqid 2442 . . . . . . . . . 10
70691stcelcls 17555 . . . . . . . . 9
7164, 68, 70syl2anc 644 . . . . . . . 8
7262, 71mtbird 294 . . . . . . 7
73 topontop 17022 . . . . . . . . 9 TopOn
7465, 73syl 16 . . . . . . . 8
75 1stccnp.4 . . . . . . . . . 10
7675ad2antrr 708 . . . . . . . . 9
7776, 67eleqtrd 2518 . . . . . . . 8
7869elcls 17168 . . . . . . . 8
7974, 68, 77, 78syl3anc 1185 . . . . . . 7
8072, 79mtbid 293 . . . . . 6
8113ad2antrr 708 . . . . . . . . . . . . 13
82 ffun 5622 . . . . . . . . . . . . 13
8381, 82syl 16 . . . . . . . . . . . 12
84 toponss 17025 . . . . . . . . . . . . . 14 TopOn
8565, 84sylan 459 . . . . . . . . . . . . 13
86 fdm 5624 . . . . . . . . . . . . . 14
8781, 86syl 16 . . . . . . . . . . . . 13
8885, 87sseqtr4d 3371 . . . . . . . . . . . 12
89 funimass3 5875 . . . . . . . . . . . 12
9083, 88, 89syl2anc 644 . . . . . . . . . . 11
91 df-ss 3320 . . . . . . . . . . . . 13
9285, 91sylib 190 . . . . . . . . . . . 12
9392sseq1d 3361 . . . . . . . . . . 11
9490, 93bitr4d 249 . . . . . . . . . 10
95 nne 2611 . . . . . . . . . . 11
96 inssdif0 3719 . . . . . . . . . . 11
9795, 96bitr4i 245 . . . . . . . . . 10
9894, 97syl6bbr 256 . . . . . . . . 9
9998anbi2d 686 . . . . . . . 8
10099rexbidva 2728 . . . . . . 7
101 rexanali 2757 . . . . . . 7
102100, 101syl6bb 254 . . . . . 6
10380, 102mpbird 225 . . . . 5
104103expr 600 . . . 4
105104ralrimiva 2795 . . 3
106 iscnp 17332 . . . . 5 TopOn TopOn
1071, 2, 75, 106syl3anc 1185 . . . 4