Step | Hyp | Ref
| Expression |
1 | | distop 20799 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Top) |
2 | 1 | adantl 482 |
. . . 4
⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → 𝒫 𝐴 ∈ Top) |
3 | | simpl 473 |
. . . 4
⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → 𝑅 ∈ Top) |
4 | | unipw 4918 |
. . . . . 6
⊢ ∪ 𝒫 𝐴 = 𝐴 |
5 | 4 | eqcomi 2631 |
. . . . 5
⊢ 𝐴 = ∪
𝒫 𝐴 |
6 | | eqid 2622 |
. . . . 5
⊢ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp} = {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp} |
7 | | eqid 2622 |
. . . . 5
⊢ (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) |
8 | 5, 6, 7 | xkoval 21390 |
. . . 4
⊢
((𝒫 𝐴 ∈
Top ∧ 𝑅 ∈ Top)
→ (𝑅
^ko 𝒫 𝐴) = (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})))) |
9 | 2, 3, 8 | syl2anc 693 |
. . 3
⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝑅 ^ko 𝒫 𝐴) = (topGen‘(fi‘ran
(𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})))) |
10 | | simpr 477 |
. . . . 5
⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → 𝐴 ∈ 𝑉) |
11 | | fconst6g 6094 |
. . . . . 6
⊢ (𝑅 ∈ Top → (𝐴 × {𝑅}):𝐴⟶Top) |
12 | 11 | adantr 481 |
. . . . 5
⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝐴 × {𝑅}):𝐴⟶Top) |
13 | | pttop 21385 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ (𝐴 × {𝑅}):𝐴⟶Top) →
(∏t‘(𝐴 × {𝑅})) ∈ Top) |
14 | 10, 12, 13 | syl2anc 693 |
. . . 4
⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (∏t‘(𝐴 × {𝑅})) ∈ Top) |
15 | | elpwi 4168 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴) |
16 | | restdis 20982 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ⊆ 𝐴) → (𝒫 𝐴 ↾t 𝑥) = 𝒫 𝑥) |
17 | 15, 16 | sylan2 491 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ 𝒫 𝐴) → (𝒫 𝐴 ↾t 𝑥) = 𝒫 𝑥) |
18 | 17 | adantll 750 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ 𝒫 𝐴) → (𝒫 𝐴 ↾t 𝑥) = 𝒫 𝑥) |
19 | 18 | eleq1d 2686 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ 𝒫 𝐴) → ((𝒫 𝐴 ↾t 𝑥) ∈ Comp ↔ 𝒫 𝑥 ∈ Comp)) |
20 | | discmp 21201 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ Fin ↔ 𝒫
𝑥 ∈
Comp) |
21 | 19, 20 | syl6bbr 278 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ 𝑥 ∈ 𝒫 𝐴) → ((𝒫 𝐴 ↾t 𝑥) ∈ Comp ↔ 𝑥 ∈ Fin)) |
22 | 21 | rabbidva 3188 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp} = {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ∈ Fin}) |
23 | | dfin5 3582 |
. . . . . . . . 9
⊢
(𝒫 𝐴 ∩
Fin) = {𝑥 ∈ 𝒫
𝐴 ∣ 𝑥 ∈ Fin} |
24 | 22, 23 | syl6eqr 2674 |
. . . . . . . 8
⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp} = (𝒫 𝐴 ∩ Fin)) |
25 | | eqidd 2623 |
. . . . . . . 8
⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → 𝑅 = 𝑅) |
26 | | eqid 2622 |
. . . . . . . . . . 11
⊢ ∪ 𝑅 =
∪ 𝑅 |
27 | 26 | toptopon 20722 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘∪ 𝑅)) |
28 | | cndis 21095 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ (TopOn‘∪ 𝑅))
→ (𝒫 𝐴 Cn
𝑅) = (∪ 𝑅
↑𝑚 𝐴)) |
29 | 28 | ancoms 469 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ (TopOn‘∪ 𝑅)
∧ 𝐴 ∈ 𝑉) → (𝒫 𝐴 Cn 𝑅) = (∪ 𝑅 ↑𝑚
𝐴)) |
30 | 27, 29 | sylanb 489 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝒫 𝐴 Cn 𝑅) = (∪ 𝑅 ↑𝑚
𝐴)) |
31 | | rabeq 3192 |
. . . . . . . . 9
⊢
((𝒫 𝐴 Cn
𝑅) = (∪ 𝑅
↑𝑚 𝐴) → {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} = {𝑓 ∈ (∪ 𝑅 ↑𝑚
𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) |
32 | 30, 31 | syl 17 |
. . . . . . . 8
⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} = {𝑓 ∈ (∪ 𝑅 ↑𝑚
𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) |
33 | 24, 25, 32 | mpt2eq123dv 6717 |
. . . . . . 7
⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = (𝑘 ∈ (𝒫 𝐴 ∩ Fin), 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (∪ 𝑅 ↑𝑚
𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})) |
34 | 33 | rneqd 5353 |
. . . . . 6
⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = ran (𝑘 ∈ (𝒫 𝐴 ∩ Fin), 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (∪ 𝑅 ↑𝑚
𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣})) |
35 | | eqid 2622 |
. . . . . . 7
⊢ (𝑘 ∈ (𝒫 𝐴 ∩ Fin), 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (∪ 𝑅 ↑𝑚
𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = (𝑘 ∈ (𝒫 𝐴 ∩ Fin), 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (∪ 𝑅 ↑𝑚
𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) |
36 | 35 | rnmpt2 6770 |
. . . . . 6
⊢ ran
(𝑘 ∈ (𝒫 𝐴 ∩ Fin), 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (∪ 𝑅 ↑𝑚
𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = {𝑥 ∣ ∃𝑘 ∈ (𝒫 𝐴 ∩ Fin)∃𝑣 ∈ 𝑅 𝑥 = {𝑓 ∈ (∪ 𝑅 ↑𝑚
𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}} |
37 | 34, 36 | syl6eq 2672 |
. . . . 5
⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) = {𝑥 ∣ ∃𝑘 ∈ (𝒫 𝐴 ∩ Fin)∃𝑣 ∈ 𝑅 𝑥 = {𝑓 ∈ (∪ 𝑅 ↑𝑚
𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}}) |
38 | | elmapi 7879 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ (∪ 𝑅
↑𝑚 𝐴) → 𝑓:𝐴⟶∪ 𝑅) |
39 | | eleq2 2690 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 = if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → ((𝑓‘𝑥) ∈ 𝑣 ↔ (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅))) |
40 | 39 | imbi2d 330 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → ((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ 𝑣) ↔ (𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)))) |
41 | 40 | bibi1d 333 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → (((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ 𝑣) ↔ (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣)) ↔ ((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)) ↔ (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣)))) |
42 | | eleq2 2690 |
. . . . . . . . . . . . . . . . 17
⊢ (∪ 𝑅 =
if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → ((𝑓‘𝑥) ∈ ∪ 𝑅 ↔ (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅))) |
43 | 42 | imbi2d 330 |
. . . . . . . . . . . . . . . 16
⊢ (∪ 𝑅 =
if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → ((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ ∪ 𝑅) ↔ (𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)))) |
44 | 43 | bibi1d 333 |
. . . . . . . . . . . . . . 15
⊢ (∪ 𝑅 =
if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → (((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ ∪ 𝑅) ↔ (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣)) ↔ ((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)) ↔ (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣)))) |
45 | | inss1 3833 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(𝒫 𝐴 ∩
Fin) ⊆ 𝒫 𝐴 |
46 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → 𝑘 ∈ (𝒫 𝐴 ∩ Fin)) |
47 | 45, 46 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → 𝑘 ∈ 𝒫 𝐴) |
48 | 47 | elpwid 4170 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → 𝑘 ⊆ 𝐴) |
49 | 48 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → 𝑘 ⊆ 𝐴) |
50 | 49 | sselda 3603 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑅 ∈ Top
∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) ∧ 𝑥 ∈ 𝑘) → 𝑥 ∈ 𝐴) |
51 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑅 ∈ Top
∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) ∧ 𝑥 ∈ 𝑘) → 𝑥 ∈ 𝑘) |
52 | 50, 51 | 2thd 255 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑅 ∈ Top
∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) ∧ 𝑥 ∈ 𝑘) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝑘)) |
53 | 52 | imbi1d 331 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈ Top
∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) ∧ 𝑥 ∈ 𝑘) → ((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ 𝑣) ↔ (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣))) |
54 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓:𝐴⟶∪ 𝑅 ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ∪ 𝑅) |
55 | 54 | ex 450 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓:𝐴⟶∪ 𝑅 → (𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ ∪ 𝑅)) |
56 | 55 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → (𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ ∪ 𝑅)) |
57 | 56 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑅 ∈ Top
∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) ∧ ¬ 𝑥 ∈ 𝑘) → (𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ ∪ 𝑅)) |
58 | | pm2.21 120 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑥 ∈ 𝑘 → (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣)) |
59 | 58 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑅 ∈ Top
∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) ∧ ¬ 𝑥 ∈ 𝑘) → (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣)) |
60 | 57, 59 | 2thd 255 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑅 ∈ Top
∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) ∧ ¬ 𝑥 ∈ 𝑘) → ((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ ∪ 𝑅) ↔ (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣))) |
61 | 41, 44, 53, 60 | ifbothda 4123 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → ((𝑥 ∈ 𝐴 → (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)) ↔ (𝑥 ∈ 𝑘 → (𝑓‘𝑥) ∈ 𝑣))) |
62 | 61 | ralbidv2 2984 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ↔ ∀𝑥 ∈ 𝑘 (𝑓‘𝑥) ∈ 𝑣)) |
63 | | ffn 6045 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:𝐴⟶∪ 𝑅 → 𝑓 Fn 𝐴) |
64 | 63 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → 𝑓 Fn 𝐴) |
65 | | vex 3203 |
. . . . . . . . . . . . . . . 16
⊢ 𝑓 ∈ V |
66 | 65 | elixp 7915 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ X𝑥 ∈
𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅))) |
67 | 66 | baib 944 |
. . . . . . . . . . . . . 14
⊢ (𝑓 Fn 𝐴 → (𝑓 ∈ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ↔ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅))) |
68 | 64, 67 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → (𝑓 ∈ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ↔ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅))) |
69 | | ffun 6048 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:𝐴⟶∪ 𝑅 → Fun 𝑓) |
70 | 69 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → Fun 𝑓) |
71 | | fdm 6051 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:𝐴⟶∪ 𝑅 → dom 𝑓 = 𝐴) |
72 | 71 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → dom 𝑓 = 𝐴) |
73 | 49, 72 | sseqtr4d 3642 |
. . . . . . . . . . . . . 14
⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → 𝑘 ⊆ dom 𝑓) |
74 | | funimass4 6247 |
. . . . . . . . . . . . . 14
⊢ ((Fun
𝑓 ∧ 𝑘 ⊆ dom 𝑓) → ((𝑓 “ 𝑘) ⊆ 𝑣 ↔ ∀𝑥 ∈ 𝑘 (𝑓‘𝑥) ∈ 𝑣)) |
75 | 70, 73, 74 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → ((𝑓 “ 𝑘) ⊆ 𝑣 ↔ ∀𝑥 ∈ 𝑘 (𝑓‘𝑥) ∈ 𝑣)) |
76 | 62, 68, 75 | 3bitr4d 300 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓:𝐴⟶∪ 𝑅) → (𝑓 ∈ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ↔ (𝑓 “ 𝑘) ⊆ 𝑣)) |
77 | 38, 76 | sylan2 491 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑓 ∈ (∪ 𝑅 ↑𝑚
𝐴)) → (𝑓 ∈ X𝑥 ∈
𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ↔ (𝑓 “ 𝑘) ⊆ 𝑣)) |
78 | 77 | rabbi2dva 3821 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → ((∪
𝑅
↑𝑚 𝐴) ∩ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)) = {𝑓 ∈ (∪ 𝑅 ↑𝑚
𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) |
79 | | elssuni 4467 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 ∈ 𝑅 → 𝑣 ⊆ ∪ 𝑅) |
80 | 79 | ad2antll 765 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → 𝑣 ⊆ ∪ 𝑅) |
81 | | ssid 3624 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑅
⊆ ∪ 𝑅 |
82 | | sseq1 3626 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → (𝑣 ⊆ ∪ 𝑅 ↔ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ ∪ 𝑅)) |
83 | | sseq1 3626 |
. . . . . . . . . . . . . . . 16
⊢ (∪ 𝑅 =
if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) → (∪ 𝑅
⊆ ∪ 𝑅 ↔ if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ ∪ 𝑅)) |
84 | 82, 83 | ifboth 4124 |
. . . . . . . . . . . . . . 15
⊢ ((𝑣 ⊆ ∪ 𝑅
∧ ∪ 𝑅 ⊆ ∪ 𝑅) → if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ ∪ 𝑅) |
85 | 80, 81, 84 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ ∪ 𝑅) |
86 | 85 | ralrimivw 2967 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → ∀𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ ∪ 𝑅) |
87 | | ss2ixp 7921 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ ∪ 𝑅
→ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ X𝑥 ∈
𝐴 ∪ 𝑅) |
88 | 86, 87 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ X𝑥 ∈
𝐴 ∪ 𝑅) |
89 | | simplr 792 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → 𝐴 ∈ 𝑉) |
90 | | uniexg 6955 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ Top → ∪ 𝑅
∈ V) |
91 | 90 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → ∪ 𝑅 ∈ V) |
92 | | ixpconstg 7917 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ ∪ 𝑅 ∈ V) → X𝑥 ∈
𝐴 ∪ 𝑅 =
(∪ 𝑅 ↑𝑚 𝐴)) |
93 | 89, 91, 92 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → X𝑥 ∈ 𝐴 ∪ 𝑅 = (∪
𝑅
↑𝑚 𝐴)) |
94 | 88, 93 | sseqtrd 3641 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ (∪ 𝑅
↑𝑚 𝐴)) |
95 | | sseqin2 3817 |
. . . . . . . . . . 11
⊢ (X𝑥 ∈
𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ⊆ (∪ 𝑅
↑𝑚 𝐴) ↔ ((∪
𝑅
↑𝑚 𝐴) ∩ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)) = X𝑥 ∈
𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)) |
96 | 94, 95 | sylib 208 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → ((∪
𝑅
↑𝑚 𝐴) ∩ X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)) = X𝑥 ∈
𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)) |
97 | 78, 96 | eqtr3d 2658 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → {𝑓 ∈ (∪ 𝑅 ↑𝑚
𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} = X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅)) |
98 | 11 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → (𝐴 × {𝑅}):𝐴⟶Top) |
99 | | inss2 3834 |
. . . . . . . . . . 11
⊢
(𝒫 𝐴 ∩
Fin) ⊆ Fin |
100 | 99, 46 | sseldi 3601 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → 𝑘 ∈ Fin) |
101 | | simplrr 801 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ 𝐴) → 𝑣 ∈ 𝑅) |
102 | 26 | topopn 20711 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ Top → ∪ 𝑅
∈ 𝑅) |
103 | 102 | ad3antrrr 766 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ 𝐴) → ∪ 𝑅 ∈ 𝑅) |
104 | 101, 103 | ifcld 4131 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ∈ 𝑅) |
105 | | simpll 790 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → 𝑅 ∈ Top) |
106 | | fvconst2g 6467 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Top ∧ 𝑥 ∈ 𝐴) → ((𝐴 × {𝑅})‘𝑥) = 𝑅) |
107 | 105, 106 | sylan 488 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ 𝐴) → ((𝐴 × {𝑅})‘𝑥) = 𝑅) |
108 | 104, 107 | eleqtrrd 2704 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ 𝐴) → if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ∈ ((𝐴 × {𝑅})‘𝑥)) |
109 | | eldifn 3733 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝐴 ∖ 𝑘) → ¬ 𝑥 ∈ 𝑘) |
110 | 109 | iffalsed 4097 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝐴 ∖ 𝑘) → if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) = ∪
𝑅) |
111 | 110 | adantl 482 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ (𝐴 ∖ 𝑘)) → if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) = ∪
𝑅) |
112 | | eldifi 3732 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝐴 ∖ 𝑘) → 𝑥 ∈ 𝐴) |
113 | 112, 107 | sylan2 491 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ (𝐴 ∖ 𝑘)) → ((𝐴 × {𝑅})‘𝑥) = 𝑅) |
114 | 113 | unieqd 4446 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ (𝐴 ∖ 𝑘)) → ∪
((𝐴 × {𝑅})‘𝑥) = ∪ 𝑅) |
115 | 111, 114 | eqtr4d 2659 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) ∧ 𝑥 ∈ (𝐴 ∖ 𝑘)) → if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) = ∪
((𝐴 × {𝑅})‘𝑥)) |
116 | 89, 98, 100, 108, 115 | ptopn 21386 |
. . . . . . . . 9
⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → X𝑥 ∈ 𝐴 if(𝑥 ∈ 𝑘, 𝑣, ∪ 𝑅) ∈
(∏t‘(𝐴 × {𝑅}))) |
117 | 97, 116 | eqeltrd 2701 |
. . . . . . . 8
⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → {𝑓 ∈ (∪ 𝑅 ↑𝑚
𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} ∈ (∏t‘(𝐴 × {𝑅}))) |
118 | | eleq1 2689 |
. . . . . . . 8
⊢ (𝑥 = {𝑓 ∈ (∪ 𝑅 ↑𝑚
𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} → (𝑥 ∈ (∏t‘(𝐴 × {𝑅})) ↔ {𝑓 ∈ (∪ 𝑅 ↑𝑚
𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} ∈ (∏t‘(𝐴 × {𝑅})))) |
119 | 117, 118 | syl5ibrcom 237 |
. . . . . . 7
⊢ (((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣 ∈ 𝑅)) → (𝑥 = {𝑓 ∈ (∪ 𝑅 ↑𝑚
𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} → 𝑥 ∈ (∏t‘(𝐴 × {𝑅})))) |
120 | 119 | rexlimdvva 3038 |
. . . . . 6
⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (∃𝑘 ∈ (𝒫 𝐴 ∩ Fin)∃𝑣 ∈ 𝑅 𝑥 = {𝑓 ∈ (∪ 𝑅 ↑𝑚
𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣} → 𝑥 ∈ (∏t‘(𝐴 × {𝑅})))) |
121 | 120 | abssdv 3676 |
. . . . 5
⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → {𝑥 ∣ ∃𝑘 ∈ (𝒫 𝐴 ∩ Fin)∃𝑣 ∈ 𝑅 𝑥 = {𝑓 ∈ (∪ 𝑅 ↑𝑚
𝐴) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}} ⊆ (∏t‘(𝐴 × {𝑅}))) |
122 | 37, 121 | eqsstrd 3639 |
. . . 4
⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ⊆ (∏t‘(𝐴 × {𝑅}))) |
123 | | tgfiss 20795 |
. . . 4
⊢
(((∏t‘(𝐴 × {𝑅})) ∈ Top ∧ ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}) ⊆ (∏t‘(𝐴 × {𝑅}))) → (topGen‘(fi‘ran
(𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))) ⊆ (∏t‘(𝐴 × {𝑅}))) |
124 | 14, 122, 123 | syl2anc 693 |
. . 3
⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴 ↾t 𝑥) ∈ Comp}, 𝑣 ∈ 𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓 “ 𝑘) ⊆ 𝑣}))) ⊆ (∏t‘(𝐴 × {𝑅}))) |
125 | 9, 124 | eqsstrd 3639 |
. 2
⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝑅 ^ko 𝒫 𝐴) ⊆
(∏t‘(𝐴 × {𝑅}))) |
126 | | eqid 2622 |
. . . . . . . 8
⊢
(∏t‘(𝐴 × {𝑅})) = (∏t‘(𝐴 × {𝑅})) |
127 | 126, 26 | ptuniconst 21401 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑅 ∈ Top) → (∪ 𝑅
↑𝑚 𝐴) = ∪
(∏t‘(𝐴 × {𝑅}))) |
128 | 127 | ancoms 469 |
. . . . . 6
⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (∪ 𝑅 ↑𝑚
𝐴) = ∪ (∏t‘(𝐴 × {𝑅}))) |
129 | 30, 128 | eqtrd 2656 |
. . . . 5
⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝒫 𝐴 Cn 𝑅) = ∪
(∏t‘(𝐴 × {𝑅}))) |
130 | 129 | oveq2d 6666 |
. . . 4
⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → ((∏t‘(𝐴 × {𝑅})) ↾t (𝒫 𝐴 Cn 𝑅)) = ((∏t‘(𝐴 × {𝑅})) ↾t ∪ (∏t‘(𝐴 × {𝑅})))) |
131 | | eqid 2622 |
. . . . . 6
⊢ ∪ (∏t‘(𝐴 × {𝑅})) = ∪
(∏t‘(𝐴 × {𝑅})) |
132 | 131 | restid 16094 |
. . . . 5
⊢
((∏t‘(𝐴 × {𝑅})) ∈ Top →
((∏t‘(𝐴 × {𝑅})) ↾t ∪ (∏t‘(𝐴 × {𝑅}))) = (∏t‘(𝐴 × {𝑅}))) |
133 | 14, 132 | syl 17 |
. . . 4
⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → ((∏t‘(𝐴 × {𝑅})) ↾t ∪ (∏t‘(𝐴 × {𝑅}))) = (∏t‘(𝐴 × {𝑅}))) |
134 | 130, 133 | eqtrd 2656 |
. . 3
⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → ((∏t‘(𝐴 × {𝑅})) ↾t (𝒫 𝐴 Cn 𝑅)) = (∏t‘(𝐴 × {𝑅}))) |
135 | 5, 126 | xkoptsub 21457 |
. . . 4
⊢
((𝒫 𝐴 ∈
Top ∧ 𝑅 ∈ Top)
→ ((∏t‘(𝐴 × {𝑅})) ↾t (𝒫 𝐴 Cn 𝑅)) ⊆ (𝑅 ^ko 𝒫 𝐴)) |
136 | 2, 3, 135 | syl2anc 693 |
. . 3
⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → ((∏t‘(𝐴 × {𝑅})) ↾t (𝒫 𝐴 Cn 𝑅)) ⊆ (𝑅 ^ko 𝒫 𝐴)) |
137 | 134, 136 | eqsstr3d 3640 |
. 2
⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (∏t‘(𝐴 × {𝑅})) ⊆ (𝑅 ^ko 𝒫 𝐴)) |
138 | 125, 137 | eqssd 3620 |
1
⊢ ((𝑅 ∈ Top ∧ 𝐴 ∈ 𝑉) → (𝑅 ^ko 𝒫 𝐴) =
(∏t‘(𝐴 × {𝑅}))) |