MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xkopt Structured version   Visualization version   GIF version

Theorem xkopt 21668
Description: The compact-open topology on a discrete set coincides with the product topology where all the factors are the same. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 12-Sep-2015.)
Assertion
Ref Expression
xkopt ((𝑅 ∈ Top ∧ 𝐴𝑉) → (𝑅 ^ko 𝒫 𝐴) = (∏t‘(𝐴 × {𝑅})))

Proof of Theorem xkopt
Dummy variables 𝑓 𝑘 𝑣 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 distop 21009 . . . . 5 (𝐴𝑉 → 𝒫 𝐴 ∈ Top)
21adantl 469 . . . 4 ((𝑅 ∈ Top ∧ 𝐴𝑉) → 𝒫 𝐴 ∈ Top)
3 simpl 470 . . . 4 ((𝑅 ∈ Top ∧ 𝐴𝑉) → 𝑅 ∈ Top)
4 unipw 5105 . . . . . 6 𝒫 𝐴 = 𝐴
54eqcomi 2814 . . . . 5 𝐴 = 𝒫 𝐴
6 eqid 2805 . . . . 5 {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴t 𝑥) ∈ Comp} = {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴t 𝑥) ∈ Comp}
7 eqid 2805 . . . . 5 (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴t 𝑥) ∈ Comp}, 𝑣𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓𝑘) ⊆ 𝑣}) = (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴t 𝑥) ∈ Comp}, 𝑣𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓𝑘) ⊆ 𝑣})
85, 6, 7xkoval 21600 . . . 4 ((𝒫 𝐴 ∈ Top ∧ 𝑅 ∈ Top) → (𝑅 ^ko 𝒫 𝐴) = (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴t 𝑥) ∈ Comp}, 𝑣𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓𝑘) ⊆ 𝑣}))))
92, 3, 8syl2anc 575 . . 3 ((𝑅 ∈ Top ∧ 𝐴𝑉) → (𝑅 ^ko 𝒫 𝐴) = (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴t 𝑥) ∈ Comp}, 𝑣𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓𝑘) ⊆ 𝑣}))))
10 simpr 473 . . . . 5 ((𝑅 ∈ Top ∧ 𝐴𝑉) → 𝐴𝑉)
11 fconst6g 6306 . . . . . 6 (𝑅 ∈ Top → (𝐴 × {𝑅}):𝐴⟶Top)
1211adantr 468 . . . . 5 ((𝑅 ∈ Top ∧ 𝐴𝑉) → (𝐴 × {𝑅}):𝐴⟶Top)
13 pttop 21595 . . . . 5 ((𝐴𝑉 ∧ (𝐴 × {𝑅}):𝐴⟶Top) → (∏t‘(𝐴 × {𝑅})) ∈ Top)
1410, 12, 13syl2anc 575 . . . 4 ((𝑅 ∈ Top ∧ 𝐴𝑉) → (∏t‘(𝐴 × {𝑅})) ∈ Top)
15 elpwi 4358 . . . . . . . . . . . . . 14 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
16 restdis 21192 . . . . . . . . . . . . . 14 ((𝐴𝑉𝑥𝐴) → (𝒫 𝐴t 𝑥) = 𝒫 𝑥)
1715, 16sylan2 582 . . . . . . . . . . . . 13 ((𝐴𝑉𝑥 ∈ 𝒫 𝐴) → (𝒫 𝐴t 𝑥) = 𝒫 𝑥)
1817adantll 696 . . . . . . . . . . . 12 (((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ 𝑥 ∈ 𝒫 𝐴) → (𝒫 𝐴t 𝑥) = 𝒫 𝑥)
1918eleq1d 2869 . . . . . . . . . . 11 (((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ 𝑥 ∈ 𝒫 𝐴) → ((𝒫 𝐴t 𝑥) ∈ Comp ↔ 𝒫 𝑥 ∈ Comp))
20 discmp 21411 . . . . . . . . . . 11 (𝑥 ∈ Fin ↔ 𝒫 𝑥 ∈ Comp)
2119, 20syl6bbr 280 . . . . . . . . . 10 (((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ 𝑥 ∈ 𝒫 𝐴) → ((𝒫 𝐴t 𝑥) ∈ Comp ↔ 𝑥 ∈ Fin))
2221rabbidva 3377 . . . . . . . . 9 ((𝑅 ∈ Top ∧ 𝐴𝑉) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴t 𝑥) ∈ Comp} = {𝑥 ∈ 𝒫 𝐴𝑥 ∈ Fin})
23 dfin5 3774 . . . . . . . . 9 (𝒫 𝐴 ∩ Fin) = {𝑥 ∈ 𝒫 𝐴𝑥 ∈ Fin}
2422, 23syl6eqr 2857 . . . . . . . 8 ((𝑅 ∈ Top ∧ 𝐴𝑉) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴t 𝑥) ∈ Comp} = (𝒫 𝐴 ∩ Fin))
25 eqidd 2806 . . . . . . . 8 ((𝑅 ∈ Top ∧ 𝐴𝑉) → 𝑅 = 𝑅)
26 eqid 2805 . . . . . . . . . . 11 𝑅 = 𝑅
2726toptopon 20931 . . . . . . . . . 10 (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘ 𝑅))
28 cndis 21305 . . . . . . . . . . 11 ((𝐴𝑉𝑅 ∈ (TopOn‘ 𝑅)) → (𝒫 𝐴 Cn 𝑅) = ( 𝑅𝑚 𝐴))
2928ancoms 448 . . . . . . . . . 10 ((𝑅 ∈ (TopOn‘ 𝑅) ∧ 𝐴𝑉) → (𝒫 𝐴 Cn 𝑅) = ( 𝑅𝑚 𝐴))
3027, 29sylanb 572 . . . . . . . . 9 ((𝑅 ∈ Top ∧ 𝐴𝑉) → (𝒫 𝐴 Cn 𝑅) = ( 𝑅𝑚 𝐴))
31 rabeq 3381 . . . . . . . . 9 ((𝒫 𝐴 Cn 𝑅) = ( 𝑅𝑚 𝐴) → {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓𝑘) ⊆ 𝑣} = {𝑓 ∈ ( 𝑅𝑚 𝐴) ∣ (𝑓𝑘) ⊆ 𝑣})
3230, 31syl 17 . . . . . . . 8 ((𝑅 ∈ Top ∧ 𝐴𝑉) → {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓𝑘) ⊆ 𝑣} = {𝑓 ∈ ( 𝑅𝑚 𝐴) ∣ (𝑓𝑘) ⊆ 𝑣})
3324, 25, 32mpt2eq123dv 6944 . . . . . . 7 ((𝑅 ∈ Top ∧ 𝐴𝑉) → (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴t 𝑥) ∈ Comp}, 𝑣𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓𝑘) ⊆ 𝑣}) = (𝑘 ∈ (𝒫 𝐴 ∩ Fin), 𝑣𝑅 ↦ {𝑓 ∈ ( 𝑅𝑚 𝐴) ∣ (𝑓𝑘) ⊆ 𝑣}))
3433rneqd 5551 . . . . . 6 ((𝑅 ∈ Top ∧ 𝐴𝑉) → ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴t 𝑥) ∈ Comp}, 𝑣𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓𝑘) ⊆ 𝑣}) = ran (𝑘 ∈ (𝒫 𝐴 ∩ Fin), 𝑣𝑅 ↦ {𝑓 ∈ ( 𝑅𝑚 𝐴) ∣ (𝑓𝑘) ⊆ 𝑣}))
35 eqid 2805 . . . . . . 7 (𝑘 ∈ (𝒫 𝐴 ∩ Fin), 𝑣𝑅 ↦ {𝑓 ∈ ( 𝑅𝑚 𝐴) ∣ (𝑓𝑘) ⊆ 𝑣}) = (𝑘 ∈ (𝒫 𝐴 ∩ Fin), 𝑣𝑅 ↦ {𝑓 ∈ ( 𝑅𝑚 𝐴) ∣ (𝑓𝑘) ⊆ 𝑣})
3635rnmpt2 6997 . . . . . 6 ran (𝑘 ∈ (𝒫 𝐴 ∩ Fin), 𝑣𝑅 ↦ {𝑓 ∈ ( 𝑅𝑚 𝐴) ∣ (𝑓𝑘) ⊆ 𝑣}) = {𝑥 ∣ ∃𝑘 ∈ (𝒫 𝐴 ∩ Fin)∃𝑣𝑅 𝑥 = {𝑓 ∈ ( 𝑅𝑚 𝐴) ∣ (𝑓𝑘) ⊆ 𝑣}}
3734, 36syl6eq 2855 . . . . 5 ((𝑅 ∈ Top ∧ 𝐴𝑉) → ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴t 𝑥) ∈ Comp}, 𝑣𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓𝑘) ⊆ 𝑣}) = {𝑥 ∣ ∃𝑘 ∈ (𝒫 𝐴 ∩ Fin)∃𝑣𝑅 𝑥 = {𝑓 ∈ ( 𝑅𝑚 𝐴) ∣ (𝑓𝑘) ⊆ 𝑣}})
38 elmapi 8111 . . . . . . . . . . . 12 (𝑓 ∈ ( 𝑅𝑚 𝐴) → 𝑓:𝐴 𝑅)
39 eleq2 2873 . . . . . . . . . . . . . . . . 17 (𝑣 = if(𝑥𝑘, 𝑣, 𝑅) → ((𝑓𝑥) ∈ 𝑣 ↔ (𝑓𝑥) ∈ if(𝑥𝑘, 𝑣, 𝑅)))
4039imbi2d 331 . . . . . . . . . . . . . . . 16 (𝑣 = if(𝑥𝑘, 𝑣, 𝑅) → ((𝑥𝐴 → (𝑓𝑥) ∈ 𝑣) ↔ (𝑥𝐴 → (𝑓𝑥) ∈ if(𝑥𝑘, 𝑣, 𝑅))))
4140bibi1d 334 . . . . . . . . . . . . . . 15 (𝑣 = if(𝑥𝑘, 𝑣, 𝑅) → (((𝑥𝐴 → (𝑓𝑥) ∈ 𝑣) ↔ (𝑥𝑘 → (𝑓𝑥) ∈ 𝑣)) ↔ ((𝑥𝐴 → (𝑓𝑥) ∈ if(𝑥𝑘, 𝑣, 𝑅)) ↔ (𝑥𝑘 → (𝑓𝑥) ∈ 𝑣))))
42 eleq2 2873 . . . . . . . . . . . . . . . . 17 ( 𝑅 = if(𝑥𝑘, 𝑣, 𝑅) → ((𝑓𝑥) ∈ 𝑅 ↔ (𝑓𝑥) ∈ if(𝑥𝑘, 𝑣, 𝑅)))
4342imbi2d 331 . . . . . . . . . . . . . . . 16 ( 𝑅 = if(𝑥𝑘, 𝑣, 𝑅) → ((𝑥𝐴 → (𝑓𝑥) ∈ 𝑅) ↔ (𝑥𝐴 → (𝑓𝑥) ∈ if(𝑥𝑘, 𝑣, 𝑅))))
4443bibi1d 334 . . . . . . . . . . . . . . 15 ( 𝑅 = if(𝑥𝑘, 𝑣, 𝑅) → (((𝑥𝐴 → (𝑓𝑥) ∈ 𝑅) ↔ (𝑥𝑘 → (𝑓𝑥) ∈ 𝑣)) ↔ ((𝑥𝐴 → (𝑓𝑥) ∈ if(𝑥𝑘, 𝑣, 𝑅)) ↔ (𝑥𝑘 → (𝑓𝑥) ∈ 𝑣))))
45 inss1 4026 . . . . . . . . . . . . . . . . . . . . 21 (𝒫 𝐴 ∩ Fin) ⊆ 𝒫 𝐴
46 simprl 778 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) → 𝑘 ∈ (𝒫 𝐴 ∩ Fin))
4745, 46sseldi 3793 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) → 𝑘 ∈ 𝒫 𝐴)
4847elpwid 4360 . . . . . . . . . . . . . . . . . . 19 (((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) → 𝑘𝐴)
4948adantr 468 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) ∧ 𝑓:𝐴 𝑅) → 𝑘𝐴)
5049sselda 3795 . . . . . . . . . . . . . . . . 17 (((((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) ∧ 𝑓:𝐴 𝑅) ∧ 𝑥𝑘) → 𝑥𝐴)
51 simpr 473 . . . . . . . . . . . . . . . . 17 (((((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) ∧ 𝑓:𝐴 𝑅) ∧ 𝑥𝑘) → 𝑥𝑘)
5250, 512thd 256 . . . . . . . . . . . . . . . 16 (((((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) ∧ 𝑓:𝐴 𝑅) ∧ 𝑥𝑘) → (𝑥𝐴𝑥𝑘))
5352imbi1d 332 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) ∧ 𝑓:𝐴 𝑅) ∧ 𝑥𝑘) → ((𝑥𝐴 → (𝑓𝑥) ∈ 𝑣) ↔ (𝑥𝑘 → (𝑓𝑥) ∈ 𝑣)))
54 ffvelrn 6576 . . . . . . . . . . . . . . . . . . 19 ((𝑓:𝐴 𝑅𝑥𝐴) → (𝑓𝑥) ∈ 𝑅)
5554ex 399 . . . . . . . . . . . . . . . . . 18 (𝑓:𝐴 𝑅 → (𝑥𝐴 → (𝑓𝑥) ∈ 𝑅))
5655adantl 469 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) ∧ 𝑓:𝐴 𝑅) → (𝑥𝐴 → (𝑓𝑥) ∈ 𝑅))
5756adantr 468 . . . . . . . . . . . . . . . 16 (((((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) ∧ 𝑓:𝐴 𝑅) ∧ ¬ 𝑥𝑘) → (𝑥𝐴 → (𝑓𝑥) ∈ 𝑅))
58 pm2.21 121 . . . . . . . . . . . . . . . . 17 𝑥𝑘 → (𝑥𝑘 → (𝑓𝑥) ∈ 𝑣))
5958adantl 469 . . . . . . . . . . . . . . . 16 (((((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) ∧ 𝑓:𝐴 𝑅) ∧ ¬ 𝑥𝑘) → (𝑥𝑘 → (𝑓𝑥) ∈ 𝑣))
6057, 592thd 256 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) ∧ 𝑓:𝐴 𝑅) ∧ ¬ 𝑥𝑘) → ((𝑥𝐴 → (𝑓𝑥) ∈ 𝑅) ↔ (𝑥𝑘 → (𝑓𝑥) ∈ 𝑣)))
6141, 44, 53, 60ifbothda 4313 . . . . . . . . . . . . . 14 ((((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) ∧ 𝑓:𝐴 𝑅) → ((𝑥𝐴 → (𝑓𝑥) ∈ if(𝑥𝑘, 𝑣, 𝑅)) ↔ (𝑥𝑘 → (𝑓𝑥) ∈ 𝑣)))
6261ralbidv2 3171 . . . . . . . . . . . . 13 ((((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) ∧ 𝑓:𝐴 𝑅) → (∀𝑥𝐴 (𝑓𝑥) ∈ if(𝑥𝑘, 𝑣, 𝑅) ↔ ∀𝑥𝑘 (𝑓𝑥) ∈ 𝑣))
63 ffn 6253 . . . . . . . . . . . . . . 15 (𝑓:𝐴 𝑅𝑓 Fn 𝐴)
6463adantl 469 . . . . . . . . . . . . . 14 ((((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) ∧ 𝑓:𝐴 𝑅) → 𝑓 Fn 𝐴)
65 vex 3393 . . . . . . . . . . . . . . . 16 𝑓 ∈ V
6665elixp 8149 . . . . . . . . . . . . . . 15 (𝑓X𝑥𝐴 if(𝑥𝑘, 𝑣, 𝑅) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑥𝐴 (𝑓𝑥) ∈ if(𝑥𝑘, 𝑣, 𝑅)))
6766baib 527 . . . . . . . . . . . . . 14 (𝑓 Fn 𝐴 → (𝑓X𝑥𝐴 if(𝑥𝑘, 𝑣, 𝑅) ↔ ∀𝑥𝐴 (𝑓𝑥) ∈ if(𝑥𝑘, 𝑣, 𝑅)))
6864, 67syl 17 . . . . . . . . . . . . 13 ((((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) ∧ 𝑓:𝐴 𝑅) → (𝑓X𝑥𝐴 if(𝑥𝑘, 𝑣, 𝑅) ↔ ∀𝑥𝐴 (𝑓𝑥) ∈ if(𝑥𝑘, 𝑣, 𝑅)))
69 ffun 6256 . . . . . . . . . . . . . . 15 (𝑓:𝐴 𝑅 → Fun 𝑓)
7069adantl 469 . . . . . . . . . . . . . 14 ((((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) ∧ 𝑓:𝐴 𝑅) → Fun 𝑓)
71 fdm 6261 . . . . . . . . . . . . . . . 16 (𝑓:𝐴 𝑅 → dom 𝑓 = 𝐴)
7271adantl 469 . . . . . . . . . . . . . . 15 ((((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) ∧ 𝑓:𝐴 𝑅) → dom 𝑓 = 𝐴)
7349, 72sseqtr4d 3836 . . . . . . . . . . . . . 14 ((((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) ∧ 𝑓:𝐴 𝑅) → 𝑘 ⊆ dom 𝑓)
74 funimass4 6465 . . . . . . . . . . . . . 14 ((Fun 𝑓𝑘 ⊆ dom 𝑓) → ((𝑓𝑘) ⊆ 𝑣 ↔ ∀𝑥𝑘 (𝑓𝑥) ∈ 𝑣))
7570, 73, 74syl2anc 575 . . . . . . . . . . . . 13 ((((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) ∧ 𝑓:𝐴 𝑅) → ((𝑓𝑘) ⊆ 𝑣 ↔ ∀𝑥𝑘 (𝑓𝑥) ∈ 𝑣))
7662, 68, 753bitr4d 302 . . . . . . . . . . . 12 ((((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) ∧ 𝑓:𝐴 𝑅) → (𝑓X𝑥𝐴 if(𝑥𝑘, 𝑣, 𝑅) ↔ (𝑓𝑘) ⊆ 𝑣))
7738, 76sylan2 582 . . . . . . . . . . 11 ((((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) ∧ 𝑓 ∈ ( 𝑅𝑚 𝐴)) → (𝑓X𝑥𝐴 if(𝑥𝑘, 𝑣, 𝑅) ↔ (𝑓𝑘) ⊆ 𝑣))
7877rabbi2dva 4015 . . . . . . . . . 10 (((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) → (( 𝑅𝑚 𝐴) ∩ X𝑥𝐴 if(𝑥𝑘, 𝑣, 𝑅)) = {𝑓 ∈ ( 𝑅𝑚 𝐴) ∣ (𝑓𝑘) ⊆ 𝑣})
79 elssuni 4657 . . . . . . . . . . . . . . . 16 (𝑣𝑅𝑣 𝑅)
8079ad2antll 711 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) → 𝑣 𝑅)
81 ssid 3817 . . . . . . . . . . . . . . 15 𝑅 𝑅
82 sseq1 3820 . . . . . . . . . . . . . . . 16 (𝑣 = if(𝑥𝑘, 𝑣, 𝑅) → (𝑣 𝑅 ↔ if(𝑥𝑘, 𝑣, 𝑅) ⊆ 𝑅))
83 sseq1 3820 . . . . . . . . . . . . . . . 16 ( 𝑅 = if(𝑥𝑘, 𝑣, 𝑅) → ( 𝑅 𝑅 ↔ if(𝑥𝑘, 𝑣, 𝑅) ⊆ 𝑅))
8482, 83ifboth 4314 . . . . . . . . . . . . . . 15 ((𝑣 𝑅 𝑅 𝑅) → if(𝑥𝑘, 𝑣, 𝑅) ⊆ 𝑅)
8580, 81, 84sylancl 576 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) → if(𝑥𝑘, 𝑣, 𝑅) ⊆ 𝑅)
8685ralrimivw 3154 . . . . . . . . . . . . 13 (((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) → ∀𝑥𝐴 if(𝑥𝑘, 𝑣, 𝑅) ⊆ 𝑅)
87 ss2ixp 8155 . . . . . . . . . . . . 13 (∀𝑥𝐴 if(𝑥𝑘, 𝑣, 𝑅) ⊆ 𝑅X𝑥𝐴 if(𝑥𝑘, 𝑣, 𝑅) ⊆ X𝑥𝐴 𝑅)
8886, 87syl 17 . . . . . . . . . . . 12 (((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) → X𝑥𝐴 if(𝑥𝑘, 𝑣, 𝑅) ⊆ X𝑥𝐴 𝑅)
89 simplr 776 . . . . . . . . . . . . 13 (((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) → 𝐴𝑉)
90 uniexg 7182 . . . . . . . . . . . . . 14 (𝑅 ∈ Top → 𝑅 ∈ V)
9190ad2antrr 708 . . . . . . . . . . . . 13 (((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) → 𝑅 ∈ V)
92 ixpconstg 8151 . . . . . . . . . . . . 13 ((𝐴𝑉 𝑅 ∈ V) → X𝑥𝐴 𝑅 = ( 𝑅𝑚 𝐴))
9389, 91, 92syl2anc 575 . . . . . . . . . . . 12 (((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) → X𝑥𝐴 𝑅 = ( 𝑅𝑚 𝐴))
9488, 93sseqtrd 3835 . . . . . . . . . . 11 (((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) → X𝑥𝐴 if(𝑥𝑘, 𝑣, 𝑅) ⊆ ( 𝑅𝑚 𝐴))
95 sseqin2 4013 . . . . . . . . . . 11 (X𝑥𝐴 if(𝑥𝑘, 𝑣, 𝑅) ⊆ ( 𝑅𝑚 𝐴) ↔ (( 𝑅𝑚 𝐴) ∩ X𝑥𝐴 if(𝑥𝑘, 𝑣, 𝑅)) = X𝑥𝐴 if(𝑥𝑘, 𝑣, 𝑅))
9694, 95sylib 209 . . . . . . . . . 10 (((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) → (( 𝑅𝑚 𝐴) ∩ X𝑥𝐴 if(𝑥𝑘, 𝑣, 𝑅)) = X𝑥𝐴 if(𝑥𝑘, 𝑣, 𝑅))
9778, 96eqtr3d 2841 . . . . . . . . 9 (((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) → {𝑓 ∈ ( 𝑅𝑚 𝐴) ∣ (𝑓𝑘) ⊆ 𝑣} = X𝑥𝐴 if(𝑥𝑘, 𝑣, 𝑅))
9811ad2antrr 708 . . . . . . . . . 10 (((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) → (𝐴 × {𝑅}):𝐴⟶Top)
99 inss2 4027 . . . . . . . . . . 11 (𝒫 𝐴 ∩ Fin) ⊆ Fin
10099, 46sseldi 3793 . . . . . . . . . 10 (((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) → 𝑘 ∈ Fin)
101 simplrr 787 . . . . . . . . . . . 12 ((((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) ∧ 𝑥𝐴) → 𝑣𝑅)
10226topopn 20920 . . . . . . . . . . . . 13 (𝑅 ∈ Top → 𝑅𝑅)
103102ad3antrrr 712 . . . . . . . . . . . 12 ((((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) ∧ 𝑥𝐴) → 𝑅𝑅)
104101, 103ifcld 4321 . . . . . . . . . . 11 ((((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) ∧ 𝑥𝐴) → if(𝑥𝑘, 𝑣, 𝑅) ∈ 𝑅)
105 simpll 774 . . . . . . . . . . . 12 (((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) → 𝑅 ∈ Top)
106 fvconst2g 6689 . . . . . . . . . . . 12 ((𝑅 ∈ Top ∧ 𝑥𝐴) → ((𝐴 × {𝑅})‘𝑥) = 𝑅)
107105, 106sylan 571 . . . . . . . . . . 11 ((((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) ∧ 𝑥𝐴) → ((𝐴 × {𝑅})‘𝑥) = 𝑅)
108104, 107eleqtrrd 2887 . . . . . . . . . 10 ((((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) ∧ 𝑥𝐴) → if(𝑥𝑘, 𝑣, 𝑅) ∈ ((𝐴 × {𝑅})‘𝑥))
109 eldifn 3929 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴𝑘) → ¬ 𝑥𝑘)
110109iffalsed 4287 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴𝑘) → if(𝑥𝑘, 𝑣, 𝑅) = 𝑅)
111110adantl 469 . . . . . . . . . . 11 ((((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) ∧ 𝑥 ∈ (𝐴𝑘)) → if(𝑥𝑘, 𝑣, 𝑅) = 𝑅)
112 eldifi 3928 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴𝑘) → 𝑥𝐴)
113112, 107sylan2 582 . . . . . . . . . . . 12 ((((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) ∧ 𝑥 ∈ (𝐴𝑘)) → ((𝐴 × {𝑅})‘𝑥) = 𝑅)
114113unieqd 4636 . . . . . . . . . . 11 ((((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) ∧ 𝑥 ∈ (𝐴𝑘)) → ((𝐴 × {𝑅})‘𝑥) = 𝑅)
115111, 114eqtr4d 2842 . . . . . . . . . 10 ((((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) ∧ 𝑥 ∈ (𝐴𝑘)) → if(𝑥𝑘, 𝑣, 𝑅) = ((𝐴 × {𝑅})‘𝑥))
11689, 98, 100, 108, 115ptopn 21596 . . . . . . . . 9 (((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) → X𝑥𝐴 if(𝑥𝑘, 𝑣, 𝑅) ∈ (∏t‘(𝐴 × {𝑅})))
11797, 116eqeltrd 2884 . . . . . . . 8 (((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) → {𝑓 ∈ ( 𝑅𝑚 𝐴) ∣ (𝑓𝑘) ⊆ 𝑣} ∈ (∏t‘(𝐴 × {𝑅})))
118 eleq1 2872 . . . . . . . 8 (𝑥 = {𝑓 ∈ ( 𝑅𝑚 𝐴) ∣ (𝑓𝑘) ⊆ 𝑣} → (𝑥 ∈ (∏t‘(𝐴 × {𝑅})) ↔ {𝑓 ∈ ( 𝑅𝑚 𝐴) ∣ (𝑓𝑘) ⊆ 𝑣} ∈ (∏t‘(𝐴 × {𝑅}))))
119117, 118syl5ibrcom 238 . . . . . . 7 (((𝑅 ∈ Top ∧ 𝐴𝑉) ∧ (𝑘 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑣𝑅)) → (𝑥 = {𝑓 ∈ ( 𝑅𝑚 𝐴) ∣ (𝑓𝑘) ⊆ 𝑣} → 𝑥 ∈ (∏t‘(𝐴 × {𝑅}))))
120119rexlimdvva 3225 . . . . . 6 ((𝑅 ∈ Top ∧ 𝐴𝑉) → (∃𝑘 ∈ (𝒫 𝐴 ∩ Fin)∃𝑣𝑅 𝑥 = {𝑓 ∈ ( 𝑅𝑚 𝐴) ∣ (𝑓𝑘) ⊆ 𝑣} → 𝑥 ∈ (∏t‘(𝐴 × {𝑅}))))
121120abssdv 3870 . . . . 5 ((𝑅 ∈ Top ∧ 𝐴𝑉) → {𝑥 ∣ ∃𝑘 ∈ (𝒫 𝐴 ∩ Fin)∃𝑣𝑅 𝑥 = {𝑓 ∈ ( 𝑅𝑚 𝐴) ∣ (𝑓𝑘) ⊆ 𝑣}} ⊆ (∏t‘(𝐴 × {𝑅})))
12237, 121eqsstrd 3833 . . . 4 ((𝑅 ∈ Top ∧ 𝐴𝑉) → ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴t 𝑥) ∈ Comp}, 𝑣𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓𝑘) ⊆ 𝑣}) ⊆ (∏t‘(𝐴 × {𝑅})))
123 tgfiss 21005 . . . 4 (((∏t‘(𝐴 × {𝑅})) ∈ Top ∧ ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴t 𝑥) ∈ Comp}, 𝑣𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓𝑘) ⊆ 𝑣}) ⊆ (∏t‘(𝐴 × {𝑅}))) → (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴t 𝑥) ∈ Comp}, 𝑣𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓𝑘) ⊆ 𝑣}))) ⊆ (∏t‘(𝐴 × {𝑅})))
12414, 122, 123syl2anc 575 . . 3 ((𝑅 ∈ Top ∧ 𝐴𝑉) → (topGen‘(fi‘ran (𝑘 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝒫 𝐴t 𝑥) ∈ Comp}, 𝑣𝑅 ↦ {𝑓 ∈ (𝒫 𝐴 Cn 𝑅) ∣ (𝑓𝑘) ⊆ 𝑣}))) ⊆ (∏t‘(𝐴 × {𝑅})))
1259, 124eqsstrd 3833 . 2 ((𝑅 ∈ Top ∧ 𝐴𝑉) → (𝑅 ^ko 𝒫 𝐴) ⊆ (∏t‘(𝐴 × {𝑅})))
126 eqid 2805 . . . . . . . 8 (∏t‘(𝐴 × {𝑅})) = (∏t‘(𝐴 × {𝑅}))
127126, 26ptuniconst 21611 . . . . . . 7 ((𝐴𝑉𝑅 ∈ Top) → ( 𝑅𝑚 𝐴) = (∏t‘(𝐴 × {𝑅})))
128127ancoms 448 . . . . . 6 ((𝑅 ∈ Top ∧ 𝐴𝑉) → ( 𝑅𝑚 𝐴) = (∏t‘(𝐴 × {𝑅})))
12930, 128eqtrd 2839 . . . . 5 ((𝑅 ∈ Top ∧ 𝐴𝑉) → (𝒫 𝐴 Cn 𝑅) = (∏t‘(𝐴 × {𝑅})))
130129oveq2d 6887 . . . 4 ((𝑅 ∈ Top ∧ 𝐴𝑉) → ((∏t‘(𝐴 × {𝑅})) ↾t (𝒫 𝐴 Cn 𝑅)) = ((∏t‘(𝐴 × {𝑅})) ↾t (∏t‘(𝐴 × {𝑅}))))
131 eqid 2805 . . . . . 6 (∏t‘(𝐴 × {𝑅})) = (∏t‘(𝐴 × {𝑅}))
132131restid 16295 . . . . 5 ((∏t‘(𝐴 × {𝑅})) ∈ Top → ((∏t‘(𝐴 × {𝑅})) ↾t (∏t‘(𝐴 × {𝑅}))) = (∏t‘(𝐴 × {𝑅})))
13314, 132syl 17 . . . 4 ((𝑅 ∈ Top ∧ 𝐴𝑉) → ((∏t‘(𝐴 × {𝑅})) ↾t (∏t‘(𝐴 × {𝑅}))) = (∏t‘(𝐴 × {𝑅})))
134130, 133eqtrd 2839 . . 3 ((𝑅 ∈ Top ∧ 𝐴𝑉) → ((∏t‘(𝐴 × {𝑅})) ↾t (𝒫 𝐴 Cn 𝑅)) = (∏t‘(𝐴 × {𝑅})))
1355, 126xkoptsub 21667 . . . 4 ((𝒫 𝐴 ∈ Top ∧ 𝑅 ∈ Top) → ((∏t‘(𝐴 × {𝑅})) ↾t (𝒫 𝐴 Cn 𝑅)) ⊆ (𝑅 ^ko 𝒫 𝐴))
1362, 3, 135syl2anc 575 . . 3 ((𝑅 ∈ Top ∧ 𝐴𝑉) → ((∏t‘(𝐴 × {𝑅})) ↾t (𝒫 𝐴 Cn 𝑅)) ⊆ (𝑅 ^ko 𝒫 𝐴))
137134, 136eqsstr3d 3834 . 2 ((𝑅 ∈ Top ∧ 𝐴𝑉) → (∏t‘(𝐴 × {𝑅})) ⊆ (𝑅 ^ko 𝒫 𝐴))
138125, 137eqssd 3812 1 ((𝑅 ∈ Top ∧ 𝐴𝑉) → (𝑅 ^ko 𝒫 𝐴) = (∏t‘(𝐴 × {𝑅})))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384   = wceq 1637  wcel 2158  {cab 2791  wral 3095  wrex 3096  {crab 3099  Vcvv 3390  cdif 3763  cin 3765  wss 3766  ifcif 4276  𝒫 cpw 4348  {csn 4367   cuni 4626   × cxp 5306  dom cdm 5308  ran crn 5309  cima 5311  Fun wfun 6092   Fn wfn 6093  wf 6094  cfv 6098  (class class class)co 6871  cmpt2 6873  𝑚 cmap 8089  Xcixp 8142  Fincfn 8189  ficfi 8552  t crest 16282  topGenctg 16299  tcpt 16300  Topctop 20907  TopOnctopon 20924   Cn ccn 21238  Compccmp 21399   ^ko cxko 21574
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-8 2160  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784  ax-rep 4960  ax-sep 4971  ax-nul 4980  ax-pow 5032  ax-pr 5093  ax-un 7176
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-eu 2636  df-mo 2637  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-ne 2978  df-ral 3100  df-rex 3101  df-reu 3102  df-rab 3104  df-v 3392  df-sbc 3631  df-csb 3726  df-dif 3769  df-un 3771  df-in 3773  df-ss 3780  df-pss 3782  df-nul 4114  df-if 4277  df-pw 4350  df-sn 4368  df-pr 4370  df-tp 4372  df-op 4374  df-uni 4627  df-int 4666  df-iun 4710  df-iin 4711  df-br 4841  df-opab 4903  df-mpt 4920  df-tr 4943  df-id 5216  df-eprel 5221  df-po 5229  df-so 5230  df-fr 5267  df-we 5269  df-xp 5314  df-rel 5315  df-cnv 5316  df-co 5317  df-dm 5318  df-rn 5319  df-res 5320  df-ima 5321  df-pred 5890  df-ord 5936  df-on 5937  df-lim 5938  df-suc 5939  df-iota 6061  df-fun 6100  df-fn 6101  df-f 6102  df-f1 6103  df-fo 6104  df-f1o 6105  df-fv 6106  df-ov 6874  df-oprab 6875  df-mpt2 6876  df-om 7293  df-1st 7395  df-2nd 7396  df-wrecs 7639  df-recs 7701  df-rdg 7739  df-1o 7793  df-2o 7794  df-oadd 7797  df-er 7976  df-map 8091  df-ixp 8143  df-en 8190  df-dom 8191  df-sdom 8192  df-fin 8193  df-fi 8553  df-rest 16284  df-topgen 16305  df-pt 16306  df-top 20908  df-topon 20925  df-bases 20960  df-cn 21241  df-cmp 21400  df-xko 21576
This theorem is referenced by:  tmdgsum  22108  tmdgsum2  22109  symgtgp  22114
  Copyright terms: Public domain W3C validator