Theorem inopn 22029

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 22025	. . . . 5 ⊢ (𝐽 ∈ Top → (𝐽 ∈ Top ↔ (∀𝑥(𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽) ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽)))
2	1	ibi 266	. . . 4 ⊢ (𝐽 ∈ Top → (∀𝑥(𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽) ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽))
3	2	simprd 495	. . 3 ⊢ (𝐽 ∈ Top → ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽)
4		ineq1 4144	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∩ 𝑦) = (𝐴 ∩ 𝑦))
5	4	eleq1d 2824	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∩ 𝑦) ∈ 𝐽 ↔ (𝐴 ∩ 𝑦) ∈ 𝐽))
6		ineq2 4145	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝐴 ∩ 𝑦) = (𝐴 ∩ 𝐵))
7	6	eleq1d 2824	. . . 4 ⊢ (𝑦 = 𝐵 → ((𝐴 ∩ 𝑦) ∈ 𝐽 ↔ (𝐴 ∩ 𝐵) ∈ 𝐽))
8	5, 7	rspc2v 3570	. . 3 ⊢ ((𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽) → (∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽 → (𝐴 ∩ 𝐵) ∈ 𝐽))
9	3, 8	syl5com 31	. 2 ⊢ (𝐽 ∈ Top → ((𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽) → (𝐴 ∩ 𝐵) ∈ 𝐽))
10	9	3impib 1114	1 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽) → (𝐴 ∩ 𝐵) ∈ 𝐽)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085  ∀wal 1539   = wceq 1541   ∈ wcel 2109  ∀wral 3065   ∩ cin 3890   ⊆ wss 3891  ∪ cuni 4844  Topctop 22023

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710  ax-sep 5226

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1087  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rab 3074  df-v 3432  df-in 3898  df-ss 3908  df-pw 4540  df-top 22024

This theorem is referenced by:  fitop  22030  tgclb  22101  topbas  22103  difopn  22166  uncld  22173  ntrin  22193  toponmre  22225  innei  22257  restopnb  22307  ordtopn3  22328  cnprest  22421  islly2  22616  kgentopon  22670  llycmpkgen2  22682  ptbasin  22709  txcnp  22752  txcnmpt  22756  qtoptop2  22831  opnfbas  22974  hauspwpwf1  23119  mopnin  23634  reconnlem2  23971  lmxrge0  31881  cvmsss2  33215  cvmcov2  33216  icccncfext  43382  toplatmeet  46241  topdlat  46242