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

Theorem uniopn 22398
Description: The union of a subset of a topology (that is, the union of any family of open sets of a topology) is an open set. (Contributed by Stefan Allan, 27-Feb-2006.)
Assertion
Ref Expression
uniopn ((𝐽 ∈ Top ∧ 𝐴𝐽) → 𝐴𝐽)

Proof of Theorem uniopn
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 istopg 22396 . . . . 5 (𝐽 ∈ Top → (𝐽 ∈ Top ↔ (∀𝑥(𝑥𝐽 𝑥𝐽) ∧ ∀𝑥𝐽𝑦𝐽 (𝑥𝑦) ∈ 𝐽)))
21ibi 266 . . . 4 (𝐽 ∈ Top → (∀𝑥(𝑥𝐽 𝑥𝐽) ∧ ∀𝑥𝐽𝑦𝐽 (𝑥𝑦) ∈ 𝐽))
32simpld 495 . . 3 (𝐽 ∈ Top → ∀𝑥(𝑥𝐽 𝑥𝐽))
4 elpw2g 5344 . . . . . . . 8 (𝐽 ∈ Top → (𝐴 ∈ 𝒫 𝐽𝐴𝐽))
54biimpar 478 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝐴𝐽) → 𝐴 ∈ 𝒫 𝐽)
6 sseq1 4007 . . . . . . . . 9 (𝑥 = 𝐴 → (𝑥𝐽𝐴𝐽))
7 unieq 4919 . . . . . . . . . 10 (𝑥 = 𝐴 𝑥 = 𝐴)
87eleq1d 2818 . . . . . . . . 9 (𝑥 = 𝐴 → ( 𝑥𝐽 𝐴𝐽))
96, 8imbi12d 344 . . . . . . . 8 (𝑥 = 𝐴 → ((𝑥𝐽 𝑥𝐽) ↔ (𝐴𝐽 𝐴𝐽)))
109spcgv 3586 . . . . . . 7 (𝐴 ∈ 𝒫 𝐽 → (∀𝑥(𝑥𝐽 𝑥𝐽) → (𝐴𝐽 𝐴𝐽)))
115, 10syl 17 . . . . . 6 ((𝐽 ∈ Top ∧ 𝐴𝐽) → (∀𝑥(𝑥𝐽 𝑥𝐽) → (𝐴𝐽 𝐴𝐽)))
1211com23 86 . . . . 5 ((𝐽 ∈ Top ∧ 𝐴𝐽) → (𝐴𝐽 → (∀𝑥(𝑥𝐽 𝑥𝐽) → 𝐴𝐽)))
1312ex 413 . . . 4 (𝐽 ∈ Top → (𝐴𝐽 → (𝐴𝐽 → (∀𝑥(𝑥𝐽 𝑥𝐽) → 𝐴𝐽))))
1413pm2.43d 53 . . 3 (𝐽 ∈ Top → (𝐴𝐽 → (∀𝑥(𝑥𝐽 𝑥𝐽) → 𝐴𝐽)))
153, 14mpid 44 . 2 (𝐽 ∈ Top → (𝐴𝐽 𝐴𝐽))
1615imp 407 1 ((𝐽 ∈ Top ∧ 𝐴𝐽) → 𝐴𝐽)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wal 1539   = wceq 1541  wcel 2106  wral 3061  cin 3947  wss 3948  𝒫 cpw 4602   cuni 4908  Topctop 22394
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 2703  ax-sep 5299
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-in 3955  df-ss 3965  df-pw 4604  df-uni 4909  df-top 22395
This theorem is referenced by:  iunopn  22399  unopn  22404  0opn  22405  topopn  22407  tgtop  22475  ntropn  22552  toponmre  22596  neips  22616  txcmplem1  23144  unimopn  24004  metrest  24032  cnopn  24302  locfinreflem  32815  cvmscld  34259  mblfinlem3  36522  mblfinlem4  36523  ismblfin  36524  topclat  47613  toplatlub  47615
  Copyright terms: Public domain W3C validator