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

Theorem inopn 21809
Description: The intersection of two open sets of a topology is an open set. (Contributed by NM, 17-Jul-2006.)
Assertion
Ref Expression
inopn ((𝐽 ∈ Top ∧ 𝐴𝐽𝐵𝐽) → (𝐴𝐵) ∈ 𝐽)

Proof of Theorem inopn
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 istopg 21805 . . . . 5 (𝐽 ∈ Top → (𝐽 ∈ Top ↔ (∀𝑥(𝑥𝐽 𝑥𝐽) ∧ ∀𝑥𝐽𝑦𝐽 (𝑥𝑦) ∈ 𝐽)))
21ibi 270 . . . 4 (𝐽 ∈ Top → (∀𝑥(𝑥𝐽 𝑥𝐽) ∧ ∀𝑥𝐽𝑦𝐽 (𝑥𝑦) ∈ 𝐽))
32simprd 499 . . 3 (𝐽 ∈ Top → ∀𝑥𝐽𝑦𝐽 (𝑥𝑦) ∈ 𝐽)
4 ineq1 4129 . . . . 5 (𝑥 = 𝐴 → (𝑥𝑦) = (𝐴𝑦))
54eleq1d 2823 . . . 4 (𝑥 = 𝐴 → ((𝑥𝑦) ∈ 𝐽 ↔ (𝐴𝑦) ∈ 𝐽))
6 ineq2 4130 . . . . 5 (𝑦 = 𝐵 → (𝐴𝑦) = (𝐴𝐵))
76eleq1d 2823 . . . 4 (𝑦 = 𝐵 → ((𝐴𝑦) ∈ 𝐽 ↔ (𝐴𝐵) ∈ 𝐽))
85, 7rspc2v 3554 . . 3 ((𝐴𝐽𝐵𝐽) → (∀𝑥𝐽𝑦𝐽 (𝑥𝑦) ∈ 𝐽 → (𝐴𝐵) ∈ 𝐽))
93, 8syl5com 31 . 2 (𝐽 ∈ Top → ((𝐴𝐽𝐵𝐽) → (𝐴𝐵) ∈ 𝐽))
1093impib 1118 1 ((𝐽 ∈ Top ∧ 𝐴𝐽𝐵𝐽) → (𝐴𝐵) ∈ 𝐽)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1089  wal 1541   = wceq 1543  wcel 2111  wral 3062  cin 3874  wss 3875   cuni 4828  Topctop 21803
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-ext 2709  ax-sep 5201
This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1091  df-tru 1546  df-ex 1788  df-sb 2072  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3067  df-rab 3071  df-v 3417  df-in 3882  df-ss 3892  df-pw 4524  df-top 21804
This theorem is referenced by:  fitop  21810  tgclb  21880  topbas  21882  difopn  21944  uncld  21951  ntrin  21971  toponmre  22003  innei  22035  restopnb  22085  ordtopn3  22106  cnprest  22199  islly2  22394  kgentopon  22448  llycmpkgen2  22460  ptbasin  22487  txcnp  22530  txcnmpt  22534  qtoptop2  22609  opnfbas  22752  hauspwpwf1  22897  mopnin  23408  reconnlem2  23737  lmxrge0  31629  cvmsss2  32962  cvmcov2  32963  icccncfext  43118  toplatmeet  45977  topdlat  45978
  Copyright terms: Public domain W3C validator