Metamath Proof Explorer


Theorem 1stccnp

Description: A mapping is continuous at P in a first-countable space X iff it is sequentially continuous at P , meaning that the image under F of every sequence converging at P converges to F ( P ) . This proof uses ax-cc , but only via 1stcelcls , 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)

Ref Expression
Hypotheses 1stccnp.1 φJ1st𝜔
1stccnp.2 φJTopOnX
1stccnp.3 φKTopOnY
1stccnp.4 φPX
Assertion 1stccnp φFJCnPKPF:XYff:XftJPFftKFP

Proof

Step Hyp Ref Expression
1 1stccnp.1 φJ1st𝜔
2 1stccnp.2 φJTopOnX
3 1stccnp.3 φKTopOnY
4 1stccnp.4 φPX
5 2 3 jca φJTopOnXKTopOnY
6 cnpf2 JTopOnXKTopOnYFJCnPKPF:XY
7 6 3expa JTopOnXKTopOnYFJCnPKPF:XY
8 5 7 sylan φFJCnPKPF:XY
9 simprr φFJCnPKPf:XftJPftJP
10 simplr φFJCnPKPf:XftJPFJCnPKP
11 9 10 lmcnp φFJCnPKPf:XftJPFftKFP
12 11 ex φFJCnPKPf:XftJPFftKFP
13 12 alrimiv φFJCnPKPff:XftJPFftKFP
14 8 13 jca φFJCnPKPF:XYff:XftJPFftKFP
15 simprl φF:XYff:XftJPFftKFPF:XY
16 fal ¬
17 19.29 ff:XftJPFftKFPff:XF-1uftJPff:XftJPFftKFPf:XF-1uftJP
18 simprl φF:XYuKFPuf:XF-1uftJPf:XF-1u
19 difss XF-1uX
20 fss f:XF-1uXF-1uXf:X
21 18 19 20 sylancl φF:XYuKFPuf:XF-1uftJPf:X
22 simprr φF:XYuKFPuf:XF-1uftJPftJP
23 21 22 jca φF:XYuKFPuf:XF-1uftJPf:XftJP
24 nnuz =1
25 simplrr φF:XYuKFPuf:XF-1uftJPFftKFPFPu
26 1zzd φF:XYuKFPuf:XF-1uftJPFftKFP1
27 simprr φF:XYuKFPuf:XF-1uftJPFftKFPFftKFP
28 simplrl φF:XYuKFPuf:XF-1uftJPFftKFPuK
29 24 25 26 27 28 lmcvg φF:XYuKFPuf:XF-1uftJPFftKFPjkjFfku
30 24 r19.2uz jkjFfkukFfku
31 simprll φF:XYuKFPuf:XF-1uftJPFftKFPf:XF-1u
32 31 ffnd φF:XYuKFPuf:XF-1uftJPFftKFPfFn
33 fvco2 fFnkFfk=Ffk
34 32 33 sylan φF:XYuKFPuf:XF-1uftJPFftKFPkFfk=Ffk
35 34 eleq1d φF:XYuKFPuf:XF-1uftJPFftKFPkFfkuFfku
36 31 ffvelrnda φF:XYuKFPuf:XF-1uftJPFftKFPkfkXF-1u
37 36 eldifad φF:XYuKFPuf:XF-1uftJPFftKFPkfkX
38 simplr φF:XYuKFPuF:XY
39 38 ad2antrr φF:XYuKFPuf:XF-1uftJPFftKFPkF:XY
40 ffn F:XYFFnX
41 elpreima FFnXfkF-1ufkXFfku
42 39 40 41 3syl φF:XYuKFPuf:XF-1uftJPFftKFPkfkF-1ufkXFfku
43 36 eldifbd φF:XYuKFPuf:XF-1uftJPFftKFPk¬fkF-1u
44 43 pm2.21d φF:XYuKFPuf:XF-1uftJPFftKFPkfkF-1u
45 42 44 sylbird φF:XYuKFPuf:XF-1uftJPFftKFPkfkXFfku
46 37 45 mpand φF:XYuKFPuf:XF-1uftJPFftKFPkFfku
47 35 46 sylbid φF:XYuKFPuf:XF-1uftJPFftKFPkFfku
48 47 rexlimdva φF:XYuKFPuf:XF-1uftJPFftKFPkFfku
49 30 48 syl5 φF:XYuKFPuf:XF-1uftJPFftKFPjkjFfku
50 29 49 mpd φF:XYuKFPuf:XF-1uftJPFftKFP
51 50 expr φF:XYuKFPuf:XF-1uftJPFftKFP
52 23 51 embantd φF:XYuKFPuf:XF-1uftJPf:XftJPFftKFP
53 52 ex φF:XYuKFPuf:XF-1uftJPf:XftJPFftKFP
54 53 impcomd φF:XYuKFPuf:XftJPFftKFPf:XF-1uftJP
55 54 exlimdv φF:XYuKFPuff:XftJPFftKFPf:XF-1uftJP
56 17 55 syl5 φF:XYuKFPuff:XftJPFftKFPff:XF-1uftJP
57 56 exp4b φF:XYuKFPuff:XftJPFftKFPff:XF-1uftJP
58 57 com23 φF:XYff:XftJPFftKFPuKFPuff:XF-1uftJP
59 58 impr φF:XYff:XftJPFftKFPuKFPuff:XF-1uftJP
60 59 imp φF:XYff:XftJPFftKFPuKFPuff:XF-1uftJP
61 16 60 mtoi φF:XYff:XftJPFftKFPuKFPu¬ff:XF-1uftJP
62 1 ad2antrr φF:XYff:XftJPFftKFPuKFPuJ1st𝜔
63 2 ad2antrr φF:XYff:XftJPFftKFPuKFPuJTopOnX
64 toponuni JTopOnXX=J
65 63 64 syl φF:XYff:XftJPFftKFPuKFPuX=J
66 19 65 sseqtrid φF:XYff:XftJPFftKFPuKFPuXF-1uJ
67 eqid J=J
68 67 1stcelcls J1st𝜔XF-1uJPclsJXF-1uff:XF-1uftJP
69 62 66 68 syl2anc φF:XYff:XftJPFftKFPuKFPuPclsJXF-1uff:XF-1uftJP
70 61 69 mtbird φF:XYff:XftJPFftKFPuKFPu¬PclsJXF-1u
71 topontop JTopOnXJTop
72 63 71 syl φF:XYff:XftJPFftKFPuKFPuJTop
73 4 ad2antrr φF:XYff:XftJPFftKFPuKFPuPX
74 73 65 eleqtrd φF:XYff:XftJPFftKFPuKFPuPJ
75 67 elcls JTopXF-1uJPJPclsJXF-1uvJPvvXF-1u
76 72 66 74 75 syl3anc φF:XYff:XftJPFftKFPuKFPuPclsJXF-1uvJPvvXF-1u
77 70 76 mtbid φF:XYff:XftJPFftKFPuKFPu¬vJPvvXF-1u
78 15 ad2antrr φF:XYff:XftJPFftKFPuKFPuvJF:XY
79 78 ffund φF:XYff:XftJPFftKFPuKFPuvJFunF
80 toponss JTopOnXvJvX
81 63 80 sylan φF:XYff:XftJPFftKFPuKFPuvJvX
82 78 fdmd φF:XYff:XftJPFftKFPuKFPuvJdomF=X
83 81 82 sseqtrrd φF:XYff:XftJPFftKFPuKFPuvJvdomF
84 funimass3 FunFvdomFFvuvF-1u
85 79 83 84 syl2anc φF:XYff:XftJPFftKFPuKFPuvJFvuvF-1u
86 df-ss vXvX=v
87 81 86 sylib φF:XYff:XftJPFftKFPuKFPuvJvX=v
88 87 sseq1d φF:XYff:XftJPFftKFPuKFPuvJvXF-1uvF-1u
89 85 88 bitr4d φF:XYff:XftJPFftKFPuKFPuvJFvuvXF-1u
90 nne ¬vXF-1uvXF-1u=
91 inssdif0 vXF-1uvXF-1u=
92 90 91 bitr4i ¬vXF-1uvXF-1u
93 89 92 bitr4di φF:XYff:XftJPFftKFPuKFPuvJFvu¬vXF-1u
94 93 anbi2d φF:XYff:XftJPFftKFPuKFPuvJPvFvuPv¬vXF-1u
95 94 rexbidva φF:XYff:XftJPFftKFPuKFPuvJPvFvuvJPv¬vXF-1u
96 rexanali vJPv¬vXF-1u¬vJPvvXF-1u
97 95 96 bitrdi φF:XYff:XftJPFftKFPuKFPuvJPvFvu¬vJPvvXF-1u
98 77 97 mpbird φF:XYff:XftJPFftKFPuKFPuvJPvFvu
99 98 expr φF:XYff:XftJPFftKFPuKFPuvJPvFvu
100 99 ralrimiva φF:XYff:XftJPFftKFPuKFPuvJPvFvu
101 iscnp JTopOnXKTopOnYPXFJCnPKPF:XYuKFPuvJPvFvu
102 2 3 4 101 syl3anc φFJCnPKPF:XYuKFPuvJPvFvu
103 102 adantr φF:XYff:XftJPFftKFPFJCnPKPF:XYuKFPuvJPvFvu
104 15 100 103 mpbir2and φF:XYff:XftJPFftKFPFJCnPKP
105 14 104 impbida φFJCnPKPF:XYff:XftJPFftKFP