Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  distop GIF version

Theorem distop 12294
 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 3765 . . . . . 6 (𝑥 ⊆ 𝒫 𝐴 𝑥 𝒫 𝐴)
2 unipw 4147 . . . . . 6 𝒫 𝐴 = 𝐴
31, 2sseqtrdi 3150 . . . . 5 (𝑥 ⊆ 𝒫 𝐴 𝑥𝐴)
4 vuniex 4368 . . . . . 6 𝑥 ∈ V
54elpw 3521 . . . . 5 ( 𝑥 ∈ 𝒫 𝐴 𝑥𝐴)
63, 5sylibr 133 . . . 4 (𝑥 ⊆ 𝒫 𝐴 𝑥 ∈ 𝒫 𝐴)
76ax-gen 1426 . . 3 𝑥(𝑥 ⊆ 𝒫 𝐴 𝑥 ∈ 𝒫 𝐴)
87a1i 9 . 2 (𝐴𝑉 → ∀𝑥(𝑥 ⊆ 𝒫 𝐴 𝑥 ∈ 𝒫 𝐴))
9 velpw 3522 . . . . . 6 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
10 velpw 3522 . . . . . . . 8 (𝑦 ∈ 𝒫 𝐴𝑦𝐴)
11 ssinss1 3310 . . . . . . . . . 10 (𝑥𝐴 → (𝑥𝑦) ⊆ 𝐴)
1211a1i 9 . . . . . . . . 9 (𝑦𝐴 → (𝑥𝐴 → (𝑥𝑦) ⊆ 𝐴))
13 vex 2692 . . . . . . . . . . 11 𝑦 ∈ V
1413inex2 4071 . . . . . . . . . 10 (𝑥𝑦) ∈ V
1514elpw 3521 . . . . . . . . 9 ((𝑥𝑦) ∈ 𝒫 𝐴 ↔ (𝑥𝑦) ⊆ 𝐴)
1612, 15syl6ibr 161 . . . . . . . 8 (𝑦𝐴 → (𝑥𝐴 → (𝑥𝑦) ∈ 𝒫 𝐴))
1710, 16sylbi 120 . . . . . . 7 (𝑦 ∈ 𝒫 𝐴 → (𝑥𝐴 → (𝑥𝑦) ∈ 𝒫 𝐴))
1817com12 30 . . . . . 6 (𝑥𝐴 → (𝑦 ∈ 𝒫 𝐴 → (𝑥𝑦) ∈ 𝒫 𝐴))
199, 18sylbi 120 . . . . 5 (𝑥 ∈ 𝒫 𝐴 → (𝑦 ∈ 𝒫 𝐴 → (𝑥𝑦) ∈ 𝒫 𝐴))
2019ralrimiv 2507 . . . 4 (𝑥 ∈ 𝒫 𝐴 → ∀𝑦 ∈ 𝒫 𝐴(𝑥𝑦) ∈ 𝒫 𝐴)
2120rgen 2488 . . 3 𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝐴(𝑥𝑦) ∈ 𝒫 𝐴
2221a1i 9 . 2 (𝐴𝑉 → ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝐴(𝑥𝑦) ∈ 𝒫 𝐴)
23 pwexg 4112 . . 3 (𝐴𝑉 → 𝒫 𝐴 ∈ V)
24 istopg 12206 . . 3 (𝒫 𝐴 ∈ V → (𝒫 𝐴 ∈ Top ↔ (∀𝑥(𝑥 ⊆ 𝒫 𝐴 𝑥 ∈ 𝒫 𝐴) ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝐴(𝑥𝑦) ∈ 𝒫 𝐴)))
2523, 24syl 14 . 2 (𝐴𝑉 → (𝒫 𝐴 ∈ Top ↔ (∀𝑥(𝑥 ⊆ 𝒫 𝐴 𝑥 ∈ 𝒫 𝐴) ∧ ∀𝑥 ∈ 𝒫 𝐴𝑦 ∈ 𝒫 𝐴(𝑥𝑦) ∈ 𝒫 𝐴)))
268, 22, 25mpbir2and 929 1 (𝐴𝑉 → 𝒫 𝐴 ∈ Top)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104  ∀wal 1330   ∈ wcel 1481  ∀wral 2417  Vcvv 2689   ∩ cin 3075   ⊆ wss 3076  𝒫 cpw 3515  ∪ cuni 3744  Topctop 12204 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4054  ax-pow 4106  ax-un 4363 This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-rex 2423  df-v 2691  df-in 3082  df-ss 3089  df-pw 3517  df-sn 3538  df-uni 3745  df-top 12205 This theorem is referenced by:  topnex  12295  distopon  12296  distps  12300  discld  12345  restdis  12393  txdis  12486
 Copyright terms: Public domain W3C validator