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

Theorem xkoco1cn 21370
 Description: If 𝐹 is a continuous function, then 𝑔 ↦ 𝑔 ∘ 𝐹 is a continuous function on function spaces. (The reason we prove this and xkoco2cn 21371 independently of the more general xkococn 21373 is because that requires some inconvenient extra assumptions on 𝑆.) (Contributed by Mario Carneiro, 20-Mar-2015.)
Hypotheses
Ref Expression
xkoco1cn.t (𝜑𝑇 ∈ Top)
xkoco1cn.f (𝜑𝐹 ∈ (𝑅 Cn 𝑆))
Assertion
Ref Expression
xkoco1cn (𝜑 → (𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔𝐹)) ∈ ((𝑇 ^ko 𝑆) Cn (𝑇 ^ko 𝑅)))
Distinct variable groups:   𝜑,𝑔   𝑅,𝑔   𝑆,𝑔   𝑇,𝑔   𝑔,𝐹

Proof of Theorem xkoco1cn
Dummy variables 𝑘 𝑣 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xkoco1cn.f . . . 4 (𝜑𝐹 ∈ (𝑅 Cn 𝑆))
2 cnco 20980 . . . 4 ((𝐹 ∈ (𝑅 Cn 𝑆) ∧ 𝑔 ∈ (𝑆 Cn 𝑇)) → (𝑔𝐹) ∈ (𝑅 Cn 𝑇))
31, 2sylan 488 . . 3 ((𝜑𝑔 ∈ (𝑆 Cn 𝑇)) → (𝑔𝐹) ∈ (𝑅 Cn 𝑇))
4 eqid 2621 . . 3 (𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔𝐹)) = (𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔𝐹))
53, 4fmptd 6340 . 2 (𝜑 → (𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔𝐹)):(𝑆 Cn 𝑇)⟶(𝑅 Cn 𝑇))
6 eqid 2621 . . . . . 6 𝑅 = 𝑅
7 eqid 2621 . . . . . 6 {𝑦 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑦) ∈ Comp} = {𝑦 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑦) ∈ Comp}
8 eqid 2621 . . . . . 6 (𝑘 ∈ {𝑦 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑦) ∈ Comp}, 𝑣𝑇 ↦ { ∈ (𝑅 Cn 𝑇) ∣ (𝑘) ⊆ 𝑣}) = (𝑘 ∈ {𝑦 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑦) ∈ Comp}, 𝑣𝑇 ↦ { ∈ (𝑅 Cn 𝑇) ∣ (𝑘) ⊆ 𝑣})
96, 7, 8xkobval 21299 . . . . 5 ran (𝑘 ∈ {𝑦 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑦) ∈ Comp}, 𝑣𝑇 ↦ { ∈ (𝑅 Cn 𝑇) ∣ (𝑘) ⊆ 𝑣}) = {𝑥 ∣ ∃𝑘 ∈ 𝒫 𝑅𝑣𝑇 ((𝑅t 𝑘) ∈ Comp ∧ 𝑥 = { ∈ (𝑅 Cn 𝑇) ∣ (𝑘) ⊆ 𝑣})}
109abeq2i 2732 . . . 4 (𝑥 ∈ ran (𝑘 ∈ {𝑦 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑦) ∈ Comp}, 𝑣𝑇 ↦ { ∈ (𝑅 Cn 𝑇) ∣ (𝑘) ⊆ 𝑣}) ↔ ∃𝑘 ∈ 𝒫 𝑅𝑣𝑇 ((𝑅t 𝑘) ∈ Comp ∧ 𝑥 = { ∈ (𝑅 Cn 𝑇) ∣ (𝑘) ⊆ 𝑣}))
111ad2antrr 761 . . . . . . . . . . 11 (((𝜑 ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑇)) ∧ (𝑅t 𝑘) ∈ Comp) → 𝐹 ∈ (𝑅 Cn 𝑆))
1211, 2sylan 488 . . . . . . . . . 10 ((((𝜑 ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑇)) ∧ (𝑅t 𝑘) ∈ Comp) ∧ 𝑔 ∈ (𝑆 Cn 𝑇)) → (𝑔𝐹) ∈ (𝑅 Cn 𝑇))
13 imaeq1 5420 . . . . . . . . . . . . 13 ( = (𝑔𝐹) → (𝑘) = ((𝑔𝐹) “ 𝑘))
14 imaco 5599 . . . . . . . . . . . . 13 ((𝑔𝐹) “ 𝑘) = (𝑔 “ (𝐹𝑘))
1513, 14syl6eq 2671 . . . . . . . . . . . 12 ( = (𝑔𝐹) → (𝑘) = (𝑔 “ (𝐹𝑘)))
1615sseq1d 3611 . . . . . . . . . . 11 ( = (𝑔𝐹) → ((𝑘) ⊆ 𝑣 ↔ (𝑔 “ (𝐹𝑘)) ⊆ 𝑣))
1716elrab3 3347 . . . . . . . . . 10 ((𝑔𝐹) ∈ (𝑅 Cn 𝑇) → ((𝑔𝐹) ∈ { ∈ (𝑅 Cn 𝑇) ∣ (𝑘) ⊆ 𝑣} ↔ (𝑔 “ (𝐹𝑘)) ⊆ 𝑣))
1812, 17syl 17 . . . . . . . . 9 ((((𝜑 ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑇)) ∧ (𝑅t 𝑘) ∈ Comp) ∧ 𝑔 ∈ (𝑆 Cn 𝑇)) → ((𝑔𝐹) ∈ { ∈ (𝑅 Cn 𝑇) ∣ (𝑘) ⊆ 𝑣} ↔ (𝑔 “ (𝐹𝑘)) ⊆ 𝑣))
1918rabbidva 3176 . . . . . . . 8 (((𝜑 ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑇)) ∧ (𝑅t 𝑘) ∈ Comp) → {𝑔 ∈ (𝑆 Cn 𝑇) ∣ (𝑔𝐹) ∈ { ∈ (𝑅 Cn 𝑇) ∣ (𝑘) ⊆ 𝑣}} = {𝑔 ∈ (𝑆 Cn 𝑇) ∣ (𝑔 “ (𝐹𝑘)) ⊆ 𝑣})
20 eqid 2621 . . . . . . . . 9 𝑆 = 𝑆
21 cntop2 20955 . . . . . . . . . . 11 (𝐹 ∈ (𝑅 Cn 𝑆) → 𝑆 ∈ Top)
221, 21syl 17 . . . . . . . . . 10 (𝜑𝑆 ∈ Top)
2322ad2antrr 761 . . . . . . . . 9 (((𝜑 ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑇)) ∧ (𝑅t 𝑘) ∈ Comp) → 𝑆 ∈ Top)
24 xkoco1cn.t . . . . . . . . . 10 (𝜑𝑇 ∈ Top)
2524ad2antrr 761 . . . . . . . . 9 (((𝜑 ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑇)) ∧ (𝑅t 𝑘) ∈ Comp) → 𝑇 ∈ Top)
26 imassrn 5436 . . . . . . . . . 10 (𝐹𝑘) ⊆ ran 𝐹
276, 20cnf 20960 . . . . . . . . . . 11 (𝐹 ∈ (𝑅 Cn 𝑆) → 𝐹: 𝑅 𝑆)
28 frn 6010 . . . . . . . . . . 11 (𝐹: 𝑅 𝑆 → ran 𝐹 𝑆)
2911, 27, 283syl 18 . . . . . . . . . 10 (((𝜑 ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑇)) ∧ (𝑅t 𝑘) ∈ Comp) → ran 𝐹 𝑆)
3026, 29syl5ss 3594 . . . . . . . . 9 (((𝜑 ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑇)) ∧ (𝑅t 𝑘) ∈ Comp) → (𝐹𝑘) ⊆ 𝑆)
31 imacmp 21110 . . . . . . . . . 10 ((𝐹 ∈ (𝑅 Cn 𝑆) ∧ (𝑅t 𝑘) ∈ Comp) → (𝑆t (𝐹𝑘)) ∈ Comp)
3211, 31sylancom 700 . . . . . . . . 9 (((𝜑 ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑇)) ∧ (𝑅t 𝑘) ∈ Comp) → (𝑆t (𝐹𝑘)) ∈ Comp)
33 simplrr 800 . . . . . . . . 9 (((𝜑 ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑇)) ∧ (𝑅t 𝑘) ∈ Comp) → 𝑣𝑇)
3420, 23, 25, 30, 32, 33xkoopn 21302 . . . . . . . 8 (((𝜑 ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑇)) ∧ (𝑅t 𝑘) ∈ Comp) → {𝑔 ∈ (𝑆 Cn 𝑇) ∣ (𝑔 “ (𝐹𝑘)) ⊆ 𝑣} ∈ (𝑇 ^ko 𝑆))
3519, 34eqeltrd 2698 . . . . . . 7 (((𝜑 ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑇)) ∧ (𝑅t 𝑘) ∈ Comp) → {𝑔 ∈ (𝑆 Cn 𝑇) ∣ (𝑔𝐹) ∈ { ∈ (𝑅 Cn 𝑇) ∣ (𝑘) ⊆ 𝑣}} ∈ (𝑇 ^ko 𝑆))
36 imaeq2 5421 . . . . . . . . 9 (𝑥 = { ∈ (𝑅 Cn 𝑇) ∣ (𝑘) ⊆ 𝑣} → ((𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔𝐹)) “ 𝑥) = ((𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔𝐹)) “ { ∈ (𝑅 Cn 𝑇) ∣ (𝑘) ⊆ 𝑣}))
374mptpreima 5587 . . . . . . . . 9 ((𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔𝐹)) “ { ∈ (𝑅 Cn 𝑇) ∣ (𝑘) ⊆ 𝑣}) = {𝑔 ∈ (𝑆 Cn 𝑇) ∣ (𝑔𝐹) ∈ { ∈ (𝑅 Cn 𝑇) ∣ (𝑘) ⊆ 𝑣}}
3836, 37syl6eq 2671 . . . . . . . 8 (𝑥 = { ∈ (𝑅 Cn 𝑇) ∣ (𝑘) ⊆ 𝑣} → ((𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔𝐹)) “ 𝑥) = {𝑔 ∈ (𝑆 Cn 𝑇) ∣ (𝑔𝐹) ∈ { ∈ (𝑅 Cn 𝑇) ∣ (𝑘) ⊆ 𝑣}})
3938eleq1d 2683 . . . . . . 7 (𝑥 = { ∈ (𝑅 Cn 𝑇) ∣ (𝑘) ⊆ 𝑣} → (((𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔𝐹)) “ 𝑥) ∈ (𝑇 ^ko 𝑆) ↔ {𝑔 ∈ (𝑆 Cn 𝑇) ∣ (𝑔𝐹) ∈ { ∈ (𝑅 Cn 𝑇) ∣ (𝑘) ⊆ 𝑣}} ∈ (𝑇 ^ko 𝑆)))
4035, 39syl5ibrcom 237 . . . . . 6 (((𝜑 ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑇)) ∧ (𝑅t 𝑘) ∈ Comp) → (𝑥 = { ∈ (𝑅 Cn 𝑇) ∣ (𝑘) ⊆ 𝑣} → ((𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔𝐹)) “ 𝑥) ∈ (𝑇 ^ko 𝑆)))
4140expimpd 628 . . . . 5 ((𝜑 ∧ (𝑘 ∈ 𝒫 𝑅𝑣𝑇)) → (((𝑅t 𝑘) ∈ Comp ∧ 𝑥 = { ∈ (𝑅 Cn 𝑇) ∣ (𝑘) ⊆ 𝑣}) → ((𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔𝐹)) “ 𝑥) ∈ (𝑇 ^ko 𝑆)))
4241rexlimdvva 3031 . . . 4 (𝜑 → (∃𝑘 ∈ 𝒫 𝑅𝑣𝑇 ((𝑅t 𝑘) ∈ Comp ∧ 𝑥 = { ∈ (𝑅 Cn 𝑇) ∣ (𝑘) ⊆ 𝑣}) → ((𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔𝐹)) “ 𝑥) ∈ (𝑇 ^ko 𝑆)))
4310, 42syl5bi 232 . . 3 (𝜑 → (𝑥 ∈ ran (𝑘 ∈ {𝑦 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑦) ∈ Comp}, 𝑣𝑇 ↦ { ∈ (𝑅 Cn 𝑇) ∣ (𝑘) ⊆ 𝑣}) → ((𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔𝐹)) “ 𝑥) ∈ (𝑇 ^ko 𝑆)))
4443ralrimiv 2959 . 2 (𝜑 → ∀𝑥 ∈ ran (𝑘 ∈ {𝑦 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑦) ∈ Comp}, 𝑣𝑇 ↦ { ∈ (𝑅 Cn 𝑇) ∣ (𝑘) ⊆ 𝑣})((𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔𝐹)) “ 𝑥) ∈ (𝑇 ^ko 𝑆))
45 eqid 2621 . . . . 5 (𝑇 ^ko 𝑆) = (𝑇 ^ko 𝑆)
4645xkotopon 21313 . . . 4 ((𝑆 ∈ Top ∧ 𝑇 ∈ Top) → (𝑇 ^ko 𝑆) ∈ (TopOn‘(𝑆 Cn 𝑇)))
4722, 24, 46syl2anc 692 . . 3 (𝜑 → (𝑇 ^ko 𝑆) ∈ (TopOn‘(𝑆 Cn 𝑇)))
48 ovex 6632 . . . . . 6 (𝑅 Cn 𝑇) ∈ V
4948pwex 4808 . . . . 5 𝒫 (𝑅 Cn 𝑇) ∈ V
506, 7, 8xkotf 21298 . . . . . 6 (𝑘 ∈ {𝑦 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑦) ∈ Comp}, 𝑣𝑇 ↦ { ∈ (𝑅 Cn 𝑇) ∣ (𝑘) ⊆ 𝑣}):({𝑦 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑦) ∈ Comp} × 𝑇)⟶𝒫 (𝑅 Cn 𝑇)
51 frn 6010 . . . . . 6 ((𝑘 ∈ {𝑦 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑦) ∈ Comp}, 𝑣𝑇 ↦ { ∈ (𝑅 Cn 𝑇) ∣ (𝑘) ⊆ 𝑣}):({𝑦 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑦) ∈ Comp} × 𝑇)⟶𝒫 (𝑅 Cn 𝑇) → ran (𝑘 ∈ {𝑦 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑦) ∈ Comp}, 𝑣𝑇 ↦ { ∈ (𝑅 Cn 𝑇) ∣ (𝑘) ⊆ 𝑣}) ⊆ 𝒫 (𝑅 Cn 𝑇))
5250, 51ax-mp 5 . . . . 5 ran (𝑘 ∈ {𝑦 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑦) ∈ Comp}, 𝑣𝑇 ↦ { ∈ (𝑅 Cn 𝑇) ∣ (𝑘) ⊆ 𝑣}) ⊆ 𝒫 (𝑅 Cn 𝑇)
5349, 52ssexi 4763 . . . 4 ran (𝑘 ∈ {𝑦 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑦) ∈ Comp}, 𝑣𝑇 ↦ { ∈ (𝑅 Cn 𝑇) ∣ (𝑘) ⊆ 𝑣}) ∈ V
5453a1i 11 . . 3 (𝜑 → ran (𝑘 ∈ {𝑦 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑦) ∈ Comp}, 𝑣𝑇 ↦ { ∈ (𝑅 Cn 𝑇) ∣ (𝑘) ⊆ 𝑣}) ∈ V)
55 cntop1 20954 . . . . 5 (𝐹 ∈ (𝑅 Cn 𝑆) → 𝑅 ∈ Top)
561, 55syl 17 . . . 4 (𝜑𝑅 ∈ Top)
576, 7, 8xkoval 21300 . . . 4 ((𝑅 ∈ Top ∧ 𝑇 ∈ Top) → (𝑇 ^ko 𝑅) = (topGen‘(fi‘ran (𝑘 ∈ {𝑦 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑦) ∈ Comp}, 𝑣𝑇 ↦ { ∈ (𝑅 Cn 𝑇) ∣ (𝑘) ⊆ 𝑣}))))
5856, 24, 57syl2anc 692 . . 3 (𝜑 → (𝑇 ^ko 𝑅) = (topGen‘(fi‘ran (𝑘 ∈ {𝑦 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑦) ∈ Comp}, 𝑣𝑇 ↦ { ∈ (𝑅 Cn 𝑇) ∣ (𝑘) ⊆ 𝑣}))))
59 eqid 2621 . . . . 5 (𝑇 ^ko 𝑅) = (𝑇 ^ko 𝑅)
6059xkotopon 21313 . . . 4 ((𝑅 ∈ Top ∧ 𝑇 ∈ Top) → (𝑇 ^ko 𝑅) ∈ (TopOn‘(𝑅 Cn 𝑇)))
6156, 24, 60syl2anc 692 . . 3 (𝜑 → (𝑇 ^ko 𝑅) ∈ (TopOn‘(𝑅 Cn 𝑇)))
6247, 54, 58, 61subbascn 20968 . 2 (𝜑 → ((𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔𝐹)) ∈ ((𝑇 ^ko 𝑆) Cn (𝑇 ^ko 𝑅)) ↔ ((𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔𝐹)):(𝑆 Cn 𝑇)⟶(𝑅 Cn 𝑇) ∧ ∀𝑥 ∈ ran (𝑘 ∈ {𝑦 ∈ 𝒫 𝑅 ∣ (𝑅t 𝑦) ∈ Comp}, 𝑣𝑇 ↦ { ∈ (𝑅 Cn 𝑇) ∣ (𝑘) ⊆ 𝑣})((𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔𝐹)) “ 𝑥) ∈ (𝑇 ^ko 𝑆))))
635, 44, 62mpbir2and 956 1 (𝜑 → (𝑔 ∈ (𝑆 Cn 𝑇) ↦ (𝑔𝐹)) ∈ ((𝑇 ^ko 𝑆) Cn (𝑇 ^ko 𝑅)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1480   ∈ wcel 1987  ∀wral 2907  ∃wrex 2908  {crab 2911  Vcvv 3186   ⊆ wss 3555  𝒫 cpw 4130  ∪ cuni 4402   ↦ cmpt 4673   × cxp 5072  ◡ccnv 5073  ran crn 5075   “ cima 5077   ∘ ccom 5078  ⟶wf 5843  ‘cfv 5847  (class class class)co 6604   ↦ cmpt2 6606  ficfi 8260   ↾t crest 16002  topGenctg 16019  Topctop 20617  TopOnctopon 20618   Cn ccn 20938  Compccmp 21099   ^ko cxko 21274 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-iin 4488  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-om 7013  df-1st 7113  df-2nd 7114  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-oadd 7509  df-er 7687  df-map 7804  df-en 7900  df-dom 7901  df-fin 7903  df-fi 8261  df-rest 16004  df-topgen 16025  df-top 20621  df-bases 20622  df-topon 20623  df-cn 20941  df-cmp 21100  df-xko 21276 This theorem is referenced by:  cnmpt1k  21395
 Copyright terms: Public domain W3C validator