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

Theorem distop 23002
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 4915 . . . . . 6 (𝑥 ⊆ 𝒫 𝐴 𝑥 𝒫 𝐴)
2 unipw 5455 . . . . . 6 𝒫 𝐴 = 𝐴
31, 2sseqtrdi 4024 . . . . 5 (𝑥 ⊆ 𝒫 𝐴 𝑥𝐴)
4 vuniex 7759 . . . . . 6 𝑥 ∈ V
54elpw 4604 . . . . 5 ( 𝑥 ∈ 𝒫 𝐴 𝑥𝐴)
63, 5sylibr 234 . . . 4 (𝑥 ⊆ 𝒫 𝐴 𝑥 ∈ 𝒫 𝐴)
76ax-gen 1795 . . 3 𝑥(𝑥 ⊆ 𝒫 𝐴 𝑥 ∈ 𝒫 𝐴)
87a1i 11 . 2 (𝐴𝑉 → ∀𝑥(𝑥 ⊆ 𝒫 𝐴 𝑥 ∈ 𝒫 𝐴))
9 velpw 4605 . . . . . 6 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
10 velpw 4605 . . . . . . . 8 (𝑦 ∈ 𝒫 𝐴𝑦𝐴)
11 ssinss1 4246 . . . . . . . . . 10 (𝑥𝐴 → (𝑥𝑦) ⊆ 𝐴)
1211a1i 11 . . . . . . . . 9 (𝑦𝐴 → (𝑥𝐴 → (𝑥𝑦) ⊆ 𝐴))
13 vex 3484 . . . . . . . . . . 11 𝑦 ∈ V
1413inex2 5318 . . . . . . . . . 10 (𝑥𝑦) ∈ V
1514elpw 4604 . . . . . . . . 9 ((𝑥𝑦) ∈ 𝒫 𝐴 ↔ (𝑥𝑦) ⊆ 𝐴)
1612, 15imbitrrdi 252 . . . . . . . 8 (𝑦𝐴 → (𝑥𝐴 → (𝑥𝑦) ∈ 𝒫 𝐴))
1710, 16sylbi 217 . . . . . . 7 (𝑦 ∈ 𝒫 𝐴 → (𝑥𝐴 → (𝑥𝑦) ∈ 𝒫 𝐴))
1817com12 32 . . . . . 6 (𝑥𝐴 → (𝑦 ∈ 𝒫 𝐴 → (𝑥𝑦) ∈ 𝒫 𝐴))
199, 18sylbi 217 . . . . 5 (𝑥 ∈ 𝒫 𝐴 → (𝑦 ∈ 𝒫 𝐴 → (𝑥𝑦) ∈ 𝒫 𝐴))
2019ralrimiv 3145 . . . 4 (𝑥 ∈ 𝒫 𝐴 → ∀𝑦 ∈ 𝒫 𝐴(𝑥𝑦) ∈ 𝒫 𝐴)
2120rgen 3063 . . 3 𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝐴(𝑥𝑦) ∈ 𝒫 𝐴
2221a1i 11 . 2 (𝐴𝑉 → ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝐴(𝑥𝑦) ∈ 𝒫 𝐴)
23 pwexg 5378 . . 3 (𝐴𝑉 → 𝒫 𝐴 ∈ V)
24 istopg 22901 . . 3 (𝒫 𝐴 ∈ V → (𝒫 𝐴 ∈ Top ↔ (∀𝑥(𝑥 ⊆ 𝒫 𝐴 𝑥 ∈ 𝒫 𝐴) ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝐴(𝑥𝑦) ∈ 𝒫 𝐴)))
2523, 24syl 17 . 2 (𝐴𝑉 → (𝒫 𝐴 ∈ Top ↔ (∀𝑥(𝑥 ⊆ 𝒫 𝐴 𝑥 ∈ 𝒫 𝐴) ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝐴(𝑥𝑦) ∈ 𝒫 𝐴)))
268, 22, 25mpbir2and 713 1 (𝐴𝑉 → 𝒫 𝐴 ∈ Top)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wal 1538  wcel 2108  wral 3061  Vcvv 3480  cin 3950  wss 3951  𝒫 cpw 4600   cuni 4907  Topctop 22899
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-un 3956  df-in 3958  df-ss 3968  df-pw 4602  df-sn 4627  df-pr 4629  df-uni 4908  df-top 22900
This theorem is referenced by:  topnex  23003  distopon  23004  distps  23023  discld  23097  restdis  23186  dishaus  23390  discmp  23406  dis2ndc  23468  dislly  23505  dis1stc  23507  dissnlocfin  23537  locfindis  23538  txdis  23640  xkopt  23663  xkofvcn  23692  efmndtmd  24109  symgtgp  24114  dispcmp  33858
  Copyright terms: Public domain W3C validator