Step | Hyp | Ref
| Expression |
1 | | topontop 13145 |
. . . 4
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top) |
2 | 1 | adantr 276 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐽 ∈ Top) |
3 | | id 19 |
. . . 4
⊢ (𝐴 ⊆ 𝑋 → 𝐴 ⊆ 𝑋) |
4 | | toponmax 13156 |
. . . 4
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐽) |
5 | | ssexg 4139 |
. . . 4
⊢ ((𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝐽) → 𝐴 ∈ V) |
6 | 3, 4, 5 | syl2anr 290 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ∈ V) |
7 | | resttop 13303 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ V) → (𝐽 ↾t 𝐴) ∈ Top) |
8 | 2, 6, 7 | syl2anc 411 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) ∈ Top) |
9 | | simpr 110 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ⊆ 𝑋) |
10 | | sseqin2 3354 |
. . . . . 6
⊢ (𝐴 ⊆ 𝑋 ↔ (𝑋 ∩ 𝐴) = 𝐴) |
11 | 9, 10 | sylib 122 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑋 ∩ 𝐴) = 𝐴) |
12 | | simpl 109 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐽 ∈ (TopOn‘𝑋)) |
13 | 4 | adantr 276 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝑋 ∈ 𝐽) |
14 | | elrestr 12631 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ V ∧ 𝑋 ∈ 𝐽) → (𝑋 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)) |
15 | 12, 6, 13, 14 | syl3anc 1238 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑋 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)) |
16 | 11, 15 | eqeltrrd 2255 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ∈ (𝐽 ↾t 𝐴)) |
17 | | elssuni 3835 |
. . . 4
⊢ (𝐴 ∈ (𝐽 ↾t 𝐴) → 𝐴 ⊆ ∪ (𝐽 ↾t 𝐴)) |
18 | 16, 17 | syl 14 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ⊆ ∪ (𝐽 ↾t 𝐴)) |
19 | | restval 12629 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ V) → (𝐽 ↾t 𝐴) = ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐴))) |
20 | 6, 19 | syldan 282 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) = ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐴))) |
21 | | inss2 3356 |
. . . . . . . . 9
⊢ (𝑥 ∩ 𝐴) ⊆ 𝐴 |
22 | | vex 2740 |
. . . . . . . . . . 11
⊢ 𝑥 ∈ V |
23 | 22 | inex1 4134 |
. . . . . . . . . 10
⊢ (𝑥 ∩ 𝐴) ∈ V |
24 | 23 | elpw 3580 |
. . . . . . . . 9
⊢ ((𝑥 ∩ 𝐴) ∈ 𝒫 𝐴 ↔ (𝑥 ∩ 𝐴) ⊆ 𝐴) |
25 | 21, 24 | mpbir 146 |
. . . . . . . 8
⊢ (𝑥 ∩ 𝐴) ∈ 𝒫 𝐴 |
26 | 25 | a1i 9 |
. . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑥 ∈ 𝐽) → (𝑥 ∩ 𝐴) ∈ 𝒫 𝐴) |
27 | 26 | fmpttd 5666 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐴)):𝐽⟶𝒫 𝐴) |
28 | 27 | frnd 5370 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐴)) ⊆ 𝒫 𝐴) |
29 | 20, 28 | eqsstrd 3191 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) ⊆ 𝒫 𝐴) |
30 | | sspwuni 3968 |
. . . 4
⊢ ((𝐽 ↾t 𝐴) ⊆ 𝒫 𝐴 ↔ ∪ (𝐽
↾t 𝐴)
⊆ 𝐴) |
31 | 29, 30 | sylib 122 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ∪ (𝐽 ↾t 𝐴) ⊆ 𝐴) |
32 | 18, 31 | eqssd 3172 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 = ∪ (𝐽 ↾t 𝐴)) |
33 | | istopon 13144 |
. 2
⊢ ((𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴) ↔ ((𝐽 ↾t 𝐴) ∈ Top ∧ 𝐴 = ∪ (𝐽 ↾t 𝐴))) |
34 | 8, 32, 33 | sylanbrc 417 |
1
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴)) |