MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  distop Structured version   Visualization version   GIF version

Theorem distop 22343
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.)
Assertion
Ref Expression
distop (𝐴𝑉 → 𝒫 𝐴 ∈ Top)

Proof of Theorem distop
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 uniss 4873 . . . . . 6 (𝑥 ⊆ 𝒫 𝐴 𝑥 𝒫 𝐴)
2 unipw 5407 . . . . . 6 𝒫 𝐴 = 𝐴
31, 2sseqtrdi 3994 . . . . 5 (𝑥 ⊆ 𝒫 𝐴 𝑥𝐴)
4 vuniex 7675 . . . . . 6 𝑥 ∈ V
54elpw 4564 . . . . 5 ( 𝑥 ∈ 𝒫 𝐴 𝑥𝐴)
63, 5sylibr 233 . . . 4 (𝑥 ⊆ 𝒫 𝐴 𝑥 ∈ 𝒫 𝐴)
76ax-gen 1797 . . 3 𝑥(𝑥 ⊆ 𝒫 𝐴 𝑥 ∈ 𝒫 𝐴)
87a1i 11 . 2 (𝐴𝑉 → ∀𝑥(𝑥 ⊆ 𝒫 𝐴 𝑥 ∈ 𝒫 𝐴))
9 velpw 4565 . . . . . 6 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
10 velpw 4565 . . . . . . . 8 (𝑦 ∈ 𝒫 𝐴𝑦𝐴)
11 ssinss1 4197 . . . . . . . . . 10 (𝑥𝐴 → (𝑥𝑦) ⊆ 𝐴)
1211a1i 11 . . . . . . . . 9 (𝑦𝐴 → (𝑥𝐴 → (𝑥𝑦) ⊆ 𝐴))
13 vex 3449 . . . . . . . . . . 11 𝑦 ∈ V
1413inex2 5275 . . . . . . . . . 10 (𝑥𝑦) ∈ V
1514elpw 4564 . . . . . . . . 9 ((𝑥𝑦) ∈ 𝒫 𝐴 ↔ (𝑥𝑦) ⊆ 𝐴)
1612, 15syl6ibr 251 . . . . . . . 8 (𝑦𝐴 → (𝑥𝐴 → (𝑥𝑦) ∈ 𝒫 𝐴))
1710, 16sylbi 216 . . . . . . 7 (𝑦 ∈ 𝒫 𝐴 → (𝑥𝐴 → (𝑥𝑦) ∈ 𝒫 𝐴))
1817com12 32 . . . . . 6 (𝑥𝐴 → (𝑦 ∈ 𝒫 𝐴 → (𝑥𝑦) ∈ 𝒫 𝐴))
199, 18sylbi 216 . . . . 5 (𝑥 ∈ 𝒫 𝐴 → (𝑦 ∈ 𝒫 𝐴 → (𝑥𝑦) ∈ 𝒫 𝐴))
2019ralrimiv 3142 . . . 4 (𝑥 ∈ 𝒫 𝐴 → ∀𝑦 ∈ 𝒫 𝐴(𝑥𝑦) ∈ 𝒫 𝐴)
2120rgen 3066 . . 3 𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝐴(𝑥𝑦) ∈ 𝒫 𝐴
2221a1i 11 . 2 (𝐴𝑉 → ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝐴(𝑥𝑦) ∈ 𝒫 𝐴)
23 pwexg 5333 . . 3 (𝐴𝑉 → 𝒫 𝐴 ∈ V)
24 istopg 22242 . . 3 (𝒫 𝐴 ∈ V → (𝒫 𝐴 ∈ Top ↔ (∀𝑥(𝑥 ⊆ 𝒫 𝐴 𝑥 ∈ 𝒫 𝐴) ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝐴(𝑥𝑦) ∈ 𝒫 𝐴)))
2523, 24syl 17 . 2 (𝐴𝑉 → (𝒫 𝐴 ∈ Top ↔ (∀𝑥(𝑥 ⊆ 𝒫 𝐴 𝑥 ∈ 𝒫 𝐴) ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝐴(𝑥𝑦) ∈ 𝒫 𝐴)))
268, 22, 25mpbir2and 711 1 (𝐴𝑉 → 𝒫 𝐴 ∈ Top)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wal 1539  wcel 2106  wral 3064  Vcvv 3445  cin 3909  wss 3910  𝒫 cpw 4560   cuni 4865  Topctop 22240
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707  ax-sep 5256  ax-pow 5320  ax-pr 5384  ax-un 7671
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3065  df-rab 3408  df-v 3447  df-un 3915  df-in 3917  df-ss 3927  df-pw 4562  df-sn 4587  df-pr 4589  df-uni 4866  df-top 22241
This theorem is referenced by:  topnex  22344  distopon  22345  distps  22364  discld  22438  restdis  22527  dishaus  22731  discmp  22747  dis2ndc  22809  dislly  22846  dis1stc  22848  dissnlocfin  22878  locfindis  22879  txdis  22981  xkopt  23004  xkofvcn  23033  efmndtmd  23450  symgtgp  23455  dispcmp  32431
  Copyright terms: Public domain W3C validator