Theorem inopn 23222

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 23218	. . . . 5 ⊢ (𝐽 ∈ Top → (𝐽 ∈ Top ↔ (∀𝑥(𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽) ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽)))
2	1	ibi 270	. . . 4 ⊢ (𝐽 ∈ Top → (∀𝑥(𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽) ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽))
3	2	simprd 501	. . 3 ⊢ (𝐽 ∈ Top → ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽)
4		ineq1 4110	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∩ 𝑦) = (𝐴 ∩ 𝑦))
5	4	eleq1d 2845	. . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∩ 𝑦) ∈ 𝐽 ↔ (𝐴 ∩ 𝑦) ∈ 𝐽))
6		ineq2 4111	. . . . 5 ⊢ (𝑦 = 𝐵 → (𝐴 ∩ 𝑦) = (𝐴 ∩ 𝐵))
7	6	eleq1d 2845	. . . 4 ⊢ (𝑦 = 𝐵 → ((𝐴 ∩ 𝑦) ∈ 𝐽 ↔ (𝐴 ∩ 𝐵) ∈ 𝐽))
8	5, 7	rspc2v 3586	. . 3 ⊢ ((𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽) → (∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽 → (𝐴 ∩ 𝐵) ∈ 𝐽))
9	3, 8	syl5com 32	. 2 ⊢ (𝐽 ∈ Top → ((𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽) → (𝐴 ∩ 𝐵) ∈ 𝐽))
10	9	3impib 1134	1 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽) → (𝐴 ∩ 𝐵) ∈ 𝐽)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103  ∀wal 1567   = wceq 1569   ∈ wcel 2144  ∀wral 3076   ⊆ wss 3895   ∩ cin 4089  ∪ cuni 4866  Topctop 23216

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-in 4091  df-pw 4558  df-top 23217

This theorem is used by:  fitop  23223  tgclb  23293  topbas  23295  difopn  23357  uncld  23364  ntrin  23384  toponmre  23416  innei  23448  restopnb  23498  ordtopn3  23519  cnprest  23612  islly2  23808  kgentopon  23862  llycmpkgen2  23874  ptbasin  23901  txcnp  23944  txcnmpt  23948  qtoptop2  24023  opnfbas  24166  hauspwpwf1  24311  mopnin  24821  reconnlem2  25152  lmxrge0  34630  cvmsss2  36125  cvmcov2  36126  inopnd  46257  icccncfext  46990  toplatmeet  50210  topdlat  50211