Step | Hyp | Ref
| Expression |
1 | | simp1 1061 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → 𝐽 ∈ Top) |
2 | | sstr 3611 |
. . . . . . . 8
⊢ ((𝑆 ⊆ 𝑌 ∧ 𝑌 ⊆ 𝑋) → 𝑆 ⊆ 𝑋) |
3 | 2 | ancoms 469 |
. . . . . . 7
⊢ ((𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → 𝑆 ⊆ 𝑋) |
4 | 3 | 3adant1 1079 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → 𝑆 ⊆ 𝑋) |
5 | | restcls.1 |
. . . . . . 7
⊢ 𝑋 = ∪
𝐽 |
6 | 5 | clscld 20851 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ∈ (Clsd‘𝐽)) |
7 | 1, 4, 6 | syl2anc 693 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → ((cls‘𝐽)‘𝑆) ∈ (Clsd‘𝐽)) |
8 | | eqid 2622 |
. . . . 5
⊢
(((cls‘𝐽)‘𝑆) ∩ 𝑌) = (((cls‘𝐽)‘𝑆) ∩ 𝑌) |
9 | | ineq1 3807 |
. . . . . . 7
⊢ (𝑥 = ((cls‘𝐽)‘𝑆) → (𝑥 ∩ 𝑌) = (((cls‘𝐽)‘𝑆) ∩ 𝑌)) |
10 | 9 | eqeq2d 2632 |
. . . . . 6
⊢ (𝑥 = ((cls‘𝐽)‘𝑆) → ((((cls‘𝐽)‘𝑆) ∩ 𝑌) = (𝑥 ∩ 𝑌) ↔ (((cls‘𝐽)‘𝑆) ∩ 𝑌) = (((cls‘𝐽)‘𝑆) ∩ 𝑌))) |
11 | 10 | rspcev 3309 |
. . . . 5
⊢
((((cls‘𝐽)‘𝑆) ∈ (Clsd‘𝐽) ∧ (((cls‘𝐽)‘𝑆) ∩ 𝑌) = (((cls‘𝐽)‘𝑆) ∩ 𝑌)) → ∃𝑥 ∈ (Clsd‘𝐽)(((cls‘𝐽)‘𝑆) ∩ 𝑌) = (𝑥 ∩ 𝑌)) |
12 | 7, 8, 11 | sylancl 694 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → ∃𝑥 ∈ (Clsd‘𝐽)(((cls‘𝐽)‘𝑆) ∩ 𝑌) = (𝑥 ∩ 𝑌)) |
13 | | restcls.2 |
. . . . . . 7
⊢ 𝐾 = (𝐽 ↾t 𝑌) |
14 | 13 | fveq2i 6194 |
. . . . . 6
⊢
(Clsd‘𝐾) =
(Clsd‘(𝐽
↾t 𝑌)) |
15 | 14 | eleq2i 2693 |
. . . . 5
⊢
((((cls‘𝐽)‘𝑆) ∩ 𝑌) ∈ (Clsd‘𝐾) ↔ (((cls‘𝐽)‘𝑆) ∩ 𝑌) ∈ (Clsd‘(𝐽 ↾t 𝑌))) |
16 | 5 | restcld 20976 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋) → ((((cls‘𝐽)‘𝑆) ∩ 𝑌) ∈ (Clsd‘(𝐽 ↾t 𝑌)) ↔ ∃𝑥 ∈ (Clsd‘𝐽)(((cls‘𝐽)‘𝑆) ∩ 𝑌) = (𝑥 ∩ 𝑌))) |
17 | 16 | 3adant3 1081 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → ((((cls‘𝐽)‘𝑆) ∩ 𝑌) ∈ (Clsd‘(𝐽 ↾t 𝑌)) ↔ ∃𝑥 ∈ (Clsd‘𝐽)(((cls‘𝐽)‘𝑆) ∩ 𝑌) = (𝑥 ∩ 𝑌))) |
18 | 15, 17 | syl5bb 272 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → ((((cls‘𝐽)‘𝑆) ∩ 𝑌) ∈ (Clsd‘𝐾) ↔ ∃𝑥 ∈ (Clsd‘𝐽)(((cls‘𝐽)‘𝑆) ∩ 𝑌) = (𝑥 ∩ 𝑌))) |
19 | 12, 18 | mpbird 247 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → (((cls‘𝐽)‘𝑆) ∩ 𝑌) ∈ (Clsd‘𝐾)) |
20 | 5 | sscls 20860 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ ((cls‘𝐽)‘𝑆)) |
21 | 1, 4, 20 | syl2anc 693 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → 𝑆 ⊆ ((cls‘𝐽)‘𝑆)) |
22 | | simp3 1063 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → 𝑆 ⊆ 𝑌) |
23 | 21, 22 | ssind 3837 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → 𝑆 ⊆ (((cls‘𝐽)‘𝑆) ∩ 𝑌)) |
24 | | eqid 2622 |
. . . 4
⊢ ∪ 𝐾 =
∪ 𝐾 |
25 | 24 | clsss2 20876 |
. . 3
⊢
(((((cls‘𝐽)‘𝑆) ∩ 𝑌) ∈ (Clsd‘𝐾) ∧ 𝑆 ⊆ (((cls‘𝐽)‘𝑆) ∩ 𝑌)) → ((cls‘𝐾)‘𝑆) ⊆ (((cls‘𝐽)‘𝑆) ∩ 𝑌)) |
26 | 19, 23, 25 | syl2anc 693 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → ((cls‘𝐾)‘𝑆) ⊆ (((cls‘𝐽)‘𝑆) ∩ 𝑌)) |
27 | 13 | fveq2i 6194 |
. . . . . 6
⊢
(cls‘𝐾) =
(cls‘(𝐽
↾t 𝑌)) |
28 | 27 | fveq1i 6192 |
. . . . 5
⊢
((cls‘𝐾)‘𝑆) = ((cls‘(𝐽 ↾t 𝑌))‘𝑆) |
29 | | id 22 |
. . . . . . . . 9
⊢ (𝑌 ⊆ 𝑋 → 𝑌 ⊆ 𝑋) |
30 | 5 | topopn 20711 |
. . . . . . . . 9
⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽) |
31 | | ssexg 4804 |
. . . . . . . . 9
⊢ ((𝑌 ⊆ 𝑋 ∧ 𝑋 ∈ 𝐽) → 𝑌 ∈ V) |
32 | 29, 30, 31 | syl2anr 495 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋) → 𝑌 ∈ V) |
33 | | resttop 20964 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑌 ∈ V) → (𝐽 ↾t 𝑌) ∈ Top) |
34 | 32, 33 | syldan 487 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋) → (𝐽 ↾t 𝑌) ∈ Top) |
35 | 34 | 3adant3 1081 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → (𝐽 ↾t 𝑌) ∈ Top) |
36 | 5 | restuni 20966 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋) → 𝑌 = ∪ (𝐽 ↾t 𝑌)) |
37 | 36 | 3adant3 1081 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → 𝑌 = ∪ (𝐽 ↾t 𝑌)) |
38 | 22, 37 | sseqtrd 3641 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → 𝑆 ⊆ ∪ (𝐽 ↾t 𝑌)) |
39 | | eqid 2622 |
. . . . . . 7
⊢ ∪ (𝐽
↾t 𝑌) =
∪ (𝐽 ↾t 𝑌) |
40 | 39 | clscld 20851 |
. . . . . 6
⊢ (((𝐽 ↾t 𝑌) ∈ Top ∧ 𝑆 ⊆ ∪ (𝐽
↾t 𝑌))
→ ((cls‘(𝐽
↾t 𝑌))‘𝑆) ∈ (Clsd‘(𝐽 ↾t 𝑌))) |
41 | 35, 38, 40 | syl2anc 693 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → ((cls‘(𝐽 ↾t 𝑌))‘𝑆) ∈ (Clsd‘(𝐽 ↾t 𝑌))) |
42 | 28, 41 | syl5eqel 2705 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → ((cls‘𝐾)‘𝑆) ∈ (Clsd‘(𝐽 ↾t 𝑌))) |
43 | 5 | restcld 20976 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋) → (((cls‘𝐾)‘𝑆) ∈ (Clsd‘(𝐽 ↾t 𝑌)) ↔ ∃𝑥 ∈ (Clsd‘𝐽)((cls‘𝐾)‘𝑆) = (𝑥 ∩ 𝑌))) |
44 | 43 | 3adant3 1081 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → (((cls‘𝐾)‘𝑆) ∈ (Clsd‘(𝐽 ↾t 𝑌)) ↔ ∃𝑥 ∈ (Clsd‘𝐽)((cls‘𝐾)‘𝑆) = (𝑥 ∩ 𝑌))) |
45 | 42, 44 | mpbid 222 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → ∃𝑥 ∈ (Clsd‘𝐽)((cls‘𝐾)‘𝑆) = (𝑥 ∩ 𝑌)) |
46 | 13, 34 | syl5eqel 2705 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋) → 𝐾 ∈ Top) |
47 | 46 | 3adant3 1081 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → 𝐾 ∈ Top) |
48 | 13 | unieqi 4445 |
. . . . . . . . 9
⊢ ∪ 𝐾 =
∪ (𝐽 ↾t 𝑌) |
49 | 48 | eqcomi 2631 |
. . . . . . . 8
⊢ ∪ (𝐽
↾t 𝑌) =
∪ 𝐾 |
50 | 49 | sscls 20860 |
. . . . . . 7
⊢ ((𝐾 ∈ Top ∧ 𝑆 ⊆ ∪ (𝐽
↾t 𝑌))
→ 𝑆 ⊆
((cls‘𝐾)‘𝑆)) |
51 | 47, 38, 50 | syl2anc 693 |
. . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → 𝑆 ⊆ ((cls‘𝐾)‘𝑆)) |
52 | 51 | adantr 481 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ (𝑥 ∈ (Clsd‘𝐽) ∧ ((cls‘𝐾)‘𝑆) = (𝑥 ∩ 𝑌))) → 𝑆 ⊆ ((cls‘𝐾)‘𝑆)) |
53 | | inss1 3833 |
. . . . . . 7
⊢ (𝑥 ∩ 𝑌) ⊆ 𝑥 |
54 | | sseq1 3626 |
. . . . . . 7
⊢
(((cls‘𝐾)‘𝑆) = (𝑥 ∩ 𝑌) → (((cls‘𝐾)‘𝑆) ⊆ 𝑥 ↔ (𝑥 ∩ 𝑌) ⊆ 𝑥)) |
55 | 53, 54 | mpbiri 248 |
. . . . . 6
⊢
(((cls‘𝐾)‘𝑆) = (𝑥 ∩ 𝑌) → ((cls‘𝐾)‘𝑆) ⊆ 𝑥) |
56 | 55 | ad2antll 765 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ (𝑥 ∈ (Clsd‘𝐽) ∧ ((cls‘𝐾)‘𝑆) = (𝑥 ∩ 𝑌))) → ((cls‘𝐾)‘𝑆) ⊆ 𝑥) |
57 | 52, 56 | sstrd 3613 |
. . . 4
⊢ (((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ (𝑥 ∈ (Clsd‘𝐽) ∧ ((cls‘𝐾)‘𝑆) = (𝑥 ∩ 𝑌))) → 𝑆 ⊆ 𝑥) |
58 | 5 | clsss2 20876 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (Clsd‘𝐽) ∧ 𝑆 ⊆ 𝑥) → ((cls‘𝐽)‘𝑆) ⊆ 𝑥) |
59 | 58 | adantl 482 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ (𝑥 ∈ (Clsd‘𝐽) ∧ 𝑆 ⊆ 𝑥)) → ((cls‘𝐽)‘𝑆) ⊆ 𝑥) |
60 | | ssrin 3838 |
. . . . . . . . 9
⊢
(((cls‘𝐽)‘𝑆) ⊆ 𝑥 → (((cls‘𝐽)‘𝑆) ∩ 𝑌) ⊆ (𝑥 ∩ 𝑌)) |
61 | 59, 60 | syl 17 |
. . . . . . . 8
⊢ (((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ (𝑥 ∈ (Clsd‘𝐽) ∧ 𝑆 ⊆ 𝑥)) → (((cls‘𝐽)‘𝑆) ∩ 𝑌) ⊆ (𝑥 ∩ 𝑌)) |
62 | | sseq2 3627 |
. . . . . . . 8
⊢
(((cls‘𝐾)‘𝑆) = (𝑥 ∩ 𝑌) → ((((cls‘𝐽)‘𝑆) ∩ 𝑌) ⊆ ((cls‘𝐾)‘𝑆) ↔ (((cls‘𝐽)‘𝑆) ∩ 𝑌) ⊆ (𝑥 ∩ 𝑌))) |
63 | 61, 62 | syl5ibrcom 237 |
. . . . . . 7
⊢ (((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ (𝑥 ∈ (Clsd‘𝐽) ∧ 𝑆 ⊆ 𝑥)) → (((cls‘𝐾)‘𝑆) = (𝑥 ∩ 𝑌) → (((cls‘𝐽)‘𝑆) ∩ 𝑌) ⊆ ((cls‘𝐾)‘𝑆))) |
64 | 63 | expr 643 |
. . . . . 6
⊢ (((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ 𝑥 ∈ (Clsd‘𝐽)) → (𝑆 ⊆ 𝑥 → (((cls‘𝐾)‘𝑆) = (𝑥 ∩ 𝑌) → (((cls‘𝐽)‘𝑆) ∩ 𝑌) ⊆ ((cls‘𝐾)‘𝑆)))) |
65 | 64 | com23 86 |
. . . . 5
⊢ (((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ 𝑥 ∈ (Clsd‘𝐽)) → (((cls‘𝐾)‘𝑆) = (𝑥 ∩ 𝑌) → (𝑆 ⊆ 𝑥 → (((cls‘𝐽)‘𝑆) ∩ 𝑌) ⊆ ((cls‘𝐾)‘𝑆)))) |
66 | 65 | impr 649 |
. . . 4
⊢ (((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ (𝑥 ∈ (Clsd‘𝐽) ∧ ((cls‘𝐾)‘𝑆) = (𝑥 ∩ 𝑌))) → (𝑆 ⊆ 𝑥 → (((cls‘𝐽)‘𝑆) ∩ 𝑌) ⊆ ((cls‘𝐾)‘𝑆))) |
67 | 57, 66 | mpd 15 |
. . 3
⊢ (((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) ∧ (𝑥 ∈ (Clsd‘𝐽) ∧ ((cls‘𝐾)‘𝑆) = (𝑥 ∩ 𝑌))) → (((cls‘𝐽)‘𝑆) ∩ 𝑌) ⊆ ((cls‘𝐾)‘𝑆)) |
68 | 45, 67 | rexlimddv 3035 |
. 2
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → (((cls‘𝐽)‘𝑆) ∩ 𝑌) ⊆ ((cls‘𝐾)‘𝑆)) |
69 | 26, 68 | eqssd 3620 |
1
⊢ ((𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌) → ((cls‘𝐾)‘𝑆) = (((cls‘𝐽)‘𝑆) ∩ 𝑌)) |