MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iscnp2 Structured version   Visualization version   GIF version
Theorem iscnp2 22963
Description: The predicate "the class 𝐹 is a continuous function from topology 𝐽 to topology 𝐾 at point 𝑃". Based on Theorem 7.2(g) of [Munkres] p. 107. (Contributed by Mario Carneiro, 21-Aug-2015.)
Hypotheses
Ref Expression
iscn.1 𝑋 = βˆͺ 𝐽
iscn.2 π‘Œ = βˆͺ 𝐾
Assertion
Ref Expression
iscnp2 (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ 𝑋) ∧ (𝐹:π‘‹βŸΆπ‘Œ ∧ βˆ€π‘¦ ∈ 𝐾 ((πΉβ€˜π‘ƒ) ∈ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦)))))
Distinct variable groups:   π‘₯,𝑦,𝐽   π‘₯,𝐾,𝑦   π‘₯,𝑋,𝑦   π‘₯,𝐹,𝑦   π‘₯,𝑃,𝑦   π‘₯,π‘Œ,𝑦
Proof of Theorem iscnp2
Dummy variables 𝑓 𝑔 𝑗 π‘˜ 𝑣 𝑀 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 n0i 4332 . . . . . . 7 (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) β†’ Β¬ ((𝐽 CnP 𝐾)β€˜π‘ƒ) = βˆ…)
2 df-ov 7414 . . . . . . . . . 10 (𝐽 CnP 𝐾) = ( CnP β€˜βŸ¨π½, 𝐾⟩)
3 ndmfv 6925 . . . . . . . . . 10 (Β¬ ⟨𝐽, 𝐾⟩ ∈ dom CnP β†’ ( CnP β€˜βŸ¨π½, 𝐾⟩) = βˆ…)
42, 3eqtrid 2782 . . . . . . . . 9 (Β¬ ⟨𝐽, 𝐾⟩ ∈ dom CnP β†’ (𝐽 CnP 𝐾) = βˆ…)
54fveq1d 6892 . . . . . . . 8 (Β¬ ⟨𝐽, 𝐾⟩ ∈ dom CnP β†’ ((𝐽 CnP 𝐾)β€˜π‘ƒ) = (βˆ…β€˜π‘ƒ))
6 0fv 6934 . . . . . . . 8 (βˆ…β€˜π‘ƒ) = βˆ…
75, 6eqtrdi 2786 . . . . . . 7 (Β¬ ⟨𝐽, 𝐾⟩ ∈ dom CnP β†’ ((𝐽 CnP 𝐾)β€˜π‘ƒ) = βˆ…)
81, 7nsyl2 141 . . . . . 6 (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) β†’ ⟨𝐽, 𝐾⟩ ∈ dom CnP )
9 df-cnp 22952 . . . . . . 7 CnP = (𝑗 ∈ Top, π‘˜ ∈ Top ↦ (π‘₯ ∈ βˆͺ 𝑗 ↦ {𝑓 ∈ (βˆͺ π‘˜ ↑m βˆͺ 𝑗) ∣ βˆ€π‘¦ ∈ π‘˜ ((π‘“β€˜π‘₯) ∈ 𝑦 β†’ βˆƒπ‘” ∈ 𝑗 (π‘₯ ∈ 𝑔 ∧ (𝑓 β€œ 𝑔) βŠ† 𝑦))}))
10 ovex 7444 . . . . . . . . . . 11 (βˆͺ π‘˜ ↑m βˆͺ 𝑗) ∈ V
11 ssrab2 4076 . . . . . . . . . . 11 {𝑓 ∈ (βˆͺ π‘˜ ↑m βˆͺ 𝑗) ∣ βˆ€π‘¦ ∈ π‘˜ ((π‘“β€˜π‘₯) ∈ 𝑦 β†’ βˆƒπ‘” ∈ 𝑗 (π‘₯ ∈ 𝑔 ∧ (𝑓 β€œ 𝑔) βŠ† 𝑦))} βŠ† (βˆͺ π‘˜ ↑m βˆͺ 𝑗)
1210, 11elpwi2 5345 . . . . . . . . . 10 {𝑓 ∈ (βˆͺ π‘˜ ↑m βˆͺ 𝑗) ∣ βˆ€π‘¦ ∈ π‘˜ ((π‘“β€˜π‘₯) ∈ 𝑦 β†’ βˆƒπ‘” ∈ 𝑗 (π‘₯ ∈ 𝑔 ∧ (𝑓 β€œ 𝑔) βŠ† 𝑦))} ∈ 𝒫 (βˆͺ π‘˜ ↑m βˆͺ 𝑗)
1312rgenw 3063 . . . . . . . . 9 βˆ€π‘₯ ∈ βˆͺ 𝑗{𝑓 ∈ (βˆͺ π‘˜ ↑m βˆͺ 𝑗) ∣ βˆ€π‘¦ ∈ π‘˜ ((π‘“β€˜π‘₯) ∈ 𝑦 β†’ βˆƒπ‘” ∈ 𝑗 (π‘₯ ∈ 𝑔 ∧ (𝑓 β€œ 𝑔) βŠ† 𝑦))} ∈ 𝒫 (βˆͺ π‘˜ ↑m βˆͺ 𝑗)
14 eqid 2730 . . . . . . . . . 10 (π‘₯ ∈ βˆͺ 𝑗 ↦ {𝑓 ∈ (βˆͺ π‘˜ ↑m βˆͺ 𝑗) ∣ βˆ€π‘¦ ∈ π‘˜ ((π‘“β€˜π‘₯) ∈ 𝑦 β†’ βˆƒπ‘” ∈ 𝑗 (π‘₯ ∈ 𝑔 ∧ (𝑓 β€œ 𝑔) βŠ† 𝑦))}) = (π‘₯ ∈ βˆͺ 𝑗 ↦ {𝑓 ∈ (βˆͺ π‘˜ ↑m βˆͺ 𝑗) ∣ βˆ€π‘¦ ∈ π‘˜ ((π‘“β€˜π‘₯) ∈ 𝑦 β†’ βˆƒπ‘” ∈ 𝑗 (π‘₯ ∈ 𝑔 ∧ (𝑓 β€œ 𝑔) βŠ† 𝑦))})
1514fmpt 7110 . . . . . . . . 9 (βˆ€π‘₯ ∈ βˆͺ 𝑗{𝑓 ∈ (βˆͺ π‘˜ ↑m βˆͺ 𝑗) ∣ βˆ€π‘¦ ∈ π‘˜ ((π‘“β€˜π‘₯) ∈ 𝑦 β†’ βˆƒπ‘” ∈ 𝑗 (π‘₯ ∈ 𝑔 ∧ (𝑓 β€œ 𝑔) βŠ† 𝑦))} ∈ 𝒫 (βˆͺ π‘˜ ↑m βˆͺ 𝑗) ↔ (π‘₯ ∈ βˆͺ 𝑗 ↦ {𝑓 ∈ (βˆͺ π‘˜ ↑m βˆͺ 𝑗) ∣ βˆ€π‘¦ ∈ π‘˜ ((π‘“β€˜π‘₯) ∈ 𝑦 β†’ βˆƒπ‘” ∈ 𝑗 (π‘₯ ∈ 𝑔 ∧ (𝑓 β€œ 𝑔) βŠ† 𝑦))}):βˆͺ π‘—βŸΆπ’« (βˆͺ π‘˜ ↑m βˆͺ 𝑗))
1613, 15mpbi 229 . . . . . . . 8 (π‘₯ ∈ βˆͺ 𝑗 ↦ {𝑓 ∈ (βˆͺ π‘˜ ↑m βˆͺ 𝑗) ∣ βˆ€π‘¦ ∈ π‘˜ ((π‘“β€˜π‘₯) ∈ 𝑦 β†’ βˆƒπ‘” ∈ 𝑗 (π‘₯ ∈ 𝑔 ∧ (𝑓 β€œ 𝑔) βŠ† 𝑦))}):βˆͺ π‘—βŸΆπ’« (βˆͺ π‘˜ ↑m βˆͺ 𝑗)
17 vuniex 7731 . . . . . . . 8 βˆͺ 𝑗 ∈ V
1810pwex 5377 . . . . . . . 8 𝒫 (βˆͺ π‘˜ ↑m βˆͺ 𝑗) ∈ V
19 fex2 7926 . . . . . . . 8 (((π‘₯ ∈ βˆͺ 𝑗 ↦ {𝑓 ∈ (βˆͺ π‘˜ ↑m βˆͺ 𝑗) ∣ βˆ€π‘¦ ∈ π‘˜ ((π‘“β€˜π‘₯) ∈ 𝑦 β†’ βˆƒπ‘” ∈ 𝑗 (π‘₯ ∈ 𝑔 ∧ (𝑓 β€œ 𝑔) βŠ† 𝑦))}):βˆͺ π‘—βŸΆπ’« (βˆͺ π‘˜ ↑m βˆͺ 𝑗) ∧ βˆͺ 𝑗 ∈ V ∧ 𝒫 (βˆͺ π‘˜ ↑m βˆͺ 𝑗) ∈ V) β†’ (π‘₯ ∈ βˆͺ 𝑗 ↦ {𝑓 ∈ (βˆͺ π‘˜ ↑m βˆͺ 𝑗) ∣ βˆ€π‘¦ ∈ π‘˜ ((π‘“β€˜π‘₯) ∈ 𝑦 β†’ βˆƒπ‘” ∈ 𝑗 (π‘₯ ∈ 𝑔 ∧ (𝑓 β€œ 𝑔) βŠ† 𝑦))}) ∈ V)
2016, 17, 18, 19mp3an 1459 . . . . . . 7 (π‘₯ ∈ βˆͺ 𝑗 ↦ {𝑓 ∈ (βˆͺ π‘˜ ↑m βˆͺ 𝑗) ∣ βˆ€π‘¦ ∈ π‘˜ ((π‘“β€˜π‘₯) ∈ 𝑦 β†’ βˆƒπ‘” ∈ 𝑗 (π‘₯ ∈ 𝑔 ∧ (𝑓 β€œ 𝑔) βŠ† 𝑦))}) ∈ V
219, 20dmmpo 8059 . . . . . 6 dom CnP = (Top Γ— Top)
228, 21eleqtrdi 2841 . . . . 5 (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) β†’ ⟨𝐽, 𝐾⟩ ∈ (Top Γ— Top))
23 opelxp 5711 . . . . 5 (⟨𝐽, 𝐾⟩ ∈ (Top Γ— Top) ↔ (𝐽 ∈ Top ∧ 𝐾 ∈ Top))
2422, 23sylib 217 . . . 4 (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) β†’ (𝐽 ∈ Top ∧ 𝐾 ∈ Top))
2524simpld 493 . . 3 (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) β†’ 𝐽 ∈ Top)
2624simprd 494 . . 3 (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) β†’ 𝐾 ∈ Top)
27 elfvdm 6927 . . . 4 (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) β†’ 𝑃 ∈ dom (𝐽 CnP 𝐾))
28 iscn.1 . . . . . . . . 9 𝑋 = βˆͺ 𝐽
2928toptopon 22639 . . . . . . . 8 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOnβ€˜π‘‹))
30 iscn.2 . . . . . . . . 9 π‘Œ = βˆͺ 𝐾
3130toptopon 22639 . . . . . . . 8 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOnβ€˜π‘Œ))
32 cnpfval 22958 . . . . . . . 8 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ)) β†’ (𝐽 CnP 𝐾) = (π‘₯ ∈ 𝑋 ↦ {𝑓 ∈ (π‘Œ ↑m 𝑋) ∣ βˆ€π‘€ ∈ 𝐾 ((π‘“β€˜π‘₯) ∈ 𝑀 β†’ βˆƒπ‘£ ∈ 𝐽 (π‘₯ ∈ 𝑣 ∧ (𝑓 β€œ 𝑣) βŠ† 𝑀))}))
3329, 31, 32syl2anb 596 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) β†’ (𝐽 CnP 𝐾) = (π‘₯ ∈ 𝑋 ↦ {𝑓 ∈ (π‘Œ ↑m 𝑋) ∣ βˆ€π‘€ ∈ 𝐾 ((π‘“β€˜π‘₯) ∈ 𝑀 β†’ βˆƒπ‘£ ∈ 𝐽 (π‘₯ ∈ 𝑣 ∧ (𝑓 β€œ 𝑣) βŠ† 𝑀))}))
3424, 33syl 17 . . . . . 6 (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) β†’ (𝐽 CnP 𝐾) = (π‘₯ ∈ 𝑋 ↦ {𝑓 ∈ (π‘Œ ↑m 𝑋) ∣ βˆ€π‘€ ∈ 𝐾 ((π‘“β€˜π‘₯) ∈ 𝑀 β†’ βˆƒπ‘£ ∈ 𝐽 (π‘₯ ∈ 𝑣 ∧ (𝑓 β€œ 𝑣) βŠ† 𝑀))}))
3534dmeqd 5904 . . . . 5 (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) β†’ dom (𝐽 CnP 𝐾) = dom (π‘₯ ∈ 𝑋 ↦ {𝑓 ∈ (π‘Œ ↑m 𝑋) ∣ βˆ€π‘€ ∈ 𝐾 ((π‘“β€˜π‘₯) ∈ 𝑀 β†’ βˆƒπ‘£ ∈ 𝐽 (π‘₯ ∈ 𝑣 ∧ (𝑓 β€œ 𝑣) βŠ† 𝑀))}))
36 ovex 7444 . . . . . . . 8 (π‘Œ ↑m 𝑋) ∈ V
3736rabex 5331 . . . . . . 7 {𝑓 ∈ (π‘Œ ↑m 𝑋) ∣ βˆ€π‘€ ∈ 𝐾 ((π‘“β€˜π‘₯) ∈ 𝑀 β†’ βˆƒπ‘£ ∈ 𝐽 (π‘₯ ∈ 𝑣 ∧ (𝑓 β€œ 𝑣) βŠ† 𝑀))} ∈ V
3837rgenw 3063 . . . . . 6 βˆ€π‘₯ ∈ 𝑋 {𝑓 ∈ (π‘Œ ↑m 𝑋) ∣ βˆ€π‘€ ∈ 𝐾 ((π‘“β€˜π‘₯) ∈ 𝑀 β†’ βˆƒπ‘£ ∈ 𝐽 (π‘₯ ∈ 𝑣 ∧ (𝑓 β€œ 𝑣) βŠ† 𝑀))} ∈ V
39 dmmptg 6240 . . . . . 6 (βˆ€π‘₯ ∈ 𝑋 {𝑓 ∈ (π‘Œ ↑m 𝑋) ∣ βˆ€π‘€ ∈ 𝐾 ((π‘“β€˜π‘₯) ∈ 𝑀 β†’ βˆƒπ‘£ ∈ 𝐽 (π‘₯ ∈ 𝑣 ∧ (𝑓 β€œ 𝑣) βŠ† 𝑀))} ∈ V β†’ dom (π‘₯ ∈ 𝑋 ↦ {𝑓 ∈ (π‘Œ ↑m 𝑋) ∣ βˆ€π‘€ ∈ 𝐾 ((π‘“β€˜π‘₯) ∈ 𝑀 β†’ βˆƒπ‘£ ∈ 𝐽 (π‘₯ ∈ 𝑣 ∧ (𝑓 β€œ 𝑣) βŠ† 𝑀))}) = 𝑋)
4038, 39ax-mp 5 . . . . 5 dom (π‘₯ ∈ 𝑋 ↦ {𝑓 ∈ (π‘Œ ↑m 𝑋) ∣ βˆ€π‘€ ∈ 𝐾 ((π‘“β€˜π‘₯) ∈ 𝑀 β†’ βˆƒπ‘£ ∈ 𝐽 (π‘₯ ∈ 𝑣 ∧ (𝑓 β€œ 𝑣) βŠ† 𝑀))}) = 𝑋
4135, 40eqtrdi 2786 . . . 4 (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) β†’ dom (𝐽 CnP 𝐾) = 𝑋)
4227, 41eleqtrd 2833 . . 3 (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) β†’ 𝑃 ∈ 𝑋)
4325, 26, 423jca 1126 . 2 (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) β†’ (𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ 𝑋))
44 biid 260 . . 3 (𝑃 ∈ 𝑋 ↔ 𝑃 ∈ 𝑋)
45 iscnp 22961 . . 3 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ 𝐾 ∈ (TopOnβ€˜π‘Œ) ∧ 𝑃 ∈ 𝑋) β†’ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ↔ (𝐹:π‘‹βŸΆπ‘Œ ∧ βˆ€π‘¦ ∈ 𝐾 ((πΉβ€˜π‘ƒ) ∈ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦)))))
4629, 31, 44, 45syl3anb 1159 . 2 ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ 𝑋) β†’ (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ↔ (𝐹:π‘‹βŸΆπ‘Œ ∧ βˆ€π‘¦ ∈ 𝐾 ((πΉβ€˜π‘ƒ) ∈ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦)))))
4743, 46biadanii 818 1 (𝐹 ∈ ((𝐽 CnP 𝐾)β€˜π‘ƒ) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top ∧ 𝑃 ∈ 𝑋) ∧ (𝐹:π‘‹βŸΆπ‘Œ ∧ βˆ€π‘¦ ∈ 𝐾 ((πΉβ€˜π‘ƒ) ∈ 𝑦 β†’ βˆƒπ‘₯ ∈ 𝐽 (𝑃 ∈ π‘₯ ∧ (𝐹 β€œ π‘₯) βŠ† 𝑦)))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1085   = wceq 1539   ∈ wcel 2104  βˆ€wral 3059  βˆƒwrex 3068  {crab 3430  Vcvv 3472   βŠ† wss 3947  βˆ…c0 4321  π’« cpw 4601  βŸ¨cop 4633  βˆͺ cuni 4907   ↦ cmpt 5230   Γ— cxp 5673  dom cdm 5675   β€œ cima 5678  βŸΆwf 6538  β€˜cfv 6542  (class class class)co 7411   ↑m cmap 8822  Topctop 22615  TopOnctopon 22632   CnP ccnp 22949
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-fv 6550  df-ov 7414  df-oprab 7415  df-mpo 7416  df-1st 7977  df-2nd 7978  df-map 8824  df-top 22616  df-topon 22633  df-cnp 22952
This theorem is referenced by:  cnptop1  22966  cnptop2  22967  cnprcl  22969  cnpf  22971  cnpimaex  22980  cnpnei  22988  cnpco  22991  cnprest  23013  cnprest2  23014
  Copyright terms: Public domain W3C validator