Step | Hyp | Ref
| Expression |
1 | | simpl3 1066 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ 𝑋) → 𝐵 ⊆ 𝐴) |
2 | | ptrescn.2 |
. . . . . . . . . 10
⊢ 𝐽 =
(∏t‘𝐹) |
3 | 2 | ptuni 21397 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → X𝑘 ∈
𝐴 ∪ (𝐹‘𝑘) = ∪ 𝐽) |
4 | 3 | 3adant3 1081 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) = ∪ 𝐽) |
5 | | ptrescn.1 |
. . . . . . . 8
⊢ 𝑋 = ∪
𝐽 |
6 | 4, 5 | syl6eqr 2674 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) = 𝑋) |
7 | 6 | eleq2d 2687 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → (𝑥 ∈ X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) ↔ 𝑥 ∈ 𝑋)) |
8 | 7 | biimpar 502 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘)) |
9 | | resixp 7943 |
. . . . 5
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝑥 ∈ X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘)) → (𝑥 ↾ 𝐵) ∈ X𝑘 ∈ 𝐵 ∪ (𝐹‘𝑘)) |
10 | 1, 8, 9 | syl2anc 693 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ 𝑋) → (𝑥 ↾ 𝐵) ∈ X𝑘 ∈ 𝐵 ∪ (𝐹‘𝑘)) |
11 | | ixpeq2 7922 |
. . . . . . 7
⊢
(∀𝑘 ∈
𝐵 ∪ ((𝐹
↾ 𝐵)‘𝑘) = ∪
(𝐹‘𝑘) → X𝑘 ∈ 𝐵 ∪ ((𝐹 ↾ 𝐵)‘𝑘) = X𝑘 ∈ 𝐵 ∪ (𝐹‘𝑘)) |
12 | | fvres 6207 |
. . . . . . . 8
⊢ (𝑘 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝑘) = (𝐹‘𝑘)) |
13 | 12 | unieqd 4446 |
. . . . . . 7
⊢ (𝑘 ∈ 𝐵 → ∪ ((𝐹 ↾ 𝐵)‘𝑘) = ∪ (𝐹‘𝑘)) |
14 | 11, 13 | mprg 2926 |
. . . . . 6
⊢ X𝑘 ∈
𝐵 ∪ ((𝐹
↾ 𝐵)‘𝑘) = X𝑘 ∈
𝐵 ∪ (𝐹‘𝑘) |
15 | | ssexg 4804 |
. . . . . . . . 9
⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐵 ∈ V) |
16 | 15 | ancoms 469 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ V) |
17 | 16 | 3adant2 1080 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ V) |
18 | | fssres 6070 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → (𝐹 ↾ 𝐵):𝐵⟶Top) |
19 | 18 | 3adant1 1079 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → (𝐹 ↾ 𝐵):𝐵⟶Top) |
20 | | ptrescn.3 |
. . . . . . . 8
⊢ 𝐾 =
(∏t‘(𝐹 ↾ 𝐵)) |
21 | 20 | ptuni 21397 |
. . . . . . 7
⊢ ((𝐵 ∈ V ∧ (𝐹 ↾ 𝐵):𝐵⟶Top) → X𝑘 ∈
𝐵 ∪ ((𝐹
↾ 𝐵)‘𝑘) = ∪
𝐾) |
22 | 17, 19, 21 | syl2anc 693 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → X𝑘 ∈ 𝐵 ∪ ((𝐹 ↾ 𝐵)‘𝑘) = ∪ 𝐾) |
23 | 14, 22 | syl5eqr 2670 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → X𝑘 ∈ 𝐵 ∪ (𝐹‘𝑘) = ∪ 𝐾) |
24 | 23 | adantr 481 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ 𝑋) → X𝑘 ∈ 𝐵 ∪ (𝐹‘𝑘) = ∪ 𝐾) |
25 | 10, 24 | eleqtrd 2703 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ 𝑋) → (𝑥 ↾ 𝐵) ∈ ∪ 𝐾) |
26 | | eqid 2622 |
. . 3
⊢ (𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) = (𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) |
27 | 25, 26 | fmptd 6385 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → (𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)):𝑋⟶∪ 𝐾) |
28 | | fimacnv 6347 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)):𝑋⟶∪ 𝐾 → (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ ∪
𝐾) = 𝑋) |
29 | 27, 28 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ ∪
𝐾) = 𝑋) |
30 | | pttop 21385 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) →
(∏t‘𝐹) ∈ Top) |
31 | 2, 30 | syl5eqel 2705 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝐽 ∈ Top) |
32 | 31 | 3adant3 1081 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → 𝐽 ∈ Top) |
33 | 5 | topopn 20711 |
. . . . . . 7
⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽) |
34 | 32, 33 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → 𝑋 ∈ 𝐽) |
35 | 29, 34 | eqeltrd 2701 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ ∪
𝐾) ∈ 𝐽) |
36 | | elsni 4194 |
. . . . . . 7
⊢ (𝑣 ∈ {∪ 𝐾}
→ 𝑣 = ∪ 𝐾) |
37 | 36 | imaeq2d 5466 |
. . . . . 6
⊢ (𝑣 ∈ {∪ 𝐾}
→ (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) = (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ ∪
𝐾)) |
38 | 37 | eleq1d 2686 |
. . . . 5
⊢ (𝑣 ∈ {∪ 𝐾}
→ ((◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽 ↔ (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ ∪
𝐾) ∈ 𝐽)) |
39 | 35, 38 | syl5ibrcom 237 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → (𝑣 ∈ {∪ 𝐾} → (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽)) |
40 | 39 | ralrimiv 2965 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → ∀𝑣 ∈ {∪ 𝐾} (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽) |
41 | | imaco 5640 |
. . . . . . . . 9
⊢ ((◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) ∘ ◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘))) “ 𝑢) = (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)) |
42 | | cnvco 5308 |
. . . . . . . . . . 11
⊢ ◡((𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) ∘ (𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵))) = (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) ∘ ◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘))) |
43 | 25 | adantlr 751 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) ∧ 𝑥 ∈ 𝑋) → (𝑥 ↾ 𝐵) ∈ ∪ 𝐾) |
44 | | eqidd 2623 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → (𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) = (𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵))) |
45 | | eqidd 2623 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → (𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) = (𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘))) |
46 | | fveq1 6190 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝑥 ↾ 𝐵) → (𝑧‘𝑘) = ((𝑥 ↾ 𝐵)‘𝑘)) |
47 | 43, 44, 45, 46 | fmptco 6396 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → ((𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) ∘ (𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵))) = (𝑥 ∈ 𝑋 ↦ ((𝑥 ↾ 𝐵)‘𝑘))) |
48 | | fvres 6207 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ 𝐵 → ((𝑥 ↾ 𝐵)‘𝑘) = (𝑥‘𝑘)) |
49 | 48 | ad2antrl 764 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → ((𝑥 ↾ 𝐵)‘𝑘) = (𝑥‘𝑘)) |
50 | 49 | mpteq2dv 4745 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → (𝑥 ∈ 𝑋 ↦ ((𝑥 ↾ 𝐵)‘𝑘)) = (𝑥 ∈ 𝑋 ↦ (𝑥‘𝑘))) |
51 | 47, 50 | eqtrd 2656 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → ((𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) ∘ (𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵))) = (𝑥 ∈ 𝑋 ↦ (𝑥‘𝑘))) |
52 | 51 | cnveqd 5298 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → ◡((𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) ∘ (𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵))) = ◡(𝑥 ∈ 𝑋 ↦ (𝑥‘𝑘))) |
53 | 42, 52 | syl5eqr 2670 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) ∘ ◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘))) = ◡(𝑥 ∈ 𝑋 ↦ (𝑥‘𝑘))) |
54 | 53 | imaeq1d 5465 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → ((◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) ∘ ◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘))) “ 𝑢) = (◡(𝑥 ∈ 𝑋 ↦ (𝑥‘𝑘)) “ 𝑢)) |
55 | 41, 54 | syl5eqr 2670 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)) = (◡(𝑥 ∈ 𝑋 ↦ (𝑥‘𝑘)) “ 𝑢)) |
56 | | simpl1 1064 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → 𝐴 ∈ 𝑉) |
57 | | simpl2 1065 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → 𝐹:𝐴⟶Top) |
58 | | simpl3 1066 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → 𝐵 ⊆ 𝐴) |
59 | | simprl 794 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → 𝑘 ∈ 𝐵) |
60 | 58, 59 | sseldd 3604 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → 𝑘 ∈ 𝐴) |
61 | 5, 2 | ptpjcn 21414 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋 ↦ (𝑥‘𝑘)) ∈ (𝐽 Cn (𝐹‘𝑘))) |
62 | 56, 57, 60, 61 | syl3anc 1326 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → (𝑥 ∈ 𝑋 ↦ (𝑥‘𝑘)) ∈ (𝐽 Cn (𝐹‘𝑘))) |
63 | | simprr 796 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → 𝑢 ∈ (𝐹‘𝑘)) |
64 | | cnima 21069 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝑋 ↦ (𝑥‘𝑘)) ∈ (𝐽 Cn (𝐹‘𝑘)) ∧ 𝑢 ∈ (𝐹‘𝑘)) → (◡(𝑥 ∈ 𝑋 ↦ (𝑥‘𝑘)) “ 𝑢) ∈ 𝐽) |
65 | 62, 63, 64 | syl2anc 693 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → (◡(𝑥 ∈ 𝑋 ↦ (𝑥‘𝑘)) “ 𝑢) ∈ 𝐽) |
66 | 55, 65 | eqeltrd 2701 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)) ∈ 𝐽) |
67 | | imaeq2 5462 |
. . . . . . . 8
⊢ (𝑣 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢) → (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) = (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢))) |
68 | 67 | eleq1d 2686 |
. . . . . . 7
⊢ (𝑣 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢) → ((◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽 ↔ (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)) ∈ 𝐽)) |
69 | 66, 68 | syl5ibrcom 237 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) ∧ (𝑘 ∈ 𝐵 ∧ 𝑢 ∈ (𝐹‘𝑘))) → (𝑣 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢) → (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽)) |
70 | 69 | rexlimdvva 3038 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → (∃𝑘 ∈ 𝐵 ∃𝑢 ∈ (𝐹‘𝑘)𝑣 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢) → (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽)) |
71 | 70 | alrimiv 1855 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → ∀𝑣(∃𝑘 ∈ 𝐵 ∃𝑢 ∈ (𝐹‘𝑘)𝑣 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢) → (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽)) |
72 | | eqid 2622 |
. . . . . . 7
⊢ (𝑘 ∈ 𝐵, 𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘) ↦ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)) = (𝑘 ∈ 𝐵, 𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘) ↦ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)) |
73 | 72 | rnmpt2 6770 |
. . . . . 6
⊢ ran
(𝑘 ∈ 𝐵, 𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘) ↦ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)) = {𝑦 ∣ ∃𝑘 ∈ 𝐵 ∃𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘)𝑦 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)} |
74 | 73 | raleqi 3142 |
. . . . 5
⊢
(∀𝑣 ∈
ran (𝑘 ∈ 𝐵, 𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘) ↦ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢))(◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽 ↔ ∀𝑣 ∈ {𝑦 ∣ ∃𝑘 ∈ 𝐵 ∃𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘)𝑦 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)} (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽) |
75 | 12 | rexeqdv 3145 |
. . . . . . . 8
⊢ (𝑘 ∈ 𝐵 → (∃𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘)𝑦 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢) ↔ ∃𝑢 ∈ (𝐹‘𝑘)𝑦 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢))) |
76 | | eqeq1 2626 |
. . . . . . . . 9
⊢ (𝑦 = 𝑣 → (𝑦 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢) ↔ 𝑣 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢))) |
77 | 76 | rexbidv 3052 |
. . . . . . . 8
⊢ (𝑦 = 𝑣 → (∃𝑢 ∈ (𝐹‘𝑘)𝑦 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢) ↔ ∃𝑢 ∈ (𝐹‘𝑘)𝑣 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢))) |
78 | 75, 77 | sylan9bbr 737 |
. . . . . . 7
⊢ ((𝑦 = 𝑣 ∧ 𝑘 ∈ 𝐵) → (∃𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘)𝑦 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢) ↔ ∃𝑢 ∈ (𝐹‘𝑘)𝑣 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢))) |
79 | 78 | rexbidva 3049 |
. . . . . 6
⊢ (𝑦 = 𝑣 → (∃𝑘 ∈ 𝐵 ∃𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘)𝑦 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢) ↔ ∃𝑘 ∈ 𝐵 ∃𝑢 ∈ (𝐹‘𝑘)𝑣 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢))) |
80 | 79 | ralab 3367 |
. . . . 5
⊢
(∀𝑣 ∈
{𝑦 ∣ ∃𝑘 ∈ 𝐵 ∃𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘)𝑦 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)} (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽 ↔ ∀𝑣(∃𝑘 ∈ 𝐵 ∃𝑢 ∈ (𝐹‘𝑘)𝑣 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢) → (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽)) |
81 | 74, 80 | bitri 264 |
. . . 4
⊢
(∀𝑣 ∈
ran (𝑘 ∈ 𝐵, 𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘) ↦ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢))(◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽 ↔ ∀𝑣(∃𝑘 ∈ 𝐵 ∃𝑢 ∈ (𝐹‘𝑘)𝑣 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢) → (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽)) |
82 | 71, 81 | sylibr 224 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → ∀𝑣 ∈ ran (𝑘 ∈ 𝐵, 𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘) ↦ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢))(◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽) |
83 | | ralunb 3794 |
. . 3
⊢
(∀𝑣 ∈
({∪ 𝐾} ∪ ran (𝑘 ∈ 𝐵, 𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘) ↦ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)))(◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽 ↔ (∀𝑣 ∈ {∪ 𝐾} (◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽 ∧ ∀𝑣 ∈ ran (𝑘 ∈ 𝐵, 𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘) ↦ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢))(◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽)) |
84 | 40, 82, 83 | sylanbrc 698 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → ∀𝑣 ∈ ({∪ 𝐾} ∪ ran (𝑘 ∈ 𝐵, 𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘) ↦ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)))(◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽) |
85 | 5 | toptopon 20722 |
. . . 4
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) |
86 | 32, 85 | sylib 208 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → 𝐽 ∈ (TopOn‘𝑋)) |
87 | | snex 4908 |
. . . 4
⊢ {∪ 𝐾}
∈ V |
88 | | fvex 6201 |
. . . . . . . 8
⊢ ((𝐹 ↾ 𝐵)‘𝑘) ∈ V |
89 | 88 | abrexex 7141 |
. . . . . . 7
⊢ {𝑦 ∣ ∃𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘)𝑦 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)} ∈ V |
90 | 89 | rgenw 2924 |
. . . . . 6
⊢
∀𝑘 ∈
𝐵 {𝑦 ∣ ∃𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘)𝑦 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)} ∈ V |
91 | | abrexex2g 7144 |
. . . . . 6
⊢ ((𝐵 ∈ V ∧ ∀𝑘 ∈ 𝐵 {𝑦 ∣ ∃𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘)𝑦 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)} ∈ V) → {𝑦 ∣ ∃𝑘 ∈ 𝐵 ∃𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘)𝑦 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)} ∈ V) |
92 | 17, 90, 91 | sylancl 694 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → {𝑦 ∣ ∃𝑘 ∈ 𝐵 ∃𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘)𝑦 = (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)} ∈ V) |
93 | 73, 92 | syl5eqel 2705 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → ran (𝑘 ∈ 𝐵, 𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘) ↦ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)) ∈ V) |
94 | | unexg 6959 |
. . . 4
⊢ (({∪ 𝐾}
∈ V ∧ ran (𝑘
∈ 𝐵, 𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘) ↦ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)) ∈ V) → ({∪ 𝐾}
∪ ran (𝑘 ∈ 𝐵, 𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘) ↦ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢))) ∈ V) |
95 | 87, 93, 94 | sylancr 695 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → ({∪
𝐾} ∪ ran (𝑘 ∈ 𝐵, 𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘) ↦ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢))) ∈ V) |
96 | | eqid 2622 |
. . . . 5
⊢ ∪ 𝐾 =
∪ 𝐾 |
97 | 20, 96, 72 | ptval2 21404 |
. . . 4
⊢ ((𝐵 ∈ V ∧ (𝐹 ↾ 𝐵):𝐵⟶Top) → 𝐾 = (topGen‘(fi‘({∪ 𝐾}
∪ ran (𝑘 ∈ 𝐵, 𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘) ↦ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)))))) |
98 | 17, 19, 97 | syl2anc 693 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → 𝐾 = (topGen‘(fi‘({∪ 𝐾}
∪ ran (𝑘 ∈ 𝐵, 𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘) ↦ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)))))) |
99 | | pttop 21385 |
. . . . . 6
⊢ ((𝐵 ∈ V ∧ (𝐹 ↾ 𝐵):𝐵⟶Top) →
(∏t‘(𝐹 ↾ 𝐵)) ∈ Top) |
100 | 17, 19, 99 | syl2anc 693 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → (∏t‘(𝐹 ↾ 𝐵)) ∈ Top) |
101 | 20, 100 | syl5eqel 2705 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → 𝐾 ∈ Top) |
102 | 96 | toptopon 20722 |
. . . 4
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾)) |
103 | 101, 102 | sylib 208 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
104 | 86, 95, 98, 103 | subbascn 21058 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → ((𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) ∈ (𝐽 Cn 𝐾) ↔ ((𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)):𝑋⟶∪ 𝐾 ∧ ∀𝑣 ∈ ({∪ 𝐾}
∪ ran (𝑘 ∈ 𝐵, 𝑢 ∈ ((𝐹 ↾ 𝐵)‘𝑘) ↦ (◡(𝑧 ∈ ∪ 𝐾 ↦ (𝑧‘𝑘)) “ 𝑢)))(◡(𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) “ 𝑣) ∈ 𝐽))) |
105 | 27, 84, 104 | mpbir2and 957 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top ∧ 𝐵 ⊆ 𝐴) → (𝑥 ∈ 𝑋 ↦ (𝑥 ↾ 𝐵)) ∈ (𝐽 Cn 𝐾)) |