Step | Hyp | Ref
| Expression |
1 | | simpl3 1189 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ 𝑋) → 𝐵 ⊆ 𝐴) |
2 | | ptrescn.2 |
. . . . . . . . . 10
⊢ 𝐽 =
(∏t‘𝐹) |
3 | 2 | ptuni 22205 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → X𝑘 ∈
𝐴 ∪ (𝐹‘𝑘) = ∪ 𝐽) |
4 | 3 | 3adant3 1128 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) = ∪ 𝐽) |
5 | | ptrescn.1 |
. . . . . . . 8
⊢ 𝑋 = ∪
𝐽 |
6 | 4, 5 | syl6eqr 2877 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) = 𝑋) |
7 | 6 | eleq2d 2901 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → (𝑥 ∈ X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) ↔ 𝑥 ∈ 𝑋)) |
8 | 7 | biimpar 480 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘)) |
9 | | resixp 8500 |
. . . . 5
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑥 ∈ X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘)) → (𝑥 ↾ 𝐵) ∈ X𝑘 ∈ 𝐵 ∪ (𝐹‘𝑘)) |
10 | 1, 8, 9 | syl2anc 586 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ 𝑋) → (𝑥 ↾ 𝐵) ∈ X𝑘 ∈ 𝐵 ∪ (𝐹‘𝑘)) |
11 | | ixpeq2 8478 |
. . . . . . 7
⊢
(∀𝑘 ∈
𝐵 ∪ ((𝐹
↾ 𝐵)‘𝑘) = ∪
(𝐹‘𝑘) → X𝑘 ∈ 𝐵 ∪ ((𝐹 ↾ 𝐵)‘𝑘) = X𝑘 ∈ 𝐵 ∪ (𝐹‘𝑘)) |
12 | | fvres 6692 |
. . . . . . . 8
⊢ (𝑘 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝑘) = (𝐹‘𝑘)) |
13 | 12 | unieqd 4855 |
. . . . . . 7
⊢ (𝑘 ∈ 𝐵 → ∪ ((𝐹 ↾ 𝐵)‘𝑘) = ∪ (𝐹‘𝑘)) |
14 | 11, 13 | mprg 3155 |
. . . . . 6
⊢ X𝑘 ∈
𝐵 ∪ ((𝐹
↾ 𝐵)‘𝑘) = X𝑘 ∈
𝐵 ∪ (𝐹‘𝑘) |
15 | | ssexg 5230 |
. . . . . . . . 9
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐵 ∈ V) |
16 | 15 | ancoms 461 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ V) |
17 | 16 | 3adant2 1127 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ V) |
18 | | fssres 6547 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → (𝐹 ↾ 𝐵):𝐵⟶Top) |
19 | 18 | 3adant1 1126 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → (𝐹 ↾ 𝐵):𝐵⟶Top) |
20 | | ptrescn.3 |
. . . . . . . 8
⊢ 𝐾 =
(∏t‘(𝐹 ↾ 𝐵)) |
21 | 20 | ptuni 22205 |
. . . . . . 7
⊢ ((𝐵 ∈ V ∧ (𝐹 ↾ 𝐵):𝐵⟶Top) → X𝑘 ∈
𝐵 ∪ ((𝐹
↾ 𝐵)‘𝑘) = ∪
𝐾) |
22 | 17, 19, 21 | syl2anc 586 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → X𝑘 ∈ 𝐵 ∪ ((𝐹 ↾ 𝐵)‘𝑘) = ∪ 𝐾) |
23 | 14, 22 | syl5eqr 2873 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → X𝑘 ∈ 𝐵 ∪ (𝐹‘𝑘) = ∪ 𝐾) |
24 | 23 | adantr 483 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ 𝑋) → X𝑘 ∈ 𝐵 ∪ (𝐹‘𝑘) = ∪ 𝐾) |
25 | 10, 24 | eleqtrd 2918 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ 𝑋) → (𝑥 ↾ 𝐵) ∈ ∪ 𝐾) |
26 | 25 | fmpttd 6882 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → (𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)):𝑋⟶∪ 𝐾) |
27 | | fimacnv 6842 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)):𝑋⟶∪ 𝐾 → (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ ∪
𝐾) = 𝑋) |
28 | 26, 27 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ ∪
𝐾) = 𝑋) |
29 | | pttop 22193 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) →
(∏t‘𝐹) ∈ Top) |
30 | 2, 29 | eqeltrid 2920 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝐽 ∈ Top) |
31 | 30 | 3adant3 1128 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → 𝐽 ∈ Top) |
32 | 5 | topopn 21517 |
. . . . . . 7
⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽) |
33 | 31, 32 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → 𝑋 ∈ 𝐽) |
34 | 28, 33 | eqeltrd 2916 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ ∪
𝐾) ∈ 𝐽) |
35 | | elsni 4587 |
. . . . . . 7
⊢ (𝑣 ∈ {∪ 𝐾}
→ 𝑣 = ∪ 𝐾) |
36 | 35 | imaeq2d 5932 |
. . . . . 6
⊢ (𝑣 ∈ {∪ 𝐾}
→ (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) = (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ ∪
𝐾)) |
37 | 36 | eleq1d 2900 |
. . . . 5
⊢ (𝑣 ∈ {∪ 𝐾}
→ ((◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽 ↔ (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ ∪
𝐾) ∈ 𝐽)) |
38 | 34, 37 | syl5ibrcom 249 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → (𝑣 ∈ {∪ 𝐾} → (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽)) |
39 | 38 | ralrimiv 3184 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → ∀𝑣 ∈ {∪ 𝐾} (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽) |
40 | | imaco 6107 |
. . . . . . . . 9
⊢ ((◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) ∘ ◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘))) “ 𝑢) = (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)) |
41 | | cnvco 5759 |
. . . . . . . . . . 11
⊢ ◡((𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) ∘ (𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵))) = (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) ∘ ◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘))) |
42 | 25 | adantlr 713 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) ∧ 𝑥 ∈ 𝑋) → (𝑥 ↾ 𝐵) ∈ ∪ 𝐾) |
43 | | eqidd 2825 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → (𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) = (𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵))) |
44 | | eqidd 2825 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → (𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) = (𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘))) |
45 | | fveq1 6672 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝑥 ↾ 𝐵) → (𝑧‘𝑘) = ((𝑥 ↾ 𝐵)‘𝑘)) |
46 | 42, 43, 44, 45 | fmptco 6894 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → ((𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) ∘ (𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵))) = (𝑥 ∈ 𝑋 ↦ ((𝑥 ↾ 𝐵)‘𝑘))) |
47 | | fvres 6692 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ 𝐵 → ((𝑥 ↾ 𝐵)‘𝑘) = (𝑥‘𝑘)) |
48 | 47 | ad2antrl 726 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → ((𝑥 ↾ 𝐵)‘𝑘) = (𝑥‘𝑘)) |
49 | 48 | mpteq2dv 5165 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → (𝑥 ∈ 𝑋 ↦ ((𝑥 ↾ 𝐵)‘𝑘)) = (𝑥 ∈ 𝑋 ↦ (𝑥‘𝑘))) |
50 | 46, 49 | eqtrd 2859 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → ((𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) ∘ (𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵))) = (𝑥 ∈ 𝑋 ↦ (𝑥‘𝑘))) |
51 | 50 | cnveqd 5749 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → ◡((𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) ∘ (𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵))) = ◡(𝑥 ∈ 𝑋 ↦ (𝑥‘𝑘))) |
52 | 41, 51 | syl5eqr 2873 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) ∘ ◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘))) = ◡(𝑥 ∈ 𝑋 ↦ (𝑥‘𝑘))) |
53 | 52 | imaeq1d 5931 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → ((◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) ∘ ◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘))) “ 𝑢) = (◡(𝑥 ∈ 𝑋 ↦ (𝑥‘𝑘)) “ 𝑢)) |
54 | 40, 53 | syl5eqr 2873 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)) = (◡(𝑥 ∈ 𝑋 ↦ (𝑥‘𝑘)) “ 𝑢)) |
55 | | simpl1 1187 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → 𝐴 ∈ 𝑉) |
56 | | simpl2 1188 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → 𝐹:𝐴⟶Top) |
57 | | simpl3 1189 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → 𝐵 ⊆ 𝐴) |
58 | | simprl 769 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → 𝑘 ∈ 𝐵) |
59 | 57, 58 | sseldd 3971 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → 𝑘 ∈ 𝐴) |
60 | 5, 2 | ptpjcn 22222 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋 ↦ (𝑥‘𝑘)) ∈ (𝐽 Cn (𝐹‘𝑘))) |
61 | 55, 56, 59, 60 | syl3anc 1367 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → (𝑥 ∈ 𝑋 ↦ (𝑥‘𝑘)) ∈ (𝐽 Cn (𝐹‘𝑘))) |
62 | | simprr 771 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → 𝑢 ∈ (𝐹‘𝑘)) |
63 | | cnima 21876 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝑋 ↦ (𝑥‘𝑘)) ∈ (𝐽 Cn (𝐹‘𝑘)) ∧ 𝑢 ∈ (𝐹‘𝑘)) → (◡(𝑥 ∈ 𝑋 ↦ (𝑥‘𝑘)) “ 𝑢) ∈ 𝐽) |
64 | 61, 62, 63 | syl2anc 586 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → (◡(𝑥 ∈ 𝑋 ↦ (𝑥‘𝑘)) “ 𝑢) ∈ 𝐽) |
65 | 54, 64 | eqeltrd 2916 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)) ∈ 𝐽) |
66 | | imaeq2 5928 |
. . . . . . . 8
⊢ (𝑣 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢) → (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) = (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢))) |
67 | 66 | eleq1d 2900 |
. . . . . . 7
⊢ (𝑣 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢) → ((◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽 ↔ (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)) ∈ 𝐽)) |
68 | 65, 67 | syl5ibrcom 249 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → (𝑣 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢) → (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽)) |
69 | 68 | rexlimdvva 3297 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → (∃𝑘 ∈ 𝐵 ∃𝑢 ∈ (𝐹‘𝑘)𝑣 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢) → (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽)) |
70 | 69 | alrimiv 1927 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → ∀𝑣(∃𝑘 ∈ 𝐵 ∃𝑢 ∈ (𝐹‘𝑘)𝑣 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢) → (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽)) |
71 | | eqid 2824 |
. . . . . . 7
⊢ (𝑘 ∈ 𝐵, 𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘) ↦ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)) = (𝑘 ∈ 𝐵, 𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘) ↦ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)) |
72 | 71 | rnmpo 7287 |
. . . . . 6
⊢ ran
(𝑘 ∈ 𝐵, 𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘) ↦ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)) = {𝑦 ∣ ∃𝑘 ∈ 𝐵 ∃𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘)𝑦 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)} |
73 | 72 | raleqi 3416 |
. . . . 5
⊢
(∀𝑣 ∈
ran (𝑘 ∈ 𝐵, 𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘) ↦ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢))(◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽 ↔ ∀𝑣 ∈ {𝑦 ∣ ∃𝑘 ∈ 𝐵 ∃𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘)𝑦 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)} (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽) |
74 | 12 | rexeqdv 3419 |
. . . . . . . 8
⊢ (𝑘 ∈ 𝐵 → (∃𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘)𝑦 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢) ↔ ∃𝑢 ∈ (𝐹‘𝑘)𝑦 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢))) |
75 | | eqeq1 2828 |
. . . . . . . . 9
⊢ (𝑦 = 𝑣 → (𝑦 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢) ↔ 𝑣 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢))) |
76 | 75 | rexbidv 3300 |
. . . . . . . 8
⊢ (𝑦 = 𝑣 → (∃𝑢 ∈ (𝐹‘𝑘)𝑦 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢) ↔ ∃𝑢 ∈ (𝐹‘𝑘)𝑣 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢))) |
77 | 74, 76 | sylan9bbr 513 |
. . . . . . 7
⊢ ((𝑦 = 𝑣 ∧ 𝑘 ∈ 𝐵) → (∃𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘)𝑦 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢) ↔ ∃𝑢 ∈ (𝐹‘𝑘)𝑣 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢))) |
78 | 77 | rexbidva 3299 |
. . . . . 6
⊢ (𝑦 = 𝑣 → (∃𝑘 ∈ 𝐵 ∃𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘)𝑦 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢) ↔ ∃𝑘 ∈ 𝐵 ∃𝑢 ∈ (𝐹‘𝑘)𝑣 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢))) |
79 | 78 | ralab 3687 |
. . . . 5
⊢
(∀𝑣 ∈
{𝑦 ∣ ∃𝑘 ∈ 𝐵 ∃𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘)𝑦 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)} (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽 ↔ ∀𝑣(∃𝑘 ∈ 𝐵 ∃𝑢 ∈ (𝐹‘𝑘)𝑣 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢) → (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽)) |
80 | 73, 79 | bitri 277 |
. . . 4
⊢
(∀𝑣 ∈
ran (𝑘 ∈ 𝐵, 𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘) ↦ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢))(◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽 ↔ ∀𝑣(∃𝑘 ∈ 𝐵 ∃𝑢 ∈ (𝐹‘𝑘)𝑣 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢) → (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽)) |
81 | 70, 80 | sylibr 236 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → ∀𝑣 ∈ ran (𝑘 ∈ 𝐵, 𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘) ↦ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢))(◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽) |
82 | | ralunb 4170 |
. . 3
⊢
(∀𝑣 ∈
({∪ 𝐾} ∪ ran (𝑘 ∈ 𝐵, 𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘) ↦ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)))(◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽 ↔ (∀𝑣 ∈ {∪ 𝐾} (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽 ∧ ∀𝑣 ∈ ran (𝑘 ∈ 𝐵, 𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘) ↦ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢))(◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽)) |
83 | 39, 81, 82 | sylanbrc 585 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → ∀𝑣 ∈ ({∪ 𝐾} ∪ ran (𝑘 ∈ 𝐵, 𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘) ↦ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)))(◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽) |
84 | 5 | toptopon 21528 |
. . . 4
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) |
85 | 31, 84 | sylib 220 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → 𝐽 ∈ (TopOn‘𝑋)) |
86 | | snex 5335 |
. . . 4
⊢ {∪ 𝐾}
∈ V |
87 | | fvex 6686 |
. . . . . . . 8
⊢ ((𝐹 ↾ 𝐵)‘𝑘) ∈ V |
88 | 87 | abrexex 7666 |
. . . . . . 7
⊢ {𝑦 ∣ ∃𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘)𝑦 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)} ∈ V |
89 | 88 | rgenw 3153 |
. . . . . 6
⊢
∀𝑘 ∈
𝐵 {𝑦 ∣ ∃𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘)𝑦 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)} ∈ V |
90 | | abrexex2g 7668 |
. . . . . 6
⊢ ((𝐵 ∈ V ∧ ∀𝑘 ∈ 𝐵 {𝑦 ∣ ∃𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘)𝑦 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)} ∈ V) → {𝑦 ∣ ∃𝑘 ∈ 𝐵 ∃𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘)𝑦 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)} ∈ V) |
91 | 17, 89, 90 | sylancl 588 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → {𝑦 ∣ ∃𝑘 ∈ 𝐵 ∃𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘)𝑦 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)} ∈ V) |
92 | 72, 91 | eqeltrid 2920 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → ran (𝑘 ∈ 𝐵, 𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘) ↦ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)) ∈ V) |
93 | | unexg 7475 |
. . . 4
⊢ (({∪ 𝐾}
∈ V ∧ ran (𝑘
∈ 𝐵, 𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘) ↦ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)) ∈ V) → ({∪ 𝐾}
∪ ran (𝑘 ∈ 𝐵, 𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘) ↦ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢))) ∈ V) |
94 | 86, 92, 93 | sylancr 589 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → ({∪
𝐾} ∪ ran (𝑘 ∈ 𝐵, 𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘) ↦ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢))) ∈ V) |
95 | | eqid 2824 |
. . . . 5
⊢ ∪ 𝐾 =
∪ 𝐾 |
96 | 20, 95, 71 | ptval2 22212 |
. . . 4
⊢ ((𝐵 ∈ V ∧ (𝐹 ↾ 𝐵):𝐵⟶Top) → 𝐾 = (topGen‘(fi‘({∪ 𝐾}
∪ ran (𝑘 ∈ 𝐵, 𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘) ↦ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)))))) |
97 | 17, 19, 96 | syl2anc 586 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → 𝐾 = (topGen‘(fi‘({∪ 𝐾}
∪ ran (𝑘 ∈ 𝐵, 𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘) ↦ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)))))) |
98 | | pttop 22193 |
. . . . . 6
⊢ ((𝐵 ∈ V ∧ (𝐹 ↾ 𝐵):𝐵⟶Top) →
(∏t‘(𝐹 ↾ 𝐵)) ∈ Top) |
99 | 17, 19, 98 | syl2anc 586 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → (∏t‘(𝐹 ↾ 𝐵)) ∈ Top) |
100 | 20, 99 | eqeltrid 2920 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → 𝐾 ∈ Top) |
101 | 95 | toptopon 21528 |
. . . 4
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾)) |
102 | 100, 101 | sylib 220 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
103 | 85, 94, 97, 102 | subbascn 21865 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → ((𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) ∈ (𝐽 Cn 𝐾) ↔ ((𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)):𝑋⟶∪ 𝐾 ∧ ∀𝑣 ∈ ({∪ 𝐾}
∪ ran (𝑘 ∈ 𝐵, 𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘) ↦ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)))(◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽))) |
104 | 26, 83, 103 | mpbir2and 711 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → (𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) ∈ (𝐽 Cn 𝐾)) |