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 φ J 2 nd 𝜔
2ndcomap.5 φ F J Cn K
2ndcomap.6 φ ran F = Y
2ndcomap.7 φ x J F x K
Assertion 2ndcomap φ K 2 nd 𝜔

Proof

Step Hyp Ref Expression
1 2ndcomap.2 Y = K
2 2ndcomap.3 φ J 2 nd 𝜔
3 2ndcomap.5 φ F J Cn K
4 2ndcomap.6 φ ran F = Y
5 2ndcomap.7 φ x J F x K
6 cntop2 F J Cn K K Top
7 3 6 syl φ K Top
8 7 ad2antrr φ b TopBases b ω topGen b = J K Top
9 simplll φ b TopBases b ω topGen b = J x b φ
10 bastg b TopBases b topGen b
11 10 ad2antlr φ b TopBases b ω topGen b = J b topGen b
12 simprr φ b TopBases b ω topGen b = J topGen b = J
13 11 12 sseqtrd φ b TopBases b ω topGen b = J b J
14 13 sselda φ b TopBases b ω topGen b = J x b x J
15 9 14 5 syl2anc φ b TopBases b ω topGen b = J x b F x K
16 15 fmpttd φ b TopBases b ω topGen b = J x b F x : b K
17 16 frnd φ b TopBases b ω topGen b = J ran x b F x K
18 elunii z k k K z K
19 18 1 eleqtrrdi z k k K z Y
20 19 ancoms k K z k z Y
21 20 adantl φ b TopBases b ω topGen b = J k K z k z Y
22 4 ad3antrrr φ b TopBases b ω topGen b = J k K z k ran F = Y
23 21 22 eleqtrrd φ b TopBases b ω topGen b = J k K z k z ran F
24 eqid J = J
25 24 1 cnf F J Cn K F : J Y
26 3 25 syl φ F : J Y
27 26 ad3antrrr φ b TopBases b ω topGen b = J k K z k F : J Y
28 ffn F : J Y F Fn J
29 fvelrnb F Fn J z ran F t J F t = z
30 27 28 29 3syl φ b TopBases b ω topGen b = J k K z k z ran F t J F t = z
31 23 30 mpbid φ b TopBases b ω topGen b = J k K z k t J F t = z
32 3 ad3antrrr φ b TopBases b ω topGen b = J k K z k t J F t = z F J Cn K
33 simprll φ b TopBases b ω topGen b = J k K z k t J F t = z k K
34 cnima F J Cn K k K F -1 k J
35 32 33 34 syl2anc φ b TopBases b ω topGen b = J k K z k t J F t = z F -1 k J
36 12 adantr φ b TopBases b ω topGen b = J k K z k t J F t = z topGen b = J
37 35 36 eleqtrrd φ b TopBases b ω topGen b = J k K z k t J F t = z F -1 k topGen b
38 simprrl φ b TopBases b ω topGen b = J k K z k t J F t = z t J
39 simprrr φ b TopBases b ω topGen b = J k K z k t J F t = z F t = z
40 simprlr φ b TopBases b ω topGen b = J k K z k t J F t = z z k
41 39 40 eqeltrd φ b TopBases b ω topGen b = J k K z k t J F t = z F t k
42 27 ffnd φ b TopBases b ω topGen b = J k K z k F Fn J
43 42 adantrr φ b TopBases b ω topGen b = J k K z k t J F t = z F Fn J
44 elpreima F Fn J t F -1 k t J F t k
45 43 44 syl φ b TopBases b ω topGen b = J k K z k t J F t = z t F -1 k t J F t k
46 38 41 45 mpbir2and φ b TopBases b ω topGen b = J k K z k t J F t = z t F -1 k
47 tg2 F -1 k topGen b t F -1 k m b t m m F -1 k
48 37 46 47 syl2anc φ b TopBases b ω topGen b = J k K z k t J F t = z m b t m m F -1 k
49 simprl φ b TopBases b ω topGen b = J k K z k t J F t = z m b t m m F -1 k m b
50 eqid F m = F m
51 imaeq2 x = m F x = F m
52 51 rspceeqv m b F m = F m x b F m = F x
53 49 50 52 sylancl φ b TopBases b ω topGen b = J k K z k t J F t = z m b t m m F -1 k x b F m = F x
54 43 adantr φ b TopBases b ω topGen b = J k K z k t J F t = z m b t m m F -1 k F Fn J
55 fnfun F Fn J Fun F
56 54 55 syl φ b TopBases b ω topGen b = J k K z k t J F t = z m b t m m F -1 k Fun F
57 simprrr φ b TopBases b ω topGen b = J k K z k t J F t = z m b t m m F -1 k m F -1 k
58 funimass2 Fun F m F -1 k F m k
59 56 57 58 syl2anc φ b TopBases b ω topGen b = J k K z k t J F t = z m b t m m F -1 k F m k
60 vex k V
61 ssexg F m k k V F m V
62 59 60 61 sylancl φ b TopBases b ω topGen b = J k K z k t J F t = z m b t m m F -1 k F m V
63 eqid x b F x = x b F x
64 63 elrnmpt F m V F m ran x b F x x b F m = F x
65 62 64 syl φ b TopBases b ω topGen b = J k K z k t J F t = z m b t m m F -1 k F m ran x b F x x b F m = F x
66 53 65 mpbird φ b TopBases b ω topGen b = J k K z k t J F t = z m b t m m F -1 k F m ran x b F x
67 39 adantr φ b TopBases b ω topGen b = J k K z k t J F t = z m b t m m F -1 k F t = z
68 simprrl φ b TopBases b ω topGen b = J k K z k t J F t = z m b t m m F -1 k t m
69 cnvimass F -1 k dom F
70 57 69 sstrdi φ b TopBases b ω topGen b = J k K z k t J F t = z m b t m m F -1 k m dom F
71 funfvima2 Fun F m dom F t m F t F m
72 56 70 71 syl2anc φ b TopBases b ω topGen b = J k K z k t J F t = z m b t m m F -1 k t m F t F m
73 68 72 mpd φ b TopBases b ω topGen b = J k K z k t J F t = z m b t m m F -1 k F t F m
74 67 73 eqeltrrd φ b TopBases b ω topGen b = J k K z k t J F t = z m b t m m F -1 k z F m
75 eleq2 w = F m z w z F m
76 sseq1 w = F m w k F m k
77 75 76 anbi12d w = F m z w w k z F m F m k
78 77 rspcev F m ran x b F x z F m F m k w ran x b F x z w w k
79 66 74 59 78 syl12anc φ b TopBases b ω topGen b = J k K z k t J F t = z m b t m m F -1 k w ran x b F x z w w k
80 48 79 rexlimddv φ b TopBases b ω topGen b = J k K z k t J F t = z w ran x b F x z w w k
81 80 anassrs φ b TopBases b ω topGen b = J k K z k t J F t = z w ran x b F x z w w k
82 31 81 rexlimddv φ b TopBases b ω topGen b = J k K z k w ran x b F x z w w k
83 82 ralrimivva φ b TopBases b ω topGen b = J k K z k w ran x b F x z w w k
84 basgen2 K Top ran x b F x K k K z k w ran x b F x z w w k topGen ran x b F x = K
85 8 17 83 84 syl3anc φ b TopBases b ω topGen b = J topGen ran x b F x = K
86 85 8 eqeltrd φ b TopBases b ω topGen b = J topGen ran x b F x Top
87 tgclb ran x b F x TopBases topGen ran x b F x Top
88 86 87 sylibr φ b TopBases b ω topGen b = J ran x b F x TopBases
89 omelon ω On
90 simprl φ b TopBases b ω topGen b = J b ω
91 ondomen ω On b ω b dom card
92 89 90 91 sylancr φ b TopBases b ω topGen b = J b dom card
93 16 ffnd φ b TopBases b ω topGen b = J x b F x Fn b
94 dffn4 x b F x Fn b x b F x : b onto ran x b F x
95 93 94 sylib φ b TopBases b ω topGen b = J x b F x : b onto ran x b F x
96 fodomnum b dom card x b F x : b onto ran x b F x ran x b F x b
97 92 95 96 sylc φ b TopBases b ω topGen b = J ran x b F x b
98 domtr ran x b F x b b ω ran x b F x ω
99 97 90 98 syl2anc φ b TopBases b ω topGen b = J ran x b F x ω
100 2ndci ran x b F x TopBases ran x b F x ω topGen ran x b F x 2 nd 𝜔
101 88 99 100 syl2anc φ b TopBases b ω topGen b = J topGen ran x b F x 2 nd 𝜔
102 85 101 eqeltrrd φ b TopBases b ω topGen b = J K 2 nd 𝜔
103 is2ndc J 2 nd 𝜔 b TopBases b ω topGen b = J
104 2 103 sylib φ b TopBases b ω topGen b = J
105 102 104 r19.29a φ K 2 nd 𝜔