| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > inopn | Structured version Visualization version GIF version | ||
| Description: The intersection of two open sets of a topology is an open set. (Contributed by NM, 17-Jul-2006.) |
| Ref | Expression |
|---|---|
| inopn | ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽) → (𝐴 ∩ 𝐵) ∈ 𝐽) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | istopg 22901 | . . . . 5 ⊢ (𝐽 ∈ Top → (𝐽 ∈ Top ↔ (∀𝑥(𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽) ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽))) | |
| 2 | 1 | ibi 267 | . . . 4 ⊢ (𝐽 ∈ Top → (∀𝑥(𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽) ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽)) |
| 3 | 2 | simprd 495 | . . 3 ⊢ (𝐽 ∈ Top → ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽) |
| 4 | ineq1 4213 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∩ 𝑦) = (𝐴 ∩ 𝑦)) | |
| 5 | 4 | eleq1d 2826 | . . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∩ 𝑦) ∈ 𝐽 ↔ (𝐴 ∩ 𝑦) ∈ 𝐽)) |
| 6 | ineq2 4214 | . . . . 5 ⊢ (𝑦 = 𝐵 → (𝐴 ∩ 𝑦) = (𝐴 ∩ 𝐵)) | |
| 7 | 6 | eleq1d 2826 | . . . 4 ⊢ (𝑦 = 𝐵 → ((𝐴 ∩ 𝑦) ∈ 𝐽 ↔ (𝐴 ∩ 𝐵) ∈ 𝐽)) |
| 8 | 5, 7 | rspc2v 3633 | . . 3 ⊢ ((𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽) → (∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽 → (𝐴 ∩ 𝐵) ∈ 𝐽)) |
| 9 | 3, 8 | syl5com 31 | . 2 ⊢ (𝐽 ∈ Top → ((𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽) → (𝐴 ∩ 𝐵) ∈ 𝐽)) |
| 10 | 9 | 3impib 1117 | 1 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽) → (𝐴 ∩ 𝐵) ∈ 𝐽) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 ∀wal 1538 = wceq 1540 ∈ wcel 2108 ∀wral 3061 ∩ cin 3950 ⊆ wss 3951 ∪ cuni 4907 Topctop 22899 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-sep 5296 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1089 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-in 3958 df-ss 3968 df-pw 4602 df-top 22900 |
| This theorem is referenced by: fitop 22906 tgclb 22977 topbas 22979 difopn 23042 uncld 23049 ntrin 23069 toponmre 23101 innei 23133 restopnb 23183 ordtopn3 23204 cnprest 23297 islly2 23492 kgentopon 23546 llycmpkgen2 23558 ptbasin 23585 txcnp 23628 txcnmpt 23632 qtoptop2 23707 opnfbas 23850 hauspwpwf1 23995 mopnin 24510 reconnlem2 24849 lmxrge0 33951 cvmsss2 35279 cvmcov2 35280 inopnd 45154 icccncfext 45902 toplatmeet 48892 topdlat 48893 |
| Copyright terms: Public domain | W3C validator |