Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > distop | Structured version Visualization version GIF version |
Description: The discrete topology on a set 𝐴. Part of Example 2 in [Munkres] p. 77. (Contributed by FL, 17-Jul-2006.) (Revised by Mario Carneiro, 19-Mar-2015.) |
Ref | Expression |
---|---|
distop | ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Top) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uniss 4852 | . . . . . 6 ⊢ (𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥 ⊆ ∪ 𝒫 𝐴) | |
2 | unipw 5334 | . . . . . 6 ⊢ ∪ 𝒫 𝐴 = 𝐴 | |
3 | 1, 2 | sseqtrdi 4016 | . . . . 5 ⊢ (𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥 ⊆ 𝐴) |
4 | vuniex 7459 | . . . . . 6 ⊢ ∪ 𝑥 ∈ V | |
5 | 4 | elpw 4545 | . . . . 5 ⊢ (∪ 𝑥 ∈ 𝒫 𝐴 ↔ ∪ 𝑥 ⊆ 𝐴) |
6 | 3, 5 | sylibr 236 | . . . 4 ⊢ (𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥 ∈ 𝒫 𝐴) |
7 | 6 | ax-gen 1792 | . . 3 ⊢ ∀𝑥(𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥 ∈ 𝒫 𝐴) |
8 | 7 | a1i 11 | . 2 ⊢ (𝐴 ∈ 𝑉 → ∀𝑥(𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥 ∈ 𝒫 𝐴)) |
9 | velpw 4546 | . . . . . 6 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴) | |
10 | velpw 4546 | . . . . . . . 8 ⊢ (𝑦 ∈ 𝒫 𝐴 ↔ 𝑦 ⊆ 𝐴) | |
11 | ssinss1 4213 | . . . . . . . . . 10 ⊢ (𝑥 ⊆ 𝐴 → (𝑥 ∩ 𝑦) ⊆ 𝐴) | |
12 | 11 | a1i 11 | . . . . . . . . 9 ⊢ (𝑦 ⊆ 𝐴 → (𝑥 ⊆ 𝐴 → (𝑥 ∩ 𝑦) ⊆ 𝐴)) |
13 | vex 3497 | . . . . . . . . . . 11 ⊢ 𝑦 ∈ V | |
14 | 13 | inex2 5214 | . . . . . . . . . 10 ⊢ (𝑥 ∩ 𝑦) ∈ V |
15 | 14 | elpw 4545 | . . . . . . . . 9 ⊢ ((𝑥 ∩ 𝑦) ∈ 𝒫 𝐴 ↔ (𝑥 ∩ 𝑦) ⊆ 𝐴) |
16 | 12, 15 | syl6ibr 254 | . . . . . . . 8 ⊢ (𝑦 ⊆ 𝐴 → (𝑥 ⊆ 𝐴 → (𝑥 ∩ 𝑦) ∈ 𝒫 𝐴)) |
17 | 10, 16 | sylbi 219 | . . . . . . 7 ⊢ (𝑦 ∈ 𝒫 𝐴 → (𝑥 ⊆ 𝐴 → (𝑥 ∩ 𝑦) ∈ 𝒫 𝐴)) |
18 | 17 | com12 32 | . . . . . 6 ⊢ (𝑥 ⊆ 𝐴 → (𝑦 ∈ 𝒫 𝐴 → (𝑥 ∩ 𝑦) ∈ 𝒫 𝐴)) |
19 | 9, 18 | sylbi 219 | . . . . 5 ⊢ (𝑥 ∈ 𝒫 𝐴 → (𝑦 ∈ 𝒫 𝐴 → (𝑥 ∩ 𝑦) ∈ 𝒫 𝐴)) |
20 | 19 | ralrimiv 3181 | . . . 4 ⊢ (𝑥 ∈ 𝒫 𝐴 → ∀𝑦 ∈ 𝒫 𝐴(𝑥 ∩ 𝑦) ∈ 𝒫 𝐴) |
21 | 20 | rgen 3148 | . . 3 ⊢ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝐴(𝑥 ∩ 𝑦) ∈ 𝒫 𝐴 |
22 | 21 | a1i 11 | . 2 ⊢ (𝐴 ∈ 𝑉 → ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝐴(𝑥 ∩ 𝑦) ∈ 𝒫 𝐴) |
23 | pwexg 5271 | . . 3 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V) | |
24 | istopg 21497 | . . 3 ⊢ (𝒫 𝐴 ∈ V → (𝒫 𝐴 ∈ Top ↔ (∀𝑥(𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥 ∈ 𝒫 𝐴) ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝐴(𝑥 ∩ 𝑦) ∈ 𝒫 𝐴))) | |
25 | 23, 24 | syl 17 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝒫 𝐴 ∈ Top ↔ (∀𝑥(𝑥 ⊆ 𝒫 𝐴 → ∪ 𝑥 ∈ 𝒫 𝐴) ∧ ∀𝑥 ∈ 𝒫 𝐴∀𝑦 ∈ 𝒫 𝐴(𝑥 ∩ 𝑦) ∈ 𝒫 𝐴))) |
26 | 8, 22, 25 | mpbir2and 711 | 1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Top) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∀wal 1531 ∈ wcel 2110 ∀wral 3138 Vcvv 3494 ∩ cin 3934 ⊆ wss 3935 𝒫 cpw 4538 ∪ cuni 4831 Topctop 21495 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-sep 5195 ax-nul 5202 ax-pow 5258 ax-pr 5321 ax-un 7455 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ral 3143 df-rab 3147 df-v 3496 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-pw 4540 df-sn 4561 df-pr 4563 df-uni 4832 df-top 21496 |
This theorem is referenced by: topnex 21598 distopon 21599 distps 21617 discld 21691 restdis 21780 dishaus 21984 discmp 22000 dis2ndc 22062 dislly 22099 dis1stc 22101 dissnlocfin 22131 locfindis 22132 txdis 22234 xkopt 22257 xkofvcn 22286 efmndtmd 22703 symgtgp 22708 dispcmp 31118 |
Copyright terms: Public domain | W3C validator |