Mathbox for Zhi Wang |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > iscnrm3rlem7 | Structured version Visualization version GIF version |
Description: Lemma for iscnrm3rlem8 45693. Open neighborhoods in the subspace topology are open neighborhoods in the original topology given that the subspace is an open set in the original topology. (Contributed by Zhi Wang, 5-Sep-2024.) |
Ref | Expression |
---|---|
iscnrm3rlem4.1 | ⊢ (𝜑 → 𝐽 ∈ Top) |
iscnrm3rlem4.2 | ⊢ (𝜑 → 𝑆 ⊆ ∪ 𝐽) |
iscnrm3rlem5.3 | ⊢ (𝜑 → 𝑇 ⊆ ∪ 𝐽) |
iscnrm3rlem7.4 | ⊢ (𝜑 → 𝑂 ∈ (𝐽 ↾t (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇))))) |
Ref | Expression |
---|---|
iscnrm3rlem7 | ⊢ (𝜑 → 𝑂 ∈ 𝐽) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iscnrm3rlem7.4 | . 2 ⊢ (𝜑 → 𝑂 ∈ (𝐽 ↾t (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇))))) | |
2 | iscnrm3rlem4.1 | . . 3 ⊢ (𝜑 → 𝐽 ∈ Top) | |
3 | iscnrm3rlem4.2 | . . 3 ⊢ (𝜑 → 𝑆 ⊆ ∪ 𝐽) | |
4 | iscnrm3rlem5.3 | . . 3 ⊢ (𝜑 → 𝑇 ⊆ ∪ 𝐽) | |
5 | 2 | uniexd 7473 | . . . . . . 7 ⊢ (𝜑 → ∪ 𝐽 ∈ V) |
6 | 5 | difexd 5204 | . . . . . 6 ⊢ (𝜑 → (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇))) ∈ V) |
7 | resttop 21875 | . . . . . 6 ⊢ ((𝐽 ∈ Top ∧ (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇))) ∈ V) → (𝐽 ↾t (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇)))) ∈ Top) | |
8 | 2, 6, 7 | syl2anc 587 | . . . . 5 ⊢ (𝜑 → (𝐽 ↾t (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇)))) ∈ Top) |
9 | eqid 2759 | . . . . . 6 ⊢ ∪ (𝐽 ↾t (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇)))) = ∪ (𝐽 ↾t (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇)))) | |
10 | 9 | eltopss 21622 | . . . . 5 ⊢ (((𝐽 ↾t (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇)))) ∈ Top ∧ 𝑂 ∈ (𝐽 ↾t (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇))))) → 𝑂 ⊆ ∪ (𝐽 ↾t (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇))))) |
11 | 8, 1, 10 | syl2anc 587 | . . . 4 ⊢ (𝜑 → 𝑂 ⊆ ∪ (𝐽 ↾t (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇))))) |
12 | difssd 4041 | . . . . 5 ⊢ (𝜑 → (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇))) ⊆ ∪ 𝐽) | |
13 | eqid 2759 | . . . . . 6 ⊢ ∪ 𝐽 = ∪ 𝐽 | |
14 | 13 | restuni 21877 | . . . . 5 ⊢ ((𝐽 ∈ Top ∧ (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇))) ⊆ ∪ 𝐽) → (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇))) = ∪ (𝐽 ↾t (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇))))) |
15 | 2, 12, 14 | syl2anc 587 | . . . 4 ⊢ (𝜑 → (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇))) = ∪ (𝐽 ↾t (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇))))) |
16 | 11, 15 | sseqtrrd 3936 | . . 3 ⊢ (𝜑 → 𝑂 ⊆ (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇)))) |
17 | 2, 3, 4, 16 | iscnrm3rlem6 45691 | . 2 ⊢ (𝜑 → (𝑂 ∈ (𝐽 ↾t (∪ 𝐽 ∖ (((cls‘𝐽)‘𝑆) ∩ ((cls‘𝐽)‘𝑇)))) ↔ 𝑂 ∈ 𝐽)) |
18 | 1, 17 | mpbid 235 | 1 ⊢ (𝜑 → 𝑂 ∈ 𝐽) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1539 ∈ wcel 2112 Vcvv 3410 ∖ cdif 3858 ∩ cin 3860 ⊆ wss 3861 ∪ cuni 4802 ‘cfv 6341 (class class class)co 7157 ↾t crest 16767 Topctop 21608 clsccl 21733 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1912 ax-6 1971 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2159 ax-12 2176 ax-ext 2730 ax-rep 5161 ax-sep 5174 ax-nul 5181 ax-pow 5239 ax-pr 5303 ax-un 7466 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2071 df-mo 2558 df-eu 2589 df-clab 2737 df-cleq 2751 df-clel 2831 df-nfc 2902 df-ne 2953 df-ral 3076 df-rex 3077 df-reu 3078 df-rab 3080 df-v 3412 df-sbc 3700 df-csb 3809 df-dif 3864 df-un 3866 df-in 3868 df-ss 3878 df-pss 3880 df-nul 4229 df-if 4425 df-pw 4500 df-sn 4527 df-pr 4529 df-tp 4531 df-op 4533 df-uni 4803 df-int 4843 df-iun 4889 df-iin 4890 df-br 5038 df-opab 5100 df-mpt 5118 df-tr 5144 df-id 5435 df-eprel 5440 df-po 5448 df-so 5449 df-fr 5488 df-we 5490 df-xp 5535 df-rel 5536 df-cnv 5537 df-co 5538 df-dm 5539 df-rn 5540 df-res 5541 df-ima 5542 df-ord 6178 df-on 6179 df-lim 6180 df-suc 6181 df-iota 6300 df-fun 6343 df-fn 6344 df-f 6345 df-f1 6346 df-fo 6347 df-f1o 6348 df-fv 6349 df-ov 7160 df-oprab 7161 df-mpo 7162 df-om 7587 df-1st 7700 df-2nd 7701 df-en 8542 df-fin 8545 df-fi 8922 df-rest 16769 df-topgen 16790 df-top 21609 df-topon 21626 df-bases 21661 df-cld 21734 df-cls 21736 |
This theorem is referenced by: iscnrm3rlem8 45693 |
Copyright terms: Public domain | W3C validator |