Metamath Proof Explorer


Theorem 2ndcomap

Description: A surjective continuous open map maps second-countable spaces to second-countable spaces. (Contributed by Mario Carneiro, 9-Apr-2015)

Ref Expression
Hypotheses 2ndcomap.2 Y=K
2ndcomap.3 φJ2nd𝜔
2ndcomap.5 φFJCnK
2ndcomap.6 φranF=Y
2ndcomap.7 φxJFxK
Assertion 2ndcomap φK2nd𝜔

Proof

Step Hyp Ref Expression
1 2ndcomap.2 Y=K
2 2ndcomap.3 φJ2nd𝜔
3 2ndcomap.5 φFJCnK
4 2ndcomap.6 φranF=Y
5 2ndcomap.7 φxJFxK
6 cntop2 FJCnKKTop
7 3 6 syl φKTop
8 7 ad2antrr φbTopBasesbωtopGenb=JKTop
9 simplll φbTopBasesbωtopGenb=Jxbφ
10 bastg bTopBasesbtopGenb
11 10 ad2antlr φbTopBasesbωtopGenb=JbtopGenb
12 simprr φbTopBasesbωtopGenb=JtopGenb=J
13 11 12 sseqtrd φbTopBasesbωtopGenb=JbJ
14 13 sselda φbTopBasesbωtopGenb=JxbxJ
15 9 14 5 syl2anc φbTopBasesbωtopGenb=JxbFxK
16 15 fmpttd φbTopBasesbωtopGenb=JxbFx:bK
17 16 frnd φbTopBasesbωtopGenb=JranxbFxK
18 elunii zkkKzK
19 18 1 eleqtrrdi zkkKzY
20 19 ancoms kKzkzY
21 20 adantl φbTopBasesbωtopGenb=JkKzkzY
22 4 ad3antrrr φbTopBasesbωtopGenb=JkKzkranF=Y
23 21 22 eleqtrrd φbTopBasesbωtopGenb=JkKzkzranF
24 eqid J=J
25 24 1 cnf FJCnKF:JY
26 3 25 syl φF:JY
27 26 ad3antrrr φbTopBasesbωtopGenb=JkKzkF:JY
28 ffn F:JYFFnJ
29 fvelrnb FFnJzranFtJFt=z
30 27 28 29 3syl φbTopBasesbωtopGenb=JkKzkzranFtJFt=z
31 23 30 mpbid φbTopBasesbωtopGenb=JkKzktJFt=z
32 3 ad3antrrr φbTopBasesbωtopGenb=JkKzktJFt=zFJCnK
33 simprll φbTopBasesbωtopGenb=JkKzktJFt=zkK
34 cnima FJCnKkKF-1kJ
35 32 33 34 syl2anc φbTopBasesbωtopGenb=JkKzktJFt=zF-1kJ
36 12 adantr φbTopBasesbωtopGenb=JkKzktJFt=ztopGenb=J
37 35 36 eleqtrrd φbTopBasesbωtopGenb=JkKzktJFt=zF-1ktopGenb
38 simprrl φbTopBasesbωtopGenb=JkKzktJFt=ztJ
39 simprrr φbTopBasesbωtopGenb=JkKzktJFt=zFt=z
40 simprlr φbTopBasesbωtopGenb=JkKzktJFt=zzk
41 39 40 eqeltrd φbTopBasesbωtopGenb=JkKzktJFt=zFtk
42 27 ffnd φbTopBasesbωtopGenb=JkKzkFFnJ
43 42 adantrr φbTopBasesbωtopGenb=JkKzktJFt=zFFnJ
44 elpreima FFnJtF-1ktJFtk
45 43 44 syl φbTopBasesbωtopGenb=JkKzktJFt=ztF-1ktJFtk
46 38 41 45 mpbir2and φbTopBasesbωtopGenb=JkKzktJFt=ztF-1k
47 tg2 F-1ktopGenbtF-1kmbtmmF-1k
48 37 46 47 syl2anc φbTopBasesbωtopGenb=JkKzktJFt=zmbtmmF-1k
49 simprl φbTopBasesbωtopGenb=JkKzktJFt=zmbtmmF-1kmb
50 eqid Fm=Fm
51 imaeq2 x=mFx=Fm
52 51 rspceeqv mbFm=FmxbFm=Fx
53 49 50 52 sylancl φbTopBasesbωtopGenb=JkKzktJFt=zmbtmmF-1kxbFm=Fx
54 43 adantr φbTopBasesbωtopGenb=JkKzktJFt=zmbtmmF-1kFFnJ
55 fnfun FFnJFunF
56 54 55 syl φbTopBasesbωtopGenb=JkKzktJFt=zmbtmmF-1kFunF
57 simprrr φbTopBasesbωtopGenb=JkKzktJFt=zmbtmmF-1kmF-1k
58 funimass2 FunFmF-1kFmk
59 56 57 58 syl2anc φbTopBasesbωtopGenb=JkKzktJFt=zmbtmmF-1kFmk
60 vex kV
61 ssexg FmkkVFmV
62 59 60 61 sylancl φbTopBasesbωtopGenb=JkKzktJFt=zmbtmmF-1kFmV
63 eqid xbFx=xbFx
64 63 elrnmpt FmVFmranxbFxxbFm=Fx
65 62 64 syl φbTopBasesbωtopGenb=JkKzktJFt=zmbtmmF-1kFmranxbFxxbFm=Fx
66 53 65 mpbird φbTopBasesbωtopGenb=JkKzktJFt=zmbtmmF-1kFmranxbFx
67 39 adantr φbTopBasesbωtopGenb=JkKzktJFt=zmbtmmF-1kFt=z
68 simprrl φbTopBasesbωtopGenb=JkKzktJFt=zmbtmmF-1ktm
69 cnvimass F-1kdomF
70 57 69 sstrdi φbTopBasesbωtopGenb=JkKzktJFt=zmbtmmF-1kmdomF
71 funfvima2 FunFmdomFtmFtFm
72 56 70 71 syl2anc φbTopBasesbωtopGenb=JkKzktJFt=zmbtmmF-1ktmFtFm
73 68 72 mpd φbTopBasesbωtopGenb=JkKzktJFt=zmbtmmF-1kFtFm
74 67 73 eqeltrrd φbTopBasesbωtopGenb=JkKzktJFt=zmbtmmF-1kzFm
75 eleq2 w=FmzwzFm
76 sseq1 w=FmwkFmk
77 75 76 anbi12d w=FmzwwkzFmFmk
78 77 rspcev FmranxbFxzFmFmkwranxbFxzwwk
79 66 74 59 78 syl12anc φbTopBasesbωtopGenb=JkKzktJFt=zmbtmmF-1kwranxbFxzwwk
80 48 79 rexlimddv φbTopBasesbωtopGenb=JkKzktJFt=zwranxbFxzwwk
81 80 anassrs φbTopBasesbωtopGenb=JkKzktJFt=zwranxbFxzwwk
82 31 81 rexlimddv φbTopBasesbωtopGenb=JkKzkwranxbFxzwwk
83 82 ralrimivva φbTopBasesbωtopGenb=JkKzkwranxbFxzwwk
84 basgen2 KTopranxbFxKkKzkwranxbFxzwwktopGenranxbFx=K
85 8 17 83 84 syl3anc φbTopBasesbωtopGenb=JtopGenranxbFx=K
86 85 8 eqeltrd φbTopBasesbωtopGenb=JtopGenranxbFxTop
87 tgclb ranxbFxTopBasestopGenranxbFxTop
88 86 87 sylibr φbTopBasesbωtopGenb=JranxbFxTopBases
89 omelon ωOn
90 simprl φbTopBasesbωtopGenb=Jbω
91 ondomen ωOnbωbdomcard
92 89 90 91 sylancr φbTopBasesbωtopGenb=Jbdomcard
93 16 ffnd φbTopBasesbωtopGenb=JxbFxFnb
94 dffn4 xbFxFnbxbFx:bontoranxbFx
95 93 94 sylib φbTopBasesbωtopGenb=JxbFx:bontoranxbFx
96 fodomnum bdomcardxbFx:bontoranxbFxranxbFxb
97 92 95 96 sylc φbTopBasesbωtopGenb=JranxbFxb
98 domtr ranxbFxbbωranxbFxω
99 97 90 98 syl2anc φbTopBasesbωtopGenb=JranxbFxω
100 2ndci ranxbFxTopBasesranxbFxωtopGenranxbFx2nd𝜔
101 88 99 100 syl2anc φbTopBasesbωtopGenb=JtopGenranxbFx2nd𝜔
102 85 101 eqeltrrd φbTopBasesbωtopGenb=JK2nd𝜔
103 is2ndc J2nd𝜔bTopBasesbωtopGenb=J
104 2 103 sylib φbTopBasesbωtopGenb=J
105 102 104 r19.29a φK2nd𝜔