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

Theorem istopon 21512
 Description: Property of being a topology with a given base set. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Revised by Mario Carneiro, 13-Aug-2015.)
Assertion
Ref Expression
istopon (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = 𝐽))

Proof of Theorem istopon
Dummy variables 𝑏 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elfvex 6696 . 2 (𝐽 ∈ (TopOn‘𝐵) → 𝐵 ∈ V)
2 uniexg 7458 . . . 4 (𝐽 ∈ Top → 𝐽 ∈ V)
3 eleq1 2898 . . . 4 (𝐵 = 𝐽 → (𝐵 ∈ V ↔ 𝐽 ∈ V))
42, 3syl5ibrcom 249 . . 3 (𝐽 ∈ Top → (𝐵 = 𝐽𝐵 ∈ V))
54imp 409 . 2 ((𝐽 ∈ Top ∧ 𝐵 = 𝐽) → 𝐵 ∈ V)
6 eqeq1 2823 . . . . . 6 (𝑏 = 𝐵 → (𝑏 = 𝑗𝐵 = 𝑗))
76rabbidv 3479 . . . . 5 (𝑏 = 𝐵 → {𝑗 ∈ Top ∣ 𝑏 = 𝑗} = {𝑗 ∈ Top ∣ 𝐵 = 𝑗})
8 df-topon 21511 . . . . 5 TopOn = (𝑏 ∈ V ↦ {𝑗 ∈ Top ∣ 𝑏 = 𝑗})
9 vpwex 5269 . . . . . . 7 𝒫 𝑏 ∈ V
109pwex 5272 . . . . . 6 𝒫 𝒫 𝑏 ∈ V
11 rabss 4046 . . . . . . 7 ({𝑗 ∈ Top ∣ 𝑏 = 𝑗} ⊆ 𝒫 𝒫 𝑏 ↔ ∀𝑗 ∈ Top (𝑏 = 𝑗𝑗 ∈ 𝒫 𝒫 𝑏))
12 pwuni 4866 . . . . . . . . . 10 𝑗 ⊆ 𝒫 𝑗
13 pweq 4540 . . . . . . . . . 10 (𝑏 = 𝑗 → 𝒫 𝑏 = 𝒫 𝑗)
1412, 13sseqtrrid 4018 . . . . . . . . 9 (𝑏 = 𝑗𝑗 ⊆ 𝒫 𝑏)
15 velpw 4545 . . . . . . . . 9 (𝑗 ∈ 𝒫 𝒫 𝑏𝑗 ⊆ 𝒫 𝑏)
1614, 15sylibr 236 . . . . . . . 8 (𝑏 = 𝑗𝑗 ∈ 𝒫 𝒫 𝑏)
1716a1i 11 . . . . . . 7 (𝑗 ∈ Top → (𝑏 = 𝑗𝑗 ∈ 𝒫 𝒫 𝑏))
1811, 17mprgbir 3151 . . . . . 6 {𝑗 ∈ Top ∣ 𝑏 = 𝑗} ⊆ 𝒫 𝒫 𝑏
1910, 18ssexi 5217 . . . . 5 {𝑗 ∈ Top ∣ 𝑏 = 𝑗} ∈ V
207, 8, 19fvmpt3i 6766 . . . 4 (𝐵 ∈ V → (TopOn‘𝐵) = {𝑗 ∈ Top ∣ 𝐵 = 𝑗})
2120eleq2d 2896 . . 3 (𝐵 ∈ V → (𝐽 ∈ (TopOn‘𝐵) ↔ 𝐽 ∈ {𝑗 ∈ Top ∣ 𝐵 = 𝑗}))
22 unieq 4838 . . . . 5 (𝑗 = 𝐽 𝑗 = 𝐽)
2322eqeq2d 2830 . . . 4 (𝑗 = 𝐽 → (𝐵 = 𝑗𝐵 = 𝐽))
2423elrab 3678 . . 3 (𝐽 ∈ {𝑗 ∈ Top ∣ 𝐵 = 𝑗} ↔ (𝐽 ∈ Top ∧ 𝐵 = 𝐽))
2521, 24syl6bb 289 . 2 (𝐵 ∈ V → (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = 𝐽)))
261, 5, 25pm5.21nii 382 1 (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = 𝐽))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1531   ∈ wcel 2108  {crab 3140  Vcvv 3493   ⊆ wss 3934  𝒫 cpw 4537  ∪ cuni 4830  ‘cfv 6348  Topctop 21493  TopOnctopon 21510 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-sbc 3771  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-iota 6307  df-fun 6350  df-fv 6356  df-topon 21511 This theorem is referenced by:  topontop  21513  toponuni  21514  toptopon  21517  toponcom  21528  istps2  21535  tgtopon  21571  distopon  21597  indistopon  21601  fctop  21604  cctop  21606  ppttop  21607  epttop  21609  mretopd  21692  toponmre  21693  resttopon  21761  resttopon2  21768  kgentopon  22138  txtopon  22191  pttopon  22196  xkotopon  22200  qtoptopon  22304  flimtopon  22570  fclstopon  22612  fclsfnflim  22627  utoptopon  22837  qtopt1  31092  neibastop1  33700  onsuctopon  33775  rfcnpre1  41266  cnfex  41275  icccncfext  42159  stoweidlem47  42322
 Copyright terms: Public domain W3C validator