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

Theorem cnpfval 21457
Description: The function mapping the points in a topology 𝐽 to the set of all functions from 𝐽 to topology 𝐾 continuous at that point. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
Assertion
Ref Expression
cnpfval ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 CnP 𝐾) = (𝑥𝑋 ↦ {𝑓 ∈ (𝑌𝑚 𝑋) ∣ ∀𝑤𝐾 ((𝑓𝑥) ∈ 𝑤 → ∃𝑣𝐽 (𝑥𝑣 ∧ (𝑓𝑣) ⊆ 𝑤))}))
Distinct variable groups:   𝑤,𝑓,𝑥,𝐾   𝑓,𝑋,𝑤,𝑥   𝑓,𝑌,𝑤,𝑥   𝑣,𝑓,𝐽,𝑤,𝑥
Allowed substitution hints:   𝐾(𝑣)   𝑋(𝑣)   𝑌(𝑣)

Proof of Theorem cnpfval
Dummy variables 𝑗 𝑘 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-cnp 21451 . . 3 CnP = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑥 𝑗 ↦ {𝑓 ∈ ( 𝑘𝑚 𝑗) ∣ ∀𝑤𝑘 ((𝑓𝑥) ∈ 𝑤 → ∃𝑣𝑗 (𝑥𝑣 ∧ (𝑓𝑣) ⊆ 𝑤))}))
21a1i 11 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → CnP = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ (𝑥 𝑗 ↦ {𝑓 ∈ ( 𝑘𝑚 𝑗) ∣ ∀𝑤𝑘 ((𝑓𝑥) ∈ 𝑤 → ∃𝑣𝑗 (𝑥𝑣 ∧ (𝑓𝑣) ⊆ 𝑤))})))
3 simprl 761 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽𝑘 = 𝐾)) → 𝑗 = 𝐽)
43unieqd 4683 . . . 4 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽𝑘 = 𝐾)) → 𝑗 = 𝐽)
5 toponuni 21137 . . . . 5 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
65ad2antrr 716 . . . 4 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽𝑘 = 𝐾)) → 𝑋 = 𝐽)
74, 6eqtr4d 2817 . . 3 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽𝑘 = 𝐾)) → 𝑗 = 𝑋)
8 simprr 763 . . . . . . 7 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽𝑘 = 𝐾)) → 𝑘 = 𝐾)
98unieqd 4683 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽𝑘 = 𝐾)) → 𝑘 = 𝐾)
10 toponuni 21137 . . . . . . 7 (𝐾 ∈ (TopOn‘𝑌) → 𝑌 = 𝐾)
1110ad2antlr 717 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽𝑘 = 𝐾)) → 𝑌 = 𝐾)
129, 11eqtr4d 2817 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽𝑘 = 𝐾)) → 𝑘 = 𝑌)
1312, 7oveq12d 6942 . . . 4 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽𝑘 = 𝐾)) → ( 𝑘𝑚 𝑗) = (𝑌𝑚 𝑋))
143rexeqdv 3341 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽𝑘 = 𝐾)) → (∃𝑣𝑗 (𝑥𝑣 ∧ (𝑓𝑣) ⊆ 𝑤) ↔ ∃𝑣𝐽 (𝑥𝑣 ∧ (𝑓𝑣) ⊆ 𝑤)))
1514imbi2d 332 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽𝑘 = 𝐾)) → (((𝑓𝑥) ∈ 𝑤 → ∃𝑣𝑗 (𝑥𝑣 ∧ (𝑓𝑣) ⊆ 𝑤)) ↔ ((𝑓𝑥) ∈ 𝑤 → ∃𝑣𝐽 (𝑥𝑣 ∧ (𝑓𝑣) ⊆ 𝑤))))
168, 15raleqbidv 3326 . . . 4 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽𝑘 = 𝐾)) → (∀𝑤𝑘 ((𝑓𝑥) ∈ 𝑤 → ∃𝑣𝑗 (𝑥𝑣 ∧ (𝑓𝑣) ⊆ 𝑤)) ↔ ∀𝑤𝐾 ((𝑓𝑥) ∈ 𝑤 → ∃𝑣𝐽 (𝑥𝑣 ∧ (𝑓𝑣) ⊆ 𝑤))))
1713, 16rabeqbidv 3392 . . 3 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽𝑘 = 𝐾)) → {𝑓 ∈ ( 𝑘𝑚 𝑗) ∣ ∀𝑤𝑘 ((𝑓𝑥) ∈ 𝑤 → ∃𝑣𝑗 (𝑥𝑣 ∧ (𝑓𝑣) ⊆ 𝑤))} = {𝑓 ∈ (𝑌𝑚 𝑋) ∣ ∀𝑤𝐾 ((𝑓𝑥) ∈ 𝑤 → ∃𝑣𝐽 (𝑥𝑣 ∧ (𝑓𝑣) ⊆ 𝑤))})
187, 17mpteq12dv 4971 . 2 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ (𝑗 = 𝐽𝑘 = 𝐾)) → (𝑥 𝑗 ↦ {𝑓 ∈ ( 𝑘𝑚 𝑗) ∣ ∀𝑤𝑘 ((𝑓𝑥) ∈ 𝑤 → ∃𝑣𝑗 (𝑥𝑣 ∧ (𝑓𝑣) ⊆ 𝑤))}) = (𝑥𝑋 ↦ {𝑓 ∈ (𝑌𝑚 𝑋) ∣ ∀𝑤𝐾 ((𝑓𝑥) ∈ 𝑤 → ∃𝑣𝐽 (𝑥𝑣 ∧ (𝑓𝑣) ⊆ 𝑤))}))
19 topontop 21136 . . 3 (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
2019adantr 474 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → 𝐽 ∈ Top)
21 topontop 21136 . . 3 (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top)
2221adantl 475 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → 𝐾 ∈ Top)
23 ovex 6956 . . . . . 6 (𝑌𝑚 𝑋) ∈ V
24 ssrab2 3908 . . . . . 6 {𝑓 ∈ (𝑌𝑚 𝑋) ∣ ∀𝑤𝐾 ((𝑓𝑥) ∈ 𝑤 → ∃𝑣𝐽 (𝑥𝑣 ∧ (𝑓𝑣) ⊆ 𝑤))} ⊆ (𝑌𝑚 𝑋)
2523, 24elpwi2 5065 . . . . 5 {𝑓 ∈ (𝑌𝑚 𝑋) ∣ ∀𝑤𝐾 ((𝑓𝑥) ∈ 𝑤 → ∃𝑣𝐽 (𝑥𝑣 ∧ (𝑓𝑣) ⊆ 𝑤))} ∈ 𝒫 (𝑌𝑚 𝑋)
2625a1i 11 . . . 4 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝑥𝑋) → {𝑓 ∈ (𝑌𝑚 𝑋) ∣ ∀𝑤𝐾 ((𝑓𝑥) ∈ 𝑤 → ∃𝑣𝐽 (𝑥𝑣 ∧ (𝑓𝑣) ⊆ 𝑤))} ∈ 𝒫 (𝑌𝑚 𝑋))
2726fmpttd 6651 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝑥𝑋 ↦ {𝑓 ∈ (𝑌𝑚 𝑋) ∣ ∀𝑤𝐾 ((𝑓𝑥) ∈ 𝑤 → ∃𝑣𝐽 (𝑥𝑣 ∧ (𝑓𝑣) ⊆ 𝑤))}):𝑋⟶𝒫 (𝑌𝑚 𝑋))
28 toponmax 21149 . . . 4 (𝐽 ∈ (TopOn‘𝑋) → 𝑋𝐽)
2928adantr 474 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → 𝑋𝐽)
3023pwex 5094 . . . 4 𝒫 (𝑌𝑚 𝑋) ∈ V
3130a1i 11 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → 𝒫 (𝑌𝑚 𝑋) ∈ V)
32 fex2 7402 . . 3 (((𝑥𝑋 ↦ {𝑓 ∈ (𝑌𝑚 𝑋) ∣ ∀𝑤𝐾 ((𝑓𝑥) ∈ 𝑤 → ∃𝑣𝐽 (𝑥𝑣 ∧ (𝑓𝑣) ⊆ 𝑤))}):𝑋⟶𝒫 (𝑌𝑚 𝑋) ∧ 𝑋𝐽 ∧ 𝒫 (𝑌𝑚 𝑋) ∈ V) → (𝑥𝑋 ↦ {𝑓 ∈ (𝑌𝑚 𝑋) ∣ ∀𝑤𝐾 ((𝑓𝑥) ∈ 𝑤 → ∃𝑣𝐽 (𝑥𝑣 ∧ (𝑓𝑣) ⊆ 𝑤))}) ∈ V)
3327, 29, 31, 32syl3anc 1439 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝑥𝑋 ↦ {𝑓 ∈ (𝑌𝑚 𝑋) ∣ ∀𝑤𝐾 ((𝑓𝑥) ∈ 𝑤 → ∃𝑣𝐽 (𝑥𝑣 ∧ (𝑓𝑣) ⊆ 𝑤))}) ∈ V)
342, 18, 20, 22, 33ovmpt2d 7067 1 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐽 CnP 𝐾) = (𝑥𝑋 ↦ {𝑓 ∈ (𝑌𝑚 𝑋) ∣ ∀𝑤𝐾 ((𝑓𝑥) ∈ 𝑤 → ∃𝑣𝐽 (𝑥𝑣 ∧ (𝑓𝑣) ⊆ 𝑤))}))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386   = wceq 1601  wcel 2107  wral 3090  wrex 3091  {crab 3094  Vcvv 3398  wss 3792  𝒫 cpw 4379   cuni 4673  cmpt 4967  cima 5360  wf 6133  cfv 6137  (class class class)co 6924  cmpt2 6926  𝑚 cmap 8142  Topctop 21116  TopOnctopon 21133   CnP ccnp 21448
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4674  df-br 4889  df-opab 4951  df-mpt 4968  df-id 5263  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-fv 6145  df-ov 6927  df-oprab 6928  df-mpt2 6929  df-top 21117  df-topon 21134  df-cnp 21451
This theorem is referenced by:  cnpval  21459  iscnp2  21462  cnambfre  34092
  Copyright terms: Public domain W3C validator