Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  cnpf2 GIF version

Theorem cnpf2 12413
 Description: A continuous function at point 𝑃 is a mapping. (Contributed by Mario Carneiro, 21-Aug-2015.) (Revised by Jim Kingdon, 28-Mar-2023.)
Assertion
Ref Expression
cnpf2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝐹:𝑋𝑌)

Proof of Theorem cnpf2
Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp3 984 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃))
2 topontop 12218 . . . . 5 (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top)
3 cnprcl2k 12412 . . . . 5 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ Top ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝑃𝑋)
42, 3syl3an2 1251 . . . 4 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝑃𝑋)
5 iscnp 12405 . . . 4 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑃𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑎𝐾 ((𝐹𝑃) ∈ 𝑎 → ∃𝑏𝐽 (𝑃𝑏 ∧ (𝐹𝑏) ⊆ 𝑎)))))
64, 5syld3an3 1262 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑎𝐾 ((𝐹𝑃) ∈ 𝑎 → ∃𝑏𝐽 (𝑃𝑏 ∧ (𝐹𝑏) ⊆ 𝑎)))))
71, 6mpbid 146 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → (𝐹:𝑋𝑌 ∧ ∀𝑎𝐾 ((𝐹𝑃) ∈ 𝑎 → ∃𝑏𝐽 (𝑃𝑏 ∧ (𝐹𝑏) ⊆ 𝑎))))
87simpld 111 1 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝐹:𝑋𝑌)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∧ w3a 963   ∈ wcel 1481  ∀wral 2417  ∃wrex 2418   ⊆ wss 3075   “ cima 4549  ⟶wf 5126  ‘cfv 5130  (class class class)co 5781  Topctop 12201  TopOnctopon 12214   CnP ccnp 12392 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-coll 4050  ax-sep 4053  ax-pow 4105  ax-pr 4138  ax-un 4362  ax-setind 4459 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-ral 2422  df-rex 2423  df-reu 2424  df-rab 2426  df-v 2691  df-sbc 2913  df-csb 3007  df-dif 3077  df-un 3079  df-in 3081  df-ss 3088  df-pw 3516  df-sn 3537  df-pr 3538  df-op 3540  df-uni 3744  df-iun 3822  df-br 3937  df-opab 3997  df-mpt 3998  df-id 4222  df-xp 4552  df-rel 4553  df-cnv 4554  df-co 4555  df-dm 4556  df-rn 4557  df-res 4558  df-ima 4559  df-iota 5095  df-fun 5132  df-fn 5133  df-f 5134  df-f1 5135  df-fo 5136  df-f1o 5137  df-fv 5138  df-ov 5784  df-oprab 5785  df-mpo 5786  df-1st 6045  df-2nd 6046  df-map 6551  df-top 12202  df-topon 12215  df-cnp 12395 This theorem is referenced by:  iscnp4  12424  cnptopco  12428  cncnp2m  12437  cnptopresti  12444  lmtopcnp  12456  txcnp  12477  metcnpi3  12723  cnplimcim  12842  limccnpcntop  12850  limccnp2lem  12851  limccnp2cntop  12852
 Copyright terms: Public domain W3C validator