Step | Hyp | Ref
| Expression |
1 | | xkoptsub.j |
. . . . 5
⊢ 𝐽 =
(∏t‘(𝑋 × {𝑆})) |
2 | | xkoptsub.x |
. . . . . . . . 9
⊢ 𝑋 = ∪
𝑅 |
3 | 2 | topopn 20711 |
. . . . . . . 8
⊢ (𝑅 ∈ Top → 𝑋 ∈ 𝑅) |
4 | 3 | adantr 481 |
. . . . . . 7
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝑋 ∈ 𝑅) |
5 | | fconstg 6092 |
. . . . . . . . 9
⊢ (𝑆 ∈ Top → (𝑋 × {𝑆}):𝑋⟶{𝑆}) |
6 | 5 | adantl 482 |
. . . . . . . 8
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × {𝑆}):𝑋⟶{𝑆}) |
7 | | ffn 6045 |
. . . . . . . 8
⊢ ((𝑋 × {𝑆}):𝑋⟶{𝑆} → (𝑋 × {𝑆}) Fn 𝑋) |
8 | 6, 7 | syl 17 |
. . . . . . 7
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × {𝑆}) Fn 𝑋) |
9 | | eqid 2622 |
. . . . . . . 8
⊢ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝑔‘𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝑋 (𝑔‘𝑦))} = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝑔‘𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝑋 (𝑔‘𝑦))} |
10 | 9 | ptval 21373 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑅 ∧ (𝑋 × {𝑆}) Fn 𝑋) → (∏t‘(𝑋 × {𝑆})) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝑔‘𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝑋 (𝑔‘𝑦))})) |
11 | 4, 8, 10 | syl2anc 693 |
. . . . . 6
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) →
(∏t‘(𝑋 × {𝑆})) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝑔‘𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝑋 (𝑔‘𝑦))})) |
12 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝑆 ∈ Top) |
13 | 12 | snssd 4340 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → {𝑆} ⊆ Top) |
14 | 6, 13 | fssd 6057 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × {𝑆}):𝑋⟶Top) |
15 | | eqid 2622 |
. . . . . . . . . 10
⊢ X𝑛 ∈
𝑋 ∪ ((𝑋
× {𝑆})‘𝑛) = X𝑛 ∈
𝑋 ∪ ((𝑋
× {𝑆})‘𝑛) |
16 | 9, 15 | ptbasfi 21384 |
. . . . . . . . 9
⊢ ((𝑋 ∈ 𝑅 ∧ (𝑋 × {𝑆}):𝑋⟶Top) → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝑔‘𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝑋 (𝑔‘𝑦))} = (fi‘({X𝑛 ∈
𝑋 ∪ ((𝑋
× {𝑆})‘𝑛)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢))))) |
17 | 4, 14, 16 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝑔‘𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝑋 (𝑔‘𝑦))} = (fi‘({X𝑛 ∈
𝑋 ∪ ((𝑋
× {𝑆})‘𝑛)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢))))) |
18 | | fvconst2g 6467 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 ∈ Top ∧ 𝑛 ∈ 𝑋) → ((𝑋 × {𝑆})‘𝑛) = 𝑆) |
19 | 18 | adantll 750 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑛 ∈ 𝑋) → ((𝑋 × {𝑆})‘𝑛) = 𝑆) |
20 | 19 | unieqd 4446 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑛 ∈ 𝑋) → ∪
((𝑋 × {𝑆})‘𝑛) = ∪ 𝑆) |
21 | 20 | ixpeq2dva 7923 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → X𝑛 ∈
𝑋 ∪ ((𝑋
× {𝑆})‘𝑛) = X𝑛 ∈
𝑋 ∪ 𝑆) |
22 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝑆 =
∪ 𝑆 |
23 | 22 | topopn 20711 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ Top → ∪ 𝑆
∈ 𝑆) |
24 | | ixpconstg 7917 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ 𝑅 ∧ ∪ 𝑆 ∈ 𝑆) → X𝑛 ∈ 𝑋 ∪ 𝑆 = (∪
𝑆
↑𝑚 𝑋)) |
25 | 3, 23, 24 | syl2an 494 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → X𝑛 ∈
𝑋 ∪ 𝑆 =
(∪ 𝑆 ↑𝑚 𝑋)) |
26 | 21, 25 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → X𝑛 ∈
𝑋 ∪ ((𝑋
× {𝑆})‘𝑛) = (∪ 𝑆
↑𝑚 𝑋)) |
27 | 26 | sneqd 4189 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → {X𝑛 ∈
𝑋 ∪ ((𝑋
× {𝑆})‘𝑛)} = {(∪ 𝑆
↑𝑚 𝑋)}) |
28 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ 𝑋 = 𝑋 |
29 | | fvconst2g 6467 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 ∈ Top ∧ 𝑘 ∈ 𝑋) → ((𝑋 × {𝑆})‘𝑘) = 𝑆) |
30 | 29 | adantll 750 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘 ∈ 𝑋) → ((𝑋 × {𝑆})‘𝑘) = 𝑆) |
31 | 26 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘 ∈ 𝑋) → X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) = (∪ 𝑆 ↑𝑚
𝑋)) |
32 | 31 | mpteq1d 4738 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘 ∈ 𝑋) → (𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) = (𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘))) |
33 | 32 | cnveqd 5298 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘 ∈ 𝑋) → ◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) = ◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘))) |
34 | 33 | imaeq1d 5465 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘 ∈ 𝑋) → (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) |
35 | 34 | ralrimivw 2967 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘 ∈ 𝑋) → ∀𝑢 ∈ ((𝑋 × {𝑆})‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) |
36 | 30, 35 | jca 554 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑘 ∈ 𝑋) → (((𝑋 × {𝑆})‘𝑘) = 𝑆 ∧ ∀𝑢 ∈ ((𝑋 × {𝑆})‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) |
37 | 36 | ralrimiva 2966 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) →
∀𝑘 ∈ 𝑋 (((𝑋 × {𝑆})‘𝑘) = 𝑆 ∧ ∀𝑢 ∈ ((𝑋 × {𝑆})‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) |
38 | | mpt2eq123 6714 |
. . . . . . . . . . . 12
⊢ ((𝑋 = 𝑋 ∧ ∀𝑘 ∈ 𝑋 (((𝑋 × {𝑆})‘𝑘) = 𝑆 ∧ ∀𝑢 ∈ ((𝑋 × {𝑆})‘𝑘)(◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) → (𝑘 ∈ 𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢)) = (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) |
39 | 28, 37, 38 | sylancr 695 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑘 ∈ 𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢)) = (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) |
40 | 39 | rneqd 5353 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ran (𝑘 ∈ 𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢)) = ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) |
41 | 27, 40 | uneq12d 3768 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ({X𝑛 ∈
𝑋 ∪ ((𝑋
× {𝑆})‘𝑛)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢))) = ({(∪ 𝑆 ↑𝑚
𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))) |
42 | 41 | fveq2d 6195 |
. . . . . . . 8
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) →
(fi‘({X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ ((𝑋 × {𝑆})‘𝑘) ↦ (◡(𝑤 ∈ X𝑛 ∈ 𝑋 ∪ ((𝑋 × {𝑆})‘𝑛) ↦ (𝑤‘𝑘)) “ 𝑢)))) = (fi‘({(∪ 𝑆
↑𝑚 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))))) |
43 | 17, 42 | eqtrd 2656 |
. . . . . . 7
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝑔‘𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝑋 (𝑔‘𝑦))} = (fi‘({(∪ 𝑆
↑𝑚 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))))) |
44 | 43 | fveq2d 6195 |
. . . . . 6
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) →
(topGen‘{𝑥 ∣
∃𝑔((𝑔 Fn 𝑋 ∧ ∀𝑦 ∈ 𝑋 (𝑔‘𝑦) ∈ ((𝑋 × {𝑆})‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝑋 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑋 × {𝑆})‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝑋 (𝑔‘𝑦))}) = (topGen‘(fi‘({(∪ 𝑆
↑𝑚 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))))) |
45 | 11, 44 | eqtrd 2656 |
. . . . 5
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) →
(∏t‘(𝑋 × {𝑆})) = (topGen‘(fi‘({(∪ 𝑆
↑𝑚 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))))) |
46 | 1, 45 | syl5eq 2668 |
. . . 4
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝐽 =
(topGen‘(fi‘({(∪ 𝑆 ↑𝑚 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))))) |
47 | 46 | oveq1d 6665 |
. . 3
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝐽 ↾t (𝑅 Cn 𝑆)) = ((topGen‘(fi‘({(∪ 𝑆
↑𝑚 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))))) ↾t (𝑅 Cn 𝑆))) |
48 | | firest 16093 |
. . . . 5
⊢
(fi‘(({(∪ 𝑆 ↑𝑚 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆))) = ((fi‘({(∪ 𝑆
↑𝑚 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))) ↾t (𝑅 Cn 𝑆)) |
49 | 48 | fveq2i 6194 |
. . . 4
⊢
(topGen‘(fi‘(({(∪ 𝑆 ↑𝑚
𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))) = (topGen‘((fi‘({(∪ 𝑆
↑𝑚 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))) ↾t (𝑅 Cn 𝑆))) |
50 | | fvex 6201 |
. . . . 5
⊢
(fi‘({(∪ 𝑆 ↑𝑚 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))) ∈ V |
51 | | ovex 6678 |
. . . . 5
⊢ (𝑅 Cn 𝑆) ∈ V |
52 | | tgrest 20963 |
. . . . 5
⊢
(((fi‘({(∪ 𝑆 ↑𝑚 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))) ∈ V ∧ (𝑅 Cn 𝑆) ∈ V) →
(topGen‘((fi‘({(∪ 𝑆 ↑𝑚 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))) ↾t (𝑅 Cn 𝑆))) = ((topGen‘(fi‘({(∪ 𝑆
↑𝑚 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))))) ↾t (𝑅 Cn 𝑆))) |
53 | 50, 51, 52 | mp2an 708 |
. . . 4
⊢
(topGen‘((fi‘({(∪ 𝑆 ↑𝑚
𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))) ↾t (𝑅 Cn 𝑆))) = ((topGen‘(fi‘({(∪ 𝑆
↑𝑚 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))))) ↾t (𝑅 Cn 𝑆)) |
54 | 49, 53 | eqtri 2644 |
. . 3
⊢
(topGen‘(fi‘(({(∪ 𝑆 ↑𝑚
𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))) = ((topGen‘(fi‘({(∪ 𝑆
↑𝑚 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))))) ↾t (𝑅 Cn 𝑆)) |
55 | 47, 54 | syl6eqr 2674 |
. 2
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝐽 ↾t (𝑅 Cn 𝑆)) = (topGen‘(fi‘(({(∪ 𝑆
↑𝑚 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆))))) |
56 | | xkotop 21391 |
. . 3
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑆 ^ko 𝑅) ∈ Top) |
57 | | snex 4908 |
. . . . . 6
⊢ {(∪ 𝑆
↑𝑚 𝑋)} ∈ V |
58 | | mpt2exga 7246 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝑅 ∧ 𝑆 ∈ Top) → (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V) |
59 | 3, 58 | sylan 488 |
. . . . . . 7
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V) |
60 | | rnexg 7098 |
. . . . . . 7
⊢ ((𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V → ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V) |
61 | 59, 60 | syl 17 |
. . . . . 6
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V) |
62 | | unexg 6959 |
. . . . . 6
⊢ (({(∪ 𝑆
↑𝑚 𝑋)} ∈ V ∧ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V) → ({(∪ 𝑆
↑𝑚 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V) |
63 | 57, 61, 62 | sylancr 695 |
. . . . 5
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ({(∪ 𝑆
↑𝑚 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V) |
64 | | restval 16087 |
. . . . 5
⊢
((({(∪ 𝑆 ↑𝑚 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V ∧ (𝑅 Cn 𝑆) ∈ V) → (({(∪ 𝑆
↑𝑚 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)) = ran (𝑥 ∈ ({(∪ 𝑆 ↑𝑚
𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↦ (𝑥 ∩ (𝑅 Cn 𝑆)))) |
65 | 63, 51, 64 | sylancl 694 |
. . . 4
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (({(∪ 𝑆
↑𝑚 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)) = ran (𝑥 ∈ ({(∪ 𝑆 ↑𝑚
𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↦ (𝑥 ∩ (𝑅 Cn 𝑆)))) |
66 | | elun 3753 |
. . . . . . 7
⊢ (𝑥 ∈ ({(∪ 𝑆
↑𝑚 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↔ (𝑥 ∈ {(∪ 𝑆 ↑𝑚
𝑋)} ∨ 𝑥 ∈ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))) |
67 | 2, 22 | cnf 21050 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝑅 Cn 𝑆) → 𝑥:𝑋⟶∪ 𝑆) |
68 | | elmapg 7870 |
. . . . . . . . . . . . . . 15
⊢ ((∪ 𝑆
∈ 𝑆 ∧ 𝑋 ∈ 𝑅) → (𝑥 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↔ 𝑥:𝑋⟶∪ 𝑆)) |
69 | 23, 3, 68 | syl2anr 495 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑥 ∈ (∪ 𝑆
↑𝑚 𝑋) ↔ 𝑥:𝑋⟶∪ 𝑆)) |
70 | 67, 69 | syl5ibr 236 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑥 ∈ (𝑅 Cn 𝑆) → 𝑥 ∈ (∪ 𝑆 ↑𝑚
𝑋))) |
71 | 70 | ssrdv 3609 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) ⊆ (∪
𝑆
↑𝑚 𝑋)) |
72 | 71 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {(∪ 𝑆
↑𝑚 𝑋)}) → (𝑅 Cn 𝑆) ⊆ (∪
𝑆
↑𝑚 𝑋)) |
73 | | elsni 4194 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ {(∪ 𝑆
↑𝑚 𝑋)} → 𝑥 = (∪ 𝑆 ↑𝑚
𝑋)) |
74 | 73 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {(∪ 𝑆
↑𝑚 𝑋)}) → 𝑥 = (∪ 𝑆 ↑𝑚
𝑋)) |
75 | 72, 74 | sseqtr4d 3642 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {(∪ 𝑆
↑𝑚 𝑋)}) → (𝑅 Cn 𝑆) ⊆ 𝑥) |
76 | | sseqin2 3817 |
. . . . . . . . . 10
⊢ ((𝑅 Cn 𝑆) ⊆ 𝑥 ↔ (𝑥 ∩ (𝑅 Cn 𝑆)) = (𝑅 Cn 𝑆)) |
77 | 75, 76 | sylib 208 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {(∪ 𝑆
↑𝑚 𝑋)}) → (𝑥 ∩ (𝑅 Cn 𝑆)) = (𝑅 Cn 𝑆)) |
78 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (𝑆 ^ko 𝑅) = (𝑆 ^ko 𝑅) |
79 | 78 | xkouni 21402 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) = ∪ (𝑆 ^ko 𝑅)) |
80 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ ∪ (𝑆
^ko 𝑅) =
∪ (𝑆 ^ko 𝑅) |
81 | 80 | topopn 20711 |
. . . . . . . . . . . 12
⊢ ((𝑆 ^ko 𝑅) ∈ Top → ∪ (𝑆
^ko 𝑅)
∈ (𝑆
^ko 𝑅)) |
82 | 56, 81 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ∪ (𝑆
^ko 𝑅)
∈ (𝑆
^ko 𝑅)) |
83 | 79, 82 | eqeltrd 2701 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 Cn 𝑆) ∈ (𝑆 ^ko 𝑅)) |
84 | 83 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {(∪ 𝑆
↑𝑚 𝑋)}) → (𝑅 Cn 𝑆) ∈ (𝑆 ^ko 𝑅)) |
85 | 77, 84 | eqeltrd 2701 |
. . . . . . . 8
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ {(∪ 𝑆
↑𝑚 𝑋)}) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ^ko 𝑅)) |
86 | | eqid 2622 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) = (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) |
87 | 86 | rnmpt2 6770 |
. . . . . . . . . 10
⊢ ran
(𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) = {𝑥 ∣ ∃𝑘 ∈ 𝑋 ∃𝑢 ∈ 𝑆 𝑥 = (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)} |
88 | 87 | abeq2i 2735 |
. . . . . . . . 9
⊢ (𝑥 ∈ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) ↔ ∃𝑘 ∈ 𝑋 ∃𝑢 ∈ 𝑆 𝑥 = (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) |
89 | | cnvresima 5623 |
. . . . . . . . . . . . . . 15
⊢ (◡((𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) ↾ (𝑅 Cn 𝑆)) “ 𝑢) = ((◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)) |
90 | 71 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (𝑅 Cn 𝑆) ⊆ (∪
𝑆
↑𝑚 𝑋)) |
91 | 90 | resmptd 5452 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → ((𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) ↾ (𝑅 Cn 𝑆)) = (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘))) |
92 | 91 | cnveqd 5298 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → ◡((𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) ↾ (𝑅 Cn 𝑆)) = ◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘))) |
93 | 92 | imaeq1d 5465 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (◡((𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) ↾ (𝑅 Cn 𝑆)) “ 𝑢) = (◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) “ 𝑢)) |
94 | 89, 93 | syl5eqr 2670 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → ((◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)) = (◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) “ 𝑢)) |
95 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤‘𝑘) ∈ V |
96 | 95 | rgenw 2924 |
. . . . . . . . . . . . . . . . . . 19
⊢
∀𝑤 ∈
(𝑅 Cn 𝑆)(𝑤‘𝑘) ∈ V |
97 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) = (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) |
98 | 97 | fnmpt 6020 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑤 ∈
(𝑅 Cn 𝑆)(𝑤‘𝑘) ∈ V → (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) Fn (𝑅 Cn 𝑆)) |
99 | 96, 98 | mp1i 13 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) Fn (𝑅 Cn 𝑆)) |
100 | | elpreima 6337 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) Fn (𝑅 Cn 𝑆) → (𝑓 ∈ (◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) “ 𝑢) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘))‘𝑓) ∈ 𝑢))) |
101 | 99, 100 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (𝑓 ∈ (◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) “ 𝑢) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘))‘𝑓) ∈ 𝑢))) |
102 | | fveq1 6190 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 = 𝑓 → (𝑤‘𝑘) = (𝑓‘𝑘)) |
103 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓‘𝑘) ∈ V |
104 | 102, 97, 103 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 ∈ (𝑅 Cn 𝑆) → ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘))‘𝑓) = (𝑓‘𝑘)) |
105 | 104 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘))‘𝑓) = (𝑓‘𝑘)) |
106 | 105 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → (((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘))‘𝑓) ∈ 𝑢 ↔ (𝑓‘𝑘) ∈ 𝑢)) |
107 | 103 | snss 4316 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓‘𝑘) ∈ 𝑢 ↔ {(𝑓‘𝑘)} ⊆ 𝑢) |
108 | 90 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → 𝑓 ∈ (∪ 𝑆 ↑𝑚
𝑋)) |
109 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 ∈ (∪ 𝑆
↑𝑚 𝑋) → 𝑓:𝑋⟶∪ 𝑆) |
110 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓:𝑋⟶∪ 𝑆 → 𝑓 Fn 𝑋) |
111 | 108, 109,
110 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → 𝑓 Fn 𝑋) |
112 | | simplrl 800 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → 𝑘 ∈ 𝑋) |
113 | | fnsnfv 6258 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑓 Fn 𝑋 ∧ 𝑘 ∈ 𝑋) → {(𝑓‘𝑘)} = (𝑓 “ {𝑘})) |
114 | 111, 112,
113 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → {(𝑓‘𝑘)} = (𝑓 “ {𝑘})) |
115 | 114 | sseq1d 3632 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → ({(𝑓‘𝑘)} ⊆ 𝑢 ↔ (𝑓 “ {𝑘}) ⊆ 𝑢)) |
116 | 107, 115 | syl5bb 272 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → ((𝑓‘𝑘) ∈ 𝑢 ↔ (𝑓 “ {𝑘}) ⊆ 𝑢)) |
117 | 106, 116 | bitrd 268 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) ∧ 𝑓 ∈ (𝑅 Cn 𝑆)) → (((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘))‘𝑓) ∈ 𝑢 ↔ (𝑓 “ {𝑘}) ⊆ 𝑢)) |
118 | 117 | pm5.32da 673 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → ((𝑓 ∈ (𝑅 Cn 𝑆) ∧ ((𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘))‘𝑓) ∈ 𝑢) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 “ {𝑘}) ⊆ 𝑢))) |
119 | 101, 118 | bitrd 268 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (𝑓 ∈ (◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) “ 𝑢) ↔ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 “ {𝑘}) ⊆ 𝑢))) |
120 | 119 | abbi2dv 2742 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) “ 𝑢) = {𝑓 ∣ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 “ {𝑘}) ⊆ 𝑢)}) |
121 | | df-rab 2921 |
. . . . . . . . . . . . . . 15
⊢ {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ {𝑘}) ⊆ 𝑢} = {𝑓 ∣ (𝑓 ∈ (𝑅 Cn 𝑆) ∧ (𝑓 “ {𝑘}) ⊆ 𝑢)} |
122 | 120, 121 | syl6eqr 2674 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (◡(𝑤 ∈ (𝑅 Cn 𝑆) ↦ (𝑤‘𝑘)) “ 𝑢) = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ {𝑘}) ⊆ 𝑢}) |
123 | 94, 122 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → ((◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)) = {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ {𝑘}) ⊆ 𝑢}) |
124 | | simpll 790 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → 𝑅 ∈ Top) |
125 | 12 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → 𝑆 ∈ Top) |
126 | | simprl 794 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → 𝑘 ∈ 𝑋) |
127 | 126 | snssd 4340 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → {𝑘} ⊆ 𝑋) |
128 | 2 | toptopon 20722 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘𝑋)) |
129 | 124, 128 | sylib 208 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → 𝑅 ∈ (TopOn‘𝑋)) |
130 | | restsn2 20975 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑘 ∈ 𝑋) → (𝑅 ↾t {𝑘}) = 𝒫 {𝑘}) |
131 | 129, 126,
130 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (𝑅 ↾t {𝑘}) = 𝒫 {𝑘}) |
132 | | snfi 8038 |
. . . . . . . . . . . . . . . 16
⊢ {𝑘} ∈ Fin |
133 | | discmp 21201 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑘} ∈ Fin ↔ 𝒫
{𝑘} ∈
Comp) |
134 | 132, 133 | mpbi 220 |
. . . . . . . . . . . . . . 15
⊢ 𝒫
{𝑘} ∈
Comp |
135 | 131, 134 | syl6eqel 2709 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (𝑅 ↾t {𝑘}) ∈ Comp) |
136 | | simprr 796 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → 𝑢 ∈ 𝑆) |
137 | 2, 124, 125, 127, 135, 136 | xkoopn 21392 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → {𝑓 ∈ (𝑅 Cn 𝑆) ∣ (𝑓 “ {𝑘}) ⊆ 𝑢} ∈ (𝑆 ^ko 𝑅)) |
138 | 123, 137 | eqeltrd 2701 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → ((◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ^ko 𝑅)) |
139 | | ineq1 3807 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) → (𝑥 ∩ (𝑅 Cn 𝑆)) = ((◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆))) |
140 | 139 | eleq1d 2686 |
. . . . . . . . . . . 12
⊢ (𝑥 = (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) → ((𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ^ko 𝑅) ↔ ((◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ^ko 𝑅))) |
141 | 138, 140 | syl5ibrcom 237 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑘 ∈ 𝑋 ∧ 𝑢 ∈ 𝑆)) → (𝑥 = (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ^ko 𝑅))) |
142 | 141 | rexlimdvva 3038 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) →
(∃𝑘 ∈ 𝑋 ∃𝑢 ∈ 𝑆 𝑥 = (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ^ko 𝑅))) |
143 | 142 | imp 445 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ ∃𝑘 ∈ 𝑋 ∃𝑢 ∈ 𝑆 𝑥 = (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ^ko 𝑅)) |
144 | 88, 143 | sylan2b 492 |
. . . . . . . 8
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ^ko 𝑅)) |
145 | 85, 144 | jaodan 826 |
. . . . . . 7
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑥 ∈ {(∪ 𝑆
↑𝑚 𝑋)} ∨ 𝑥 ∈ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ^ko 𝑅)) |
146 | 66, 145 | sylan2b 492 |
. . . . . 6
⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ 𝑥 ∈ ({(∪ 𝑆
↑𝑚 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))) → (𝑥 ∩ (𝑅 Cn 𝑆)) ∈ (𝑆 ^ko 𝑅)) |
147 | | eqid 2622 |
. . . . . 6
⊢ (𝑥 ∈ ({(∪ 𝑆
↑𝑚 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↦ (𝑥 ∩ (𝑅 Cn 𝑆))) = (𝑥 ∈ ({(∪ 𝑆 ↑𝑚
𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↦ (𝑥 ∩ (𝑅 Cn 𝑆))) |
148 | 146, 147 | fmptd 6385 |
. . . . 5
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑥 ∈ ({(∪ 𝑆
↑𝑚 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↦ (𝑥 ∩ (𝑅 Cn 𝑆))):({(∪ 𝑆 ↑𝑚
𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))⟶(𝑆 ^ko 𝑅)) |
149 | | frn 6053 |
. . . . 5
⊢ ((𝑥 ∈ ({(∪ 𝑆
↑𝑚 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↦ (𝑥 ∩ (𝑅 Cn 𝑆))):({(∪ 𝑆 ↑𝑚
𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢)))⟶(𝑆 ^ko 𝑅) → ran (𝑥 ∈ ({(∪ 𝑆 ↑𝑚
𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↦ (𝑥 ∩ (𝑅 Cn 𝑆))) ⊆ (𝑆 ^ko 𝑅)) |
150 | 148, 149 | syl 17 |
. . . 4
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ran (𝑥 ∈ ({(∪ 𝑆
↑𝑚 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↦ (𝑥 ∩ (𝑅 Cn 𝑆))) ⊆ (𝑆 ^ko 𝑅)) |
151 | 65, 150 | eqsstrd 3639 |
. . 3
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (({(∪ 𝑆
↑𝑚 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)) ⊆ (𝑆 ^ko 𝑅)) |
152 | | tgfiss 20795 |
. . 3
⊢ (((𝑆 ^ko 𝑅) ∈ Top ∧ (({(∪ 𝑆
↑𝑚 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)) ⊆ (𝑆 ^ko 𝑅)) → (topGen‘(fi‘(({(∪ 𝑆
↑𝑚 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))) ⊆ (𝑆 ^ko 𝑅)) |
153 | 56, 151, 152 | syl2anc 693 |
. 2
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) →
(topGen‘(fi‘(({(∪ 𝑆 ↑𝑚 𝑋)} ∪ ran (𝑘 ∈ 𝑋, 𝑢 ∈ 𝑆 ↦ (◡(𝑤 ∈ (∪ 𝑆 ↑𝑚
𝑋) ↦ (𝑤‘𝑘)) “ 𝑢))) ↾t (𝑅 Cn 𝑆)))) ⊆ (𝑆 ^ko 𝑅)) |
154 | 55, 153 | eqsstrd 3639 |
1
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝐽 ↾t (𝑅 Cn 𝑆)) ⊆ (𝑆 ^ko 𝑅)) |