Theorem inopn 23017

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.

Step	Hyp	Ref	Expression
1		istopg 23013	. . . . 5 ⊢ (𝐽 ∈ Top → (𝐽 ∈ Top ↔ (∀𝑥(𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽) ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽)))
2	1	ibi 270	. . . 4 ⊢ (𝐽 ∈ Top → (∀𝑥(𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽) ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽))
3	2	simprd 500	. . 3 ⊢ (𝐽 ∈ Top → ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽)
4		ineq1 4168	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∩ 𝑦) = (𝐴 ∩ 𝑦))
5	4	eleq1d 2850	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∩ 𝑦) ∈ 𝐽 ↔ (𝐴 ∩ 𝑦) ∈ 𝐽))
6		ineq2 4169	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝐴 ∩ 𝑦) = (𝐴 ∩ 𝐵))
7	6	eleq1d 2850	. . . 4 ⊢ (𝑦 = 𝐵 → ((𝐴 ∩ 𝑦) ∈ 𝐽 ↔ (𝐴 ∩ 𝐵) ∈ 𝐽))
8	5, 7	rspc2v 3595	. . 3 ⊢ ((𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽) → (∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽 → (𝐴 ∩ 𝐵) ∈ 𝐽))
9	3, 8	syl5com 32	. 2 ⊢ (𝐽 ∈ Top → ((𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽) → (𝐴 ∩ 𝐵) ∈ 𝐽))
10	9	3impib 1132	1 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽) → (𝐴 ∩ 𝐵) ∈ 𝐽)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101  ∀wal 1561   = wceq 1563   ∈ wcel 2145  ∀wral 3079   ∩ cin 3906   ⊆ wss 3907  ∪ cuni 4868  Topctop 23011

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5251

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-in 3914  df-ss 3924  df-pw 4560  df-top 23012

This theorem is referenced by:  fitop  23018  tgclb  23088  topbas  23090  difopn  23152  uncld  23159  ntrin  23179  toponmre  23211  innei  23243  restopnb  23293  ordtopn3  23314  cnprest  23407  islly2  23602  kgentopon  23656  llycmpkgen2  23668  ptbasin  23695  txcnp  23738  txcnmpt  23742  qtoptop2  23817  opnfbas  23960  hauspwpwf1  24105  mopnin  24615  reconnlem2  24946  lmxrge0  34259  cvmsss2  35637  cvmcov2  35638  inopnd  45725  icccncfext  46459  toplatmeet  49632  topdlat  49633