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 21805 | . . . . 5 ⊢ (𝐽 ∈ Top → (𝐽 ∈ Top ↔ (∀𝑥(𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽) ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽))) | |
2 | 1 | ibi 270 | . . . 4 ⊢ (𝐽 ∈ Top → (∀𝑥(𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽) ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽)) |
3 | 2 | simprd 499 | . . 3 ⊢ (𝐽 ∈ Top → ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽) |
4 | ineq1 4129 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝑥 ∩ 𝑦) = (𝐴 ∩ 𝑦)) | |
5 | 4 | eleq1d 2823 | . . . 4 ⊢ (𝑥 = 𝐴 → ((𝑥 ∩ 𝑦) ∈ 𝐽 ↔ (𝐴 ∩ 𝑦) ∈ 𝐽)) |
6 | ineq2 4130 | . . . . 5 ⊢ (𝑦 = 𝐵 → (𝐴 ∩ 𝑦) = (𝐴 ∩ 𝐵)) | |
7 | 6 | eleq1d 2823 | . . . 4 ⊢ (𝑦 = 𝐵 → ((𝐴 ∩ 𝑦) ∈ 𝐽 ↔ (𝐴 ∩ 𝐵) ∈ 𝐽)) |
8 | 5, 7 | rspc2v 3554 | . . 3 ⊢ ((𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽) → (∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽 → (𝐴 ∩ 𝐵) ∈ 𝐽)) |
9 | 3, 8 | syl5com 31 | . 2 ⊢ (𝐽 ∈ Top → ((𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽) → (𝐴 ∩ 𝐵) ∈ 𝐽)) |
10 | 9 | 3impib 1118 | 1 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽) → (𝐴 ∩ 𝐵) ∈ 𝐽) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1089 ∀wal 1541 = wceq 1543 ∈ wcel 2111 ∀wral 3062 ∩ cin 3874 ⊆ wss 3875 ∪ cuni 4828 Topctop 21803 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2113 ax-9 2121 ax-ext 2709 ax-sep 5201 |
This theorem depends on definitions: df-bi 210 df-an 400 df-3an 1091 df-tru 1546 df-ex 1788 df-sb 2072 df-clab 2716 df-cleq 2730 df-clel 2817 df-ral 3067 df-rab 3071 df-v 3417 df-in 3882 df-ss 3892 df-pw 4524 df-top 21804 |
This theorem is referenced by: fitop 21810 tgclb 21880 topbas 21882 difopn 21944 uncld 21951 ntrin 21971 toponmre 22003 innei 22035 restopnb 22085 ordtopn3 22106 cnprest 22199 islly2 22394 kgentopon 22448 llycmpkgen2 22460 ptbasin 22487 txcnp 22530 txcnmpt 22534 qtoptop2 22609 opnfbas 22752 hauspwpwf1 22897 mopnin 23408 reconnlem2 23737 lmxrge0 31629 cvmsss2 32962 cvmcov2 32963 icccncfext 43118 toplatmeet 45977 topdlat 45978 |
Copyright terms: Public domain | W3C validator |