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

Theorem uniopn 22619
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 22617 . . . . 5 (𝐽 ∈ Top → (𝐽 ∈ Top ↔ (∀𝑥(𝑥𝐽 𝑥𝐽) ∧ ∀𝑥𝐽𝑦𝐽 (𝑥𝑦) ∈ 𝐽)))
21ibi 266 . . . 4 (𝐽 ∈ Top → (∀𝑥(𝑥𝐽 𝑥𝐽) ∧ ∀𝑥𝐽𝑦𝐽 (𝑥𝑦) ∈ 𝐽))
32simpld 493 . . 3 (𝐽 ∈ Top → ∀𝑥(𝑥𝐽 𝑥𝐽))
4 elpw2g 5343 . . . . . . . 8 (𝐽 ∈ Top → (𝐴 ∈ 𝒫 𝐽𝐴𝐽))
54biimpar 476 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝐴𝐽) → 𝐴 ∈ 𝒫 𝐽)
6 sseq1 4006 . . . . . . . . 9 (𝑥 = 𝐴 → (𝑥𝐽𝐴𝐽))
7 unieq 4918 . . . . . . . . . 10 (𝑥 = 𝐴 𝑥 = 𝐴)
87eleq1d 2816 . . . . . . . . 9 (𝑥 = 𝐴 → ( 𝑥𝐽 𝐴𝐽))
96, 8imbi12d 343 . . . . . . . 8 (𝑥 = 𝐴 → ((𝑥𝐽 𝑥𝐽) ↔ (𝐴𝐽 𝐴𝐽)))
109spcgv 3585 . . . . . . 7 (𝐴 ∈ 𝒫 𝐽 → (∀𝑥(𝑥𝐽 𝑥𝐽) → (𝐴𝐽 𝐴𝐽)))
115, 10syl 17 . . . . . 6 ((𝐽 ∈ Top ∧ 𝐴𝐽) → (∀𝑥(𝑥𝐽 𝑥𝐽) → (𝐴𝐽 𝐴𝐽)))
1211com23 86 . . . . 5 ((𝐽 ∈ Top ∧ 𝐴𝐽) → (𝐴𝐽 → (∀𝑥(𝑥𝐽 𝑥𝐽) → 𝐴𝐽)))
1312ex 411 . . . 4 (𝐽 ∈ Top → (𝐴𝐽 → (𝐴𝐽 → (∀𝑥(𝑥𝐽 𝑥𝐽) → 𝐴𝐽))))
1413pm2.43d 53 . . 3 (𝐽 ∈ Top → (𝐴𝐽 → (∀𝑥(𝑥𝐽 𝑥𝐽) → 𝐴𝐽)))
153, 14mpid 44 . 2 (𝐽 ∈ Top → (𝐴𝐽 𝐴𝐽))
1615imp 405 1 ((𝐽 ∈ Top ∧ 𝐴𝐽) → 𝐴𝐽)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  wal 1537   = wceq 1539  wcel 2104  wral 3059  cin 3946  wss 3947  𝒫 cpw 4601   cuni 4907  Topctop 22615
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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-sep 5298
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-in 3954  df-ss 3964  df-pw 4603  df-uni 4908  df-top 22616
This theorem is referenced by:  iunopn  22620  unopn  22625  0opn  22626  topopn  22628  tgtop  22696  ntropn  22773  toponmre  22817  neips  22837  txcmplem1  23365  unimopn  24225  metrest  24253  cnopn  24523  locfinreflem  33118  cvmscld  34562  mblfinlem3  36830  mblfinlem4  36831  ismblfin  36832  topclat  47710  toplatlub  47712
  Copyright terms: Public domain W3C validator