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

Theorem uniopn 20527
 Description: The union of a subset 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 20525 . . . . 5 (𝐽 ∈ Top → (𝐽 ∈ Top ↔ (∀𝑥(𝑥𝐽 𝑥𝐽) ∧ ∀𝑥𝐽𝑦𝐽 (𝑥𝑦) ∈ 𝐽)))
21ibi 255 . . . 4 (𝐽 ∈ Top → (∀𝑥(𝑥𝐽 𝑥𝐽) ∧ ∀𝑥𝐽𝑦𝐽 (𝑥𝑦) ∈ 𝐽))
32simpld 474 . . 3 (𝐽 ∈ Top → ∀𝑥(𝑥𝐽 𝑥𝐽))
4 elpw2g 4754 . . . . . . . 8 (𝐽 ∈ Top → (𝐴 ∈ 𝒫 𝐽𝐴𝐽))
54biimpar 501 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝐴𝐽) → 𝐴 ∈ 𝒫 𝐽)
6 sseq1 3589 . . . . . . . . 9 (𝑥 = 𝐴 → (𝑥𝐽𝐴𝐽))
7 unieq 4380 . . . . . . . . . 10 (𝑥 = 𝐴 𝑥 = 𝐴)
87eleq1d 2672 . . . . . . . . 9 (𝑥 = 𝐴 → ( 𝑥𝐽 𝐴𝐽))
96, 8imbi12d 333 . . . . . . . 8 (𝑥 = 𝐴 → ((𝑥𝐽 𝑥𝐽) ↔ (𝐴𝐽 𝐴𝐽)))
109spcgv 3266 . . . . . . 7 (𝐴 ∈ 𝒫 𝐽 → (∀𝑥(𝑥𝐽 𝑥𝐽) → (𝐴𝐽 𝐴𝐽)))
115, 10syl 17 . . . . . 6 ((𝐽 ∈ Top ∧ 𝐴𝐽) → (∀𝑥(𝑥𝐽 𝑥𝐽) → (𝐴𝐽 𝐴𝐽)))
1211com23 84 . . . . 5 ((𝐽 ∈ Top ∧ 𝐴𝐽) → (𝐴𝐽 → (∀𝑥(𝑥𝐽 𝑥𝐽) → 𝐴𝐽)))
1312ex 449 . . . 4 (𝐽 ∈ Top → (𝐴𝐽 → (𝐴𝐽 → (∀𝑥(𝑥𝐽 𝑥𝐽) → 𝐴𝐽))))
1413pm2.43d 51 . . 3 (𝐽 ∈ Top → (𝐴𝐽 → (∀𝑥(𝑥𝐽 𝑥𝐽) → 𝐴𝐽)))
153, 14mpid 43 . 2 (𝐽 ∈ Top → (𝐴𝐽 𝐴𝐽))
1615imp 444 1 ((𝐽 ∈ Top ∧ 𝐴𝐽) → 𝐴𝐽)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383  ∀wal 1473   = wceq 1475   ∈ wcel 1977  ∀wral 2896   ∩ cin 3539   ⊆ wss 3540  𝒫 cpw 4108  ∪ cuni 4372  Topctop 20517 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-v 3175  df-in 3547  df-ss 3554  df-pw 4110  df-uni 4373  df-top 20521 This theorem is referenced by:  iunopn  20528  unopn  20533  0opn  20534  topopn  20536  tgtop  20588  ntropn  20663  toponmre  20707  neips  20727  txcmplem1  21254  unimopn  22111  metrest  22139  locfinreflem  29235  cvmscld  30509  mblfinlem3  32618  mblfinlem4  32619  ismblfin  32620  cnopn  38233
 Copyright terms: Public domain W3C validator