Metamath Proof Explorer


Theorem 2ndcdisj

Description: Any disjoint family of open sets in a second-countable space is countable. (The sets are required to be nonempty because otherwise there could be many empty sets in the family.) (Contributed by Mario Carneiro, 21-Mar-2015) (Proof shortened by Mario Carneiro, 9-Apr-2015) (Revised by NM, 17-Jun-2017)

Ref Expression
Assertion 2ndcdisj J 2 nd 𝜔 x A B J y * x A y B A ω

Proof

Step Hyp Ref Expression
1 is2ndc J 2 nd 𝜔 b TopBases b ω topGen b = J
2 omex ω V
3 2 brdom b ω f f : b 1-1 ω
4 ssrab2 n ran f | f -1 n 𝒫 B ran f
5 f1f f : b 1-1 ω f : b ω
6 5 frnd f : b 1-1 ω ran f ω
7 6 adantl b TopBases f : b 1-1 ω ran f ω
8 4 7 sstrid b TopBases f : b 1-1 ω n ran f | f -1 n 𝒫 B ω
9 8 adantr b TopBases f : b 1-1 ω x A B topGen b n ran f | f -1 n 𝒫 B ω
10 eldifsn B topGen b B topGen b B
11 n0 B y y B
12 tg2 B topGen b y B z b y z z B
13 omsson ω On
14 8 13 sstrdi b TopBases f : b 1-1 ω n ran f | f -1 n 𝒫 B On
15 14 ad2antrr b TopBases f : b 1-1 ω x A z b y z z B n ran f | f -1 n 𝒫 B On
16 f1fn f : b 1-1 ω f Fn b
17 16 ad3antlr b TopBases f : b 1-1 ω x A z b y z z B f Fn b
18 simprl b TopBases f : b 1-1 ω x A z b y z z B z b
19 fnfvelrn f Fn b z b f z ran f
20 17 18 19 syl2anc b TopBases f : b 1-1 ω x A z b y z z B f z ran f
21 f1f1orn f : b 1-1 ω f : b 1-1 onto ran f
22 21 ad3antlr b TopBases f : b 1-1 ω x A z b y z z B f : b 1-1 onto ran f
23 f1ocnvfv1 f : b 1-1 onto ran f z b f -1 f z = z
24 22 18 23 syl2anc b TopBases f : b 1-1 ω x A z b y z z B f -1 f z = z
25 simprrr b TopBases f : b 1-1 ω x A z b y z z B z B
26 velpw z 𝒫 B z B
27 25 26 sylibr b TopBases f : b 1-1 ω x A z b y z z B z 𝒫 B
28 simprrl b TopBases f : b 1-1 ω x A z b y z z B y z
29 28 ne0d b TopBases f : b 1-1 ω x A z b y z z B z
30 eldifsn z 𝒫 B z 𝒫 B z
31 27 29 30 sylanbrc b TopBases f : b 1-1 ω x A z b y z z B z 𝒫 B
32 24 31 eqeltrd b TopBases f : b 1-1 ω x A z b y z z B f -1 f z 𝒫 B
33 fveq2 n = f z f -1 n = f -1 f z
34 33 eleq1d n = f z f -1 n 𝒫 B f -1 f z 𝒫 B
35 34 rspcev f z ran f f -1 f z 𝒫 B n ran f f -1 n 𝒫 B
36 20 32 35 syl2anc b TopBases f : b 1-1 ω x A z b y z z B n ran f f -1 n 𝒫 B
37 rabn0 n ran f | f -1 n 𝒫 B n ran f f -1 n 𝒫 B
38 36 37 sylibr b TopBases f : b 1-1 ω x A z b y z z B n ran f | f -1 n 𝒫 B
39 onint n ran f | f -1 n 𝒫 B On n ran f | f -1 n 𝒫 B n ran f | f -1 n 𝒫 B n ran f | f -1 n 𝒫 B
40 15 38 39 syl2anc b TopBases f : b 1-1 ω x A z b y z z B n ran f | f -1 n 𝒫 B n ran f | f -1 n 𝒫 B
41 40 rexlimdvaa b TopBases f : b 1-1 ω x A z b y z z B n ran f | f -1 n 𝒫 B n ran f | f -1 n 𝒫 B
42 12 41 syl5 b TopBases f : b 1-1 ω x A B topGen b y B n ran f | f -1 n 𝒫 B n ran f | f -1 n 𝒫 B
43 42 expdimp b TopBases f : b 1-1 ω x A B topGen b y B n ran f | f -1 n 𝒫 B n ran f | f -1 n 𝒫 B
44 43 exlimdv b TopBases f : b 1-1 ω x A B topGen b y y B n ran f | f -1 n 𝒫 B n ran f | f -1 n 𝒫 B
45 11 44 syl5bi b TopBases f : b 1-1 ω x A B topGen b B n ran f | f -1 n 𝒫 B n ran f | f -1 n 𝒫 B
46 45 expimpd b TopBases f : b 1-1 ω x A B topGen b B n ran f | f -1 n 𝒫 B n ran f | f -1 n 𝒫 B
47 10 46 syl5bi b TopBases f : b 1-1 ω x A B topGen b n ran f | f -1 n 𝒫 B n ran f | f -1 n 𝒫 B
48 47 impr b TopBases f : b 1-1 ω x A B topGen b n ran f | f -1 n 𝒫 B n ran f | f -1 n 𝒫 B
49 9 48 sseldd b TopBases f : b 1-1 ω x A B topGen b n ran f | f -1 n 𝒫 B ω
50 49 expr b TopBases f : b 1-1 ω x A B topGen b n ran f | f -1 n 𝒫 B ω
51 50 ralimdva b TopBases f : b 1-1 ω x A B topGen b x A n ran f | f -1 n 𝒫 B ω
52 51 imp b TopBases f : b 1-1 ω x A B topGen b x A n ran f | f -1 n 𝒫 B ω
53 52 adantrr b TopBases f : b 1-1 ω x A B topGen b y * x A y B x A n ran f | f -1 n 𝒫 B ω
54 eqid x A n ran f | f -1 n 𝒫 B = x A n ran f | f -1 n 𝒫 B
55 54 fmpt x A n ran f | f -1 n 𝒫 B ω x A n ran f | f -1 n 𝒫 B : A ω
56 53 55 sylib b TopBases f : b 1-1 ω x A B topGen b y * x A y B x A n ran f | f -1 n 𝒫 B : A ω
57 neeq1 f -1 z = if f -1 z f -1 z 1 𝑜 f -1 z if f -1 z f -1 z 1 𝑜
58 neeq1 1 𝑜 = if f -1 z f -1 z 1 𝑜 1 𝑜 if f -1 z f -1 z 1 𝑜
59 1n0 1 𝑜
60 57 58 59 elimhyp if f -1 z f -1 z 1 𝑜
61 n0 if f -1 z f -1 z 1 𝑜 y y if f -1 z f -1 z 1 𝑜
62 60 61 mpbi y y if f -1 z f -1 z 1 𝑜
63 19.29r y y if f -1 z f -1 z 1 𝑜 y * x A y B y y if f -1 z f -1 z 1 𝑜 * x A y B
64 62 63 mpan y * x A y B y y if f -1 z f -1 z 1 𝑜 * x A y B
65 eleq1 z = n ran f | f -1 n 𝒫 B z n ran f | f -1 n 𝒫 B n ran f | f -1 n 𝒫 B n ran f | f -1 n 𝒫 B
66 48 65 syl5ibrcom b TopBases f : b 1-1 ω x A B topGen b z = n ran f | f -1 n 𝒫 B z n ran f | f -1 n 𝒫 B
67 66 imp b TopBases f : b 1-1 ω x A B topGen b z = n ran f | f -1 n 𝒫 B z n ran f | f -1 n 𝒫 B
68 fveq2 n = z f -1 n = f -1 z
69 68 eleq1d n = z f -1 n 𝒫 B f -1 z 𝒫 B
70 69 elrab z n ran f | f -1 n 𝒫 B z ran f f -1 z 𝒫 B
71 70 simprbi z n ran f | f -1 n 𝒫 B f -1 z 𝒫 B
72 67 71 syl b TopBases f : b 1-1 ω x A B topGen b z = n ran f | f -1 n 𝒫 B f -1 z 𝒫 B
73 eldifsn f -1 z 𝒫 B f -1 z 𝒫 B f -1 z
74 72 73 sylib b TopBases f : b 1-1 ω x A B topGen b z = n ran f | f -1 n 𝒫 B f -1 z 𝒫 B f -1 z
75 74 simprd b TopBases f : b 1-1 ω x A B topGen b z = n ran f | f -1 n 𝒫 B f -1 z
76 75 iftrued b TopBases f : b 1-1 ω x A B topGen b z = n ran f | f -1 n 𝒫 B if f -1 z f -1 z 1 𝑜 = f -1 z
77 74 simpld b TopBases f : b 1-1 ω x A B topGen b z = n ran f | f -1 n 𝒫 B f -1 z 𝒫 B
78 77 elpwid b TopBases f : b 1-1 ω x A B topGen b z = n ran f | f -1 n 𝒫 B f -1 z B
79 76 78 eqsstrd b TopBases f : b 1-1 ω x A B topGen b z = n ran f | f -1 n 𝒫 B if f -1 z f -1 z 1 𝑜 B
80 79 sseld b TopBases f : b 1-1 ω x A B topGen b z = n ran f | f -1 n 𝒫 B y if f -1 z f -1 z 1 𝑜 y B
81 80 exp31 b TopBases f : b 1-1 ω x A B topGen b z = n ran f | f -1 n 𝒫 B y if f -1 z f -1 z 1 𝑜 y B
82 81 com23 b TopBases f : b 1-1 ω z = n ran f | f -1 n 𝒫 B x A B topGen b y if f -1 z f -1 z 1 𝑜 y B
83 82 exp4a b TopBases f : b 1-1 ω z = n ran f | f -1 n 𝒫 B x A B topGen b y if f -1 z f -1 z 1 𝑜 y B
84 83 com25 b TopBases f : b 1-1 ω y if f -1 z f -1 z 1 𝑜 x A B topGen b z = n ran f | f -1 n 𝒫 B y B
85 84 imp31 b TopBases f : b 1-1 ω y if f -1 z f -1 z 1 𝑜 x A B topGen b z = n ran f | f -1 n 𝒫 B y B
86 85 ralimdva b TopBases f : b 1-1 ω y if f -1 z f -1 z 1 𝑜 x A B topGen b x A z = n ran f | f -1 n 𝒫 B y B
87 86 imp b TopBases f : b 1-1 ω y if f -1 z f -1 z 1 𝑜 x A B topGen b x A z = n ran f | f -1 n 𝒫 B y B
88 87 an32s b TopBases f : b 1-1 ω x A B topGen b y if f -1 z f -1 z 1 𝑜 x A z = n ran f | f -1 n 𝒫 B y B
89 rmoim x A z = n ran f | f -1 n 𝒫 B y B * x A y B * x A z = n ran f | f -1 n 𝒫 B
90 88 89 syl b TopBases f : b 1-1 ω x A B topGen b y if f -1 z f -1 z 1 𝑜 * x A y B * x A z = n ran f | f -1 n 𝒫 B
91 90 expimpd b TopBases f : b 1-1 ω x A B topGen b y if f -1 z f -1 z 1 𝑜 * x A y B * x A z = n ran f | f -1 n 𝒫 B
92 91 exlimdv b TopBases f : b 1-1 ω x A B topGen b y y if f -1 z f -1 z 1 𝑜 * x A y B * x A z = n ran f | f -1 n 𝒫 B
93 64 92 syl5 b TopBases f : b 1-1 ω x A B topGen b y * x A y B * x A z = n ran f | f -1 n 𝒫 B
94 93 impr b TopBases f : b 1-1 ω x A B topGen b y * x A y B * x A z = n ran f | f -1 n 𝒫 B
95 nfcv _ x w
96 nfmpt1 _ x x A n ran f | f -1 n 𝒫 B
97 nfcv _ x z
98 95 96 97 nfbr x w x A n ran f | f -1 n 𝒫 B z
99 nfv w x A z = n ran f | f -1 n 𝒫 B
100 breq1 w = x w x A n ran f | f -1 n 𝒫 B z x x A n ran f | f -1 n 𝒫 B z
101 df-br x x A n ran f | f -1 n 𝒫 B z x z x A n ran f | f -1 n 𝒫 B
102 df-mpt x A n ran f | f -1 n 𝒫 B = x z | x A z = n ran f | f -1 n 𝒫 B
103 102 eleq2i x z x A n ran f | f -1 n 𝒫 B x z x z | x A z = n ran f | f -1 n 𝒫 B
104 opabidw x z x z | x A z = n ran f | f -1 n 𝒫 B x A z = n ran f | f -1 n 𝒫 B
105 101 103 104 3bitri x x A n ran f | f -1 n 𝒫 B z x A z = n ran f | f -1 n 𝒫 B
106 100 105 bitrdi w = x w x A n ran f | f -1 n 𝒫 B z x A z = n ran f | f -1 n 𝒫 B
107 98 99 106 cbvmow * w w x A n ran f | f -1 n 𝒫 B z * x x A z = n ran f | f -1 n 𝒫 B
108 df-rmo * x A z = n ran f | f -1 n 𝒫 B * x x A z = n ran f | f -1 n 𝒫 B
109 107 108 bitr4i * w w x A n ran f | f -1 n 𝒫 B z * x A z = n ran f | f -1 n 𝒫 B
110 94 109 sylibr b TopBases f : b 1-1 ω x A B topGen b y * x A y B * w w x A n ran f | f -1 n 𝒫 B z
111 110 alrimiv b TopBases f : b 1-1 ω x A B topGen b y * x A y B z * w w x A n ran f | f -1 n 𝒫 B z
112 dff12 x A n ran f | f -1 n 𝒫 B : A 1-1 ω x A n ran f | f -1 n 𝒫 B : A ω z * w w x A n ran f | f -1 n 𝒫 B z
113 56 111 112 sylanbrc b TopBases f : b 1-1 ω x A B topGen b y * x A y B x A n ran f | f -1 n 𝒫 B : A 1-1 ω
114 f1domg ω V x A n ran f | f -1 n 𝒫 B : A 1-1 ω A ω
115 2 113 114 mpsyl b TopBases f : b 1-1 ω x A B topGen b y * x A y B A ω
116 115 ex b TopBases f : b 1-1 ω x A B topGen b y * x A y B A ω
117 difeq1 topGen b = J topGen b = J
118 117 eleq2d topGen b = J B topGen b B J
119 118 ralbidv topGen b = J x A B topGen b x A B J
120 119 anbi1d topGen b = J x A B topGen b y * x A y B x A B J y * x A y B
121 120 imbi1d topGen b = J x A B topGen b y * x A y B A ω x A B J y * x A y B A ω
122 116 121 syl5ibcom b TopBases f : b 1-1 ω topGen b = J x A B J y * x A y B A ω
123 122 ex b TopBases f : b 1-1 ω topGen b = J x A B J y * x A y B A ω
124 123 exlimdv b TopBases f f : b 1-1 ω topGen b = J x A B J y * x A y B A ω
125 3 124 syl5bi b TopBases b ω topGen b = J x A B J y * x A y B A ω
126 125 impd b TopBases b ω topGen b = J x A B J y * x A y B A ω
127 126 rexlimiv b TopBases b ω topGen b = J x A B J y * x A y B A ω
128 1 127 sylbi J 2 nd 𝜔 x A B J y * x A y B A ω
129 128 3impib J 2 nd 𝜔 x A B J y * x A y B A ω