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

Theorem cnflf 23164
Description: A function is continuous iff it respects filter limits. (Contributed by Jeff Hankins, 6-Sep-2009.) (Revised by Stefan O'Rear, 7-Aug-2015.)
Assertion
Ref Expression
cnflf ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)∀𝑥 ∈ (𝐽 fLim 𝑓)(𝐹𝑥) ∈ ((𝐾 fLimf 𝑓)‘𝐹))))
Distinct variable groups:   𝑥,𝑓,𝑋   𝑓,𝑌,𝑥   𝑓,𝐹,𝑥   𝑓,𝐽,𝑥   𝑓,𝐾,𝑥

Proof of Theorem cnflf
StepHypRef Expression
1 cncnp 22442 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑥𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥))))
2 simplr 766 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋𝑌) ∧ 𝑥𝑋) → 𝐹:𝑋𝑌)
3 cnpflf 23163 . . . . . . 7 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝑥𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝑥 ∈ (𝐽 fLim 𝑓) → (𝐹𝑥) ∈ ((𝐾 fLimf 𝑓)‘𝐹)))))
43ad4ant124 1172 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋𝑌) ∧ 𝑥𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝑥 ∈ (𝐽 fLim 𝑓) → (𝐹𝑥) ∈ ((𝐾 fLimf 𝑓)‘𝐹)))))
52, 4mpbirand 704 . . . . 5 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋𝑌) ∧ 𝑥𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥) ↔ ∀𝑓 ∈ (Fil‘𝑋)(𝑥 ∈ (𝐽 fLim 𝑓) → (𝐹𝑥) ∈ ((𝐾 fLimf 𝑓)‘𝐹))))
65ralbidva 3122 . . . 4 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋𝑌) → (∀𝑥𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥) ↔ ∀𝑥𝑋𝑓 ∈ (Fil‘𝑋)(𝑥 ∈ (𝐽 fLim 𝑓) → (𝐹𝑥) ∈ ((𝐾 fLimf 𝑓)‘𝐹))))
7 eqid 2740 . . . . . . . . . . . 12 𝐽 = 𝐽
87flimelbas 23130 . . . . . . . . . . 11 (𝑥 ∈ (𝐽 fLim 𝑓) → 𝑥 𝐽)
9 toponuni 22074 . . . . . . . . . . . . 13 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
109ad2antrr 723 . . . . . . . . . . . 12 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋𝑌) → 𝑋 = 𝐽)
1110eleq2d 2826 . . . . . . . . . . 11 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋𝑌) → (𝑥𝑋𝑥 𝐽))
128, 11syl5ibr 245 . . . . . . . . . 10 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋𝑌) → (𝑥 ∈ (𝐽 fLim 𝑓) → 𝑥𝑋))
1312pm4.71rd 563 . . . . . . . . 9 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋𝑌) → (𝑥 ∈ (𝐽 fLim 𝑓) ↔ (𝑥𝑋𝑥 ∈ (𝐽 fLim 𝑓))))
1413imbi1d 342 . . . . . . . 8 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋𝑌) → ((𝑥 ∈ (𝐽 fLim 𝑓) → (𝐹𝑥) ∈ ((𝐾 fLimf 𝑓)‘𝐹)) ↔ ((𝑥𝑋𝑥 ∈ (𝐽 fLim 𝑓)) → (𝐹𝑥) ∈ ((𝐾 fLimf 𝑓)‘𝐹))))
15 impexp 451 . . . . . . . 8 (((𝑥𝑋𝑥 ∈ (𝐽 fLim 𝑓)) → (𝐹𝑥) ∈ ((𝐾 fLimf 𝑓)‘𝐹)) ↔ (𝑥𝑋 → (𝑥 ∈ (𝐽 fLim 𝑓) → (𝐹𝑥) ∈ ((𝐾 fLimf 𝑓)‘𝐹))))
1614, 15bitrdi 287 . . . . . . 7 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋𝑌) → ((𝑥 ∈ (𝐽 fLim 𝑓) → (𝐹𝑥) ∈ ((𝐾 fLimf 𝑓)‘𝐹)) ↔ (𝑥𝑋 → (𝑥 ∈ (𝐽 fLim 𝑓) → (𝐹𝑥) ∈ ((𝐾 fLimf 𝑓)‘𝐹)))))
1716ralbidv2 3121 . . . . . 6 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋𝑌) → (∀𝑥 ∈ (𝐽 fLim 𝑓)(𝐹𝑥) ∈ ((𝐾 fLimf 𝑓)‘𝐹) ↔ ∀𝑥𝑋 (𝑥 ∈ (𝐽 fLim 𝑓) → (𝐹𝑥) ∈ ((𝐾 fLimf 𝑓)‘𝐹))))
1817ralbidv 3123 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋𝑌) → (∀𝑓 ∈ (Fil‘𝑋)∀𝑥 ∈ (𝐽 fLim 𝑓)(𝐹𝑥) ∈ ((𝐾 fLimf 𝑓)‘𝐹) ↔ ∀𝑓 ∈ (Fil‘𝑋)∀𝑥𝑋 (𝑥 ∈ (𝐽 fLim 𝑓) → (𝐹𝑥) ∈ ((𝐾 fLimf 𝑓)‘𝐹))))
19 ralcom 3283 . . . . 5 (∀𝑓 ∈ (Fil‘𝑋)∀𝑥𝑋 (𝑥 ∈ (𝐽 fLim 𝑓) → (𝐹𝑥) ∈ ((𝐾 fLimf 𝑓)‘𝐹)) ↔ ∀𝑥𝑋𝑓 ∈ (Fil‘𝑋)(𝑥 ∈ (𝐽 fLim 𝑓) → (𝐹𝑥) ∈ ((𝐾 fLimf 𝑓)‘𝐹)))
2018, 19bitrdi 287 . . . 4 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋𝑌) → (∀𝑓 ∈ (Fil‘𝑋)∀𝑥 ∈ (𝐽 fLim 𝑓)(𝐹𝑥) ∈ ((𝐾 fLimf 𝑓)‘𝐹) ↔ ∀𝑥𝑋𝑓 ∈ (Fil‘𝑋)(𝑥 ∈ (𝐽 fLim 𝑓) → (𝐹𝑥) ∈ ((𝐾 fLimf 𝑓)‘𝐹))))
216, 20bitr4d 281 . . 3 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹:𝑋𝑌) → (∀𝑥𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥) ↔ ∀𝑓 ∈ (Fil‘𝑋)∀𝑥 ∈ (𝐽 fLim 𝑓)(𝐹𝑥) ∈ ((𝐾 fLimf 𝑓)‘𝐹)))
2221pm5.32da 579 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → ((𝐹:𝑋𝑌 ∧ ∀𝑥𝑋 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑥)) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)∀𝑥 ∈ (𝐽 fLim 𝑓)(𝐹𝑥) ∈ ((𝐾 fLimf 𝑓)‘𝐹))))
231, 22bitrd 278 1 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)∀𝑥 ∈ (𝐽 fLim 𝑓)(𝐹𝑥) ∈ ((𝐾 fLimf 𝑓)‘𝐹))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1542  wcel 2110  wral 3066   cuni 4845  wf 6428  cfv 6432  (class class class)co 7272  TopOnctopon 22070   Cn ccn 22386   CnP ccnp 22387  Filcfil 23007   fLim cflim 23096   fLimf cflf 23097
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-rep 5214  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7583
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-nel 3052  df-ral 3071  df-rex 3072  df-reu 3073  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-iun 4932  df-br 5080  df-opab 5142  df-mpt 5163  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6390  df-fun 6434  df-fn 6435  df-f 6436  df-f1 6437  df-fo 6438  df-f1o 6439  df-fv 6440  df-ov 7275  df-oprab 7276  df-mpo 7277  df-1st 7825  df-2nd 7826  df-map 8609  df-topgen 17165  df-fbas 20605  df-fg 20606  df-top 22054  df-topon 22071  df-ntr 22182  df-nei 22260  df-cn 22389  df-cnp 22390  df-fil 23008  df-fm 23100  df-flim 23101  df-flf 23102
This theorem is referenced by:  cnflf2  23165  flfcntr  23205  fmcncfil  31890
  Copyright terms: Public domain W3C validator