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

Theorem inopn 21032
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 21028 . . . . 5 (𝐽 ∈ Top → (𝐽 ∈ Top ↔ (∀𝑥(𝑥𝐽 𝑥𝐽) ∧ ∀𝑥𝐽𝑦𝐽 (𝑥𝑦) ∈ 𝐽)))
21ibi 259 . . . 4 (𝐽 ∈ Top → (∀𝑥(𝑥𝐽 𝑥𝐽) ∧ ∀𝑥𝐽𝑦𝐽 (𝑥𝑦) ∈ 𝐽))
32simprd 490 . . 3 (𝐽 ∈ Top → ∀𝑥𝐽𝑦𝐽 (𝑥𝑦) ∈ 𝐽)
4 ineq1 4005 . . . . 5 (𝑥 = 𝐴 → (𝑥𝑦) = (𝐴𝑦))
54eleq1d 2863 . . . 4 (𝑥 = 𝐴 → ((𝑥𝑦) ∈ 𝐽 ↔ (𝐴𝑦) ∈ 𝐽))
6 ineq2 4006 . . . . 5 (𝑦 = 𝐵 → (𝐴𝑦) = (𝐴𝐵))
76eleq1d 2863 . . . 4 (𝑦 = 𝐵 → ((𝐴𝑦) ∈ 𝐽 ↔ (𝐴𝐵) ∈ 𝐽))
85, 7rspc2v 3510 . . 3 ((𝐴𝐽𝐵𝐽) → (∀𝑥𝐽𝑦𝐽 (𝑥𝑦) ∈ 𝐽 → (𝐴𝐵) ∈ 𝐽))
93, 8syl5com 31 . 2 (𝐽 ∈ Top → ((𝐴𝐽𝐵𝐽) → (𝐴𝐵) ∈ 𝐽))
1093impib 1145 1 ((𝐽 ∈ Top ∧ 𝐴𝐽𝐵𝐽) → (𝐴𝐵) ∈ 𝐽)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385  w3a 1108  wal 1651   = wceq 1653  wcel 2157  wral 3089  cin 3768  wss 3769   cuni 4628  Topctop 21026
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777  ax-sep 4975
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ral 3094  df-v 3387  df-in 3776  df-ss 3783  df-pw 4351  df-top 21027
This theorem is referenced by:  fitop  21033  tgclb  21103  topbas  21105  difopn  21167  uncld  21174  ntrin  21194  toponmre  21226  innei  21258  restopnb  21308  ordtopn3  21329  cnprest  21422  islly2  21616  kgentopon  21670  llycmpkgen2  21682  ptbasin  21709  txcnp  21752  txcnmpt  21756  qtoptop2  21831  opnfbas  21974  hauspwpwf1  22119  mopnin  22630  reconnlem2  22958  lmxrge0  30514  cvmsss2  31773  cvmcov2  31774  icccncfext  40844
  Copyright terms: Public domain W3C validator