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

Theorem cnpfcf 22066
Description: A function 𝐹 is continuous at point 𝐴 iff 𝐹 respects cluster points there. (Contributed by Jeff Hankins, 14-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.)
Assertion
Ref Expression
cnpfcf ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)))))
Distinct variable groups:   𝐴,𝑓   𝑓,𝐹   𝑓,𝐽   𝑓,𝐾   𝑓,𝑋   𝑓,𝑌

Proof of Theorem cnpfcf
Dummy variables 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnpf2 21276 . . . . . 6 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐹:𝑋𝑌)
213expa 1111 . . . . 5 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐹:𝑋𝑌)
323adantl3 1173 . . . 4 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → 𝐹:𝑋𝑌)
4 topontop 20939 . . . . . . 7 (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top)
5 cnpfcfi 22065 . . . . . . . . 9 ((𝐾 ∈ Top ∧ 𝐴 ∈ (𝐽 fClus 𝑓) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → (𝐹𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹))
653com23 1120 . . . . . . . 8 ((𝐾 ∈ Top ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ∧ 𝐴 ∈ (𝐽 fClus 𝑓)) → (𝐹𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹))
763expia 1114 . . . . . . 7 ((𝐾 ∈ Top ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → (𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)))
84, 7sylan 563 . . . . . 6 ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → (𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)))
98ralrimivw 3116 . . . . 5 ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → ∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)))
1093ad2antl2 1201 . . . 4 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → ∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)))
113, 10jca 497 . . 3 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → (𝐹:𝑋𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹))))
1211ex 397 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) → (𝐹:𝑋𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)))))
13 simplrl 756 . . . . . . . . . . . . . 14 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ ( ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ )) → 𝑔 ∈ (Fil‘𝑋))
14 filfbas 21873 . . . . . . . . . . . . . 14 (𝑔 ∈ (Fil‘𝑋) → 𝑔 ∈ (fBas‘𝑋))
1513, 14syl 17 . . . . . . . . . . . . 13 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ ( ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ )) → 𝑔 ∈ (fBas‘𝑋))
16 simprl 748 . . . . . . . . . . . . 13 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ ( ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ )) → ∈ (Fil‘𝑌))
17 simpllr 754 . . . . . . . . . . . . 13 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ ( ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ )) → 𝐹:𝑋𝑌)
18 simprr 750 . . . . . . . . . . . . 13 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ ( ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ )) → ((𝑌 FilMap 𝐹)‘𝑔) ⊆ )
1915, 16, 17, 18fmfnfm 21983 . . . . . . . . . . . 12 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ ( ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ )) → ∃𝑓 ∈ (Fil‘𝑋)(𝑔𝑓 = ((𝑌 FilMap 𝐹)‘𝑓)))
20 r19.29 3220 . . . . . . . . . . . . 13 ((∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) ∧ ∃𝑓 ∈ (Fil‘𝑋)(𝑔𝑓 = ((𝑌 FilMap 𝐹)‘𝑓))) → ∃𝑓 ∈ (Fil‘𝑋)((𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) ∧ (𝑔𝑓 = ((𝑌 FilMap 𝐹)‘𝑓))))
21 flimfcls 22051 . . . . . . . . . . . . . . . . . . 19 (𝐽 fLim 𝑓) ⊆ (𝐽 fClus 𝑓)
22 simpll1 1254 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → 𝐽 ∈ (TopOn‘𝑋))
2322ad2antrr 699 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ ( ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ )) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔𝑓 = ((𝑌 FilMap 𝐹)‘𝑓)))) → 𝐽 ∈ (TopOn‘𝑋))
24 simprl 748 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ ( ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ )) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔𝑓 = ((𝑌 FilMap 𝐹)‘𝑓)))) → 𝑓 ∈ (Fil‘𝑋))
25 simprrl 760 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ ( ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ )) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔𝑓 = ((𝑌 FilMap 𝐹)‘𝑓)))) → 𝑔𝑓)
26 flimss2 21997 . . . . . . . . . . . . . . . . . . . . 21 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑓 ∈ (Fil‘𝑋) ∧ 𝑔𝑓) → (𝐽 fLim 𝑔) ⊆ (𝐽 fLim 𝑓))
2723, 24, 25, 26syl3anc 1476 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ ( ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ )) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔𝑓 = ((𝑌 FilMap 𝐹)‘𝑓)))) → (𝐽 fLim 𝑔) ⊆ (𝐽 fLim 𝑓))
28 simprr 750 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → 𝐴 ∈ (𝐽 fLim 𝑔))
2928ad2antrr 699 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ ( ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ )) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔𝑓 = ((𝑌 FilMap 𝐹)‘𝑓)))) → 𝐴 ∈ (𝐽 fLim 𝑔))
3027, 29sseldd 3754 . . . . . . . . . . . . . . . . . . 19 ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ ( ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ )) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔𝑓 = ((𝑌 FilMap 𝐹)‘𝑓)))) → 𝐴 ∈ (𝐽 fLim 𝑓))
3121, 30sseldi 3751 . . . . . . . . . . . . . . . . . 18 ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ ( ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ )) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔𝑓 = ((𝑌 FilMap 𝐹)‘𝑓)))) → 𝐴 ∈ (𝐽 fClus 𝑓))
32 simpll2 1256 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → 𝐾 ∈ (TopOn‘𝑌))
3332ad2antrr 699 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ ( ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ )) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔𝑓 = ((𝑌 FilMap 𝐹)‘𝑓)))) → 𝐾 ∈ (TopOn‘𝑌))
34 simplr 746 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → 𝐹:𝑋𝑌)
3534ad2antrr 699 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ ( ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ )) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔𝑓 = ((𝑌 FilMap 𝐹)‘𝑓)))) → 𝐹:𝑋𝑌)
36 fcfval 22058 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝑓 ∈ (Fil‘𝑋) ∧ 𝐹:𝑋𝑌) → ((𝐾 fClusf 𝑓)‘𝐹) = (𝐾 fClus ((𝑌 FilMap 𝐹)‘𝑓)))
3733, 24, 35, 36syl3anc 1476 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ ( ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ )) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔𝑓 = ((𝑌 FilMap 𝐹)‘𝑓)))) → ((𝐾 fClusf 𝑓)‘𝐹) = (𝐾 fClus ((𝑌 FilMap 𝐹)‘𝑓)))
38 simprrr 761 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ ( ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ )) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔𝑓 = ((𝑌 FilMap 𝐹)‘𝑓)))) → = ((𝑌 FilMap 𝐹)‘𝑓))
3938oveq2d 6810 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ ( ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ )) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔𝑓 = ((𝑌 FilMap 𝐹)‘𝑓)))) → (𝐾 fClus ) = (𝐾 fClus ((𝑌 FilMap 𝐹)‘𝑓)))
4037, 39eqtr4d 2808 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ ( ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ )) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔𝑓 = ((𝑌 FilMap 𝐹)‘𝑓)))) → ((𝐾 fClusf 𝑓)‘𝐹) = (𝐾 fClus ))
4140eleq2d 2836 . . . . . . . . . . . . . . . . . . 19 ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ ( ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ )) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔𝑓 = ((𝑌 FilMap 𝐹)‘𝑓)))) → ((𝐹𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹) ↔ (𝐹𝐴) ∈ (𝐾 fClus )))
4241biimpd 219 . . . . . . . . . . . . . . . . . 18 ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ ( ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ )) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔𝑓 = ((𝑌 FilMap 𝐹)‘𝑓)))) → ((𝐹𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹) → (𝐹𝐴) ∈ (𝐾 fClus )))
4331, 42embantd 59 . . . . . . . . . . . . . . . . 17 ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ ( ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ )) ∧ (𝑓 ∈ (Fil‘𝑋) ∧ (𝑔𝑓 = ((𝑌 FilMap 𝐹)‘𝑓)))) → ((𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → (𝐹𝐴) ∈ (𝐾 fClus )))
4443expr 444 . . . . . . . . . . . . . . . 16 ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ ( ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ )) ∧ 𝑓 ∈ (Fil‘𝑋)) → ((𝑔𝑓 = ((𝑌 FilMap 𝐹)‘𝑓)) → ((𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → (𝐹𝐴) ∈ (𝐾 fClus ))))
4544com23 86 . . . . . . . . . . . . . . 15 ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ ( ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ )) ∧ 𝑓 ∈ (Fil‘𝑋)) → ((𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → ((𝑔𝑓 = ((𝑌 FilMap 𝐹)‘𝑓)) → (𝐹𝐴) ∈ (𝐾 fClus ))))
4645impd 396 . . . . . . . . . . . . . 14 ((((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ ( ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ )) ∧ 𝑓 ∈ (Fil‘𝑋)) → (((𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) ∧ (𝑔𝑓 = ((𝑌 FilMap 𝐹)‘𝑓))) → (𝐹𝐴) ∈ (𝐾 fClus )))
4746rexlimdva 3179 . . . . . . . . . . . . 13 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ ( ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ )) → (∃𝑓 ∈ (Fil‘𝑋)((𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) ∧ (𝑔𝑓 = ((𝑌 FilMap 𝐹)‘𝑓))) → (𝐹𝐴) ∈ (𝐾 fClus )))
4820, 47syl5 34 . . . . . . . . . . . 12 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ ( ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ )) → ((∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) ∧ ∃𝑓 ∈ (Fil‘𝑋)(𝑔𝑓 = ((𝑌 FilMap 𝐹)‘𝑓))) → (𝐹𝐴) ∈ (𝐾 fClus )))
4919, 48mpan2d 668 . . . . . . . . . . 11 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ ( ∈ (Fil‘𝑌) ∧ ((𝑌 FilMap 𝐹)‘𝑔) ⊆ )) → (∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → (𝐹𝐴) ∈ (𝐾 fClus )))
5049expr 444 . . . . . . . . . 10 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ ∈ (Fil‘𝑌)) → (((𝑌 FilMap 𝐹)‘𝑔) ⊆ → (∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → (𝐹𝐴) ∈ (𝐾 fClus ))))
5150com23 86 . . . . . . . . 9 (((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) ∧ ∈ (Fil‘𝑌)) → (∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → (((𝑌 FilMap 𝐹)‘𝑔) ⊆ → (𝐹𝐴) ∈ (𝐾 fClus ))))
5251ralrimdva 3118 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → (∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → ∀ ∈ (Fil‘𝑌)(((𝑌 FilMap 𝐹)‘𝑔) ⊆ → (𝐹𝐴) ∈ (𝐾 fClus ))))
53 toponmax 20952 . . . . . . . . . . . . 13 (𝐾 ∈ (TopOn‘𝑌) → 𝑌𝐾)
5432, 53syl 17 . . . . . . . . . . . 12 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → 𝑌𝐾)
55 simprl 748 . . . . . . . . . . . . 13 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → 𝑔 ∈ (Fil‘𝑋))
5655, 14syl 17 . . . . . . . . . . . 12 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → 𝑔 ∈ (fBas‘𝑋))
57 fmfil 21969 . . . . . . . . . . . 12 ((𝑌𝐾𝑔 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋𝑌) → ((𝑌 FilMap 𝐹)‘𝑔) ∈ (Fil‘𝑌))
5854, 56, 34, 57syl3anc 1476 . . . . . . . . . . 11 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → ((𝑌 FilMap 𝐹)‘𝑔) ∈ (Fil‘𝑌))
59 toponuni 20940 . . . . . . . . . . . . 13 (𝐾 ∈ (TopOn‘𝑌) → 𝑌 = 𝐾)
6032, 59syl 17 . . . . . . . . . . . 12 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → 𝑌 = 𝐾)
6160fveq2d 6337 . . . . . . . . . . 11 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → (Fil‘𝑌) = (Fil‘ 𝐾))
6258, 61eleqtrd 2852 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → ((𝑌 FilMap 𝐹)‘𝑔) ∈ (Fil‘ 𝐾))
63 eqid 2771 . . . . . . . . . . 11 𝐾 = 𝐾
6463flimfnfcls 22053 . . . . . . . . . 10 (((𝑌 FilMap 𝐹)‘𝑔) ∈ (Fil‘ 𝐾) → ((𝐹𝐴) ∈ (𝐾 fLim ((𝑌 FilMap 𝐹)‘𝑔)) ↔ ∀ ∈ (Fil‘ 𝐾)(((𝑌 FilMap 𝐹)‘𝑔) ⊆ → (𝐹𝐴) ∈ (𝐾 fClus ))))
6562, 64syl 17 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → ((𝐹𝐴) ∈ (𝐾 fLim ((𝑌 FilMap 𝐹)‘𝑔)) ↔ ∀ ∈ (Fil‘ 𝐾)(((𝑌 FilMap 𝐹)‘𝑔) ⊆ → (𝐹𝐴) ∈ (𝐾 fClus ))))
66 flfval 22015 . . . . . . . . . . 11 ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝑔 ∈ (Fil‘𝑋) ∧ 𝐹:𝑋𝑌) → ((𝐾 fLimf 𝑔)‘𝐹) = (𝐾 fLim ((𝑌 FilMap 𝐹)‘𝑔)))
6732, 55, 34, 66syl3anc 1476 . . . . . . . . . 10 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → ((𝐾 fLimf 𝑔)‘𝐹) = (𝐾 fLim ((𝑌 FilMap 𝐹)‘𝑔)))
6867eleq2d 2836 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → ((𝐹𝐴) ∈ ((𝐾 fLimf 𝑔)‘𝐹) ↔ (𝐹𝐴) ∈ (𝐾 fLim ((𝑌 FilMap 𝐹)‘𝑔))))
6961raleqdv 3293 . . . . . . . . 9 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → (∀ ∈ (Fil‘𝑌)(((𝑌 FilMap 𝐹)‘𝑔) ⊆ → (𝐹𝐴) ∈ (𝐾 fClus )) ↔ ∀ ∈ (Fil‘ 𝐾)(((𝑌 FilMap 𝐹)‘𝑔) ⊆ → (𝐹𝐴) ∈ (𝐾 fClus ))))
7065, 68, 693bitr4d 300 . . . . . . . 8 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → ((𝐹𝐴) ∈ ((𝐾 fLimf 𝑔)‘𝐹) ↔ ∀ ∈ (Fil‘𝑌)(((𝑌 FilMap 𝐹)‘𝑔) ⊆ → (𝐹𝐴) ∈ (𝐾 fClus ))))
7152, 70sylibrd 249 . . . . . . 7 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ (𝑔 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝑔))) → (∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → (𝐹𝐴) ∈ ((𝐾 fLimf 𝑔)‘𝐹)))
7271expr 444 . . . . . 6 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ 𝑔 ∈ (Fil‘𝑋)) → (𝐴 ∈ (𝐽 fLim 𝑔) → (∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → (𝐹𝐴) ∈ ((𝐾 fLimf 𝑔)‘𝐹))))
7372com23 86 . . . . 5 ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) ∧ 𝑔 ∈ (Fil‘𝑋)) → (∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → (𝐴 ∈ (𝐽 fLim 𝑔) → (𝐹𝐴) ∈ ((𝐾 fLimf 𝑔)‘𝐹))))
7473ralrimdva 3118 . . . 4 (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) ∧ 𝐹:𝑋𝑌) → (∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)) → ∀𝑔 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fLim 𝑔) → (𝐹𝐴) ∈ ((𝐾 fLimf 𝑔)‘𝐹))))
7574imdistanda 555 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) → ((𝐹:𝑋𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹))) → (𝐹:𝑋𝑌 ∧ ∀𝑔 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fLim 𝑔) → (𝐹𝐴) ∈ ((𝐾 fLimf 𝑔)‘𝐹)))))
76 cnpflf 22026 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑔 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fLim 𝑔) → (𝐹𝐴) ∈ ((𝐾 fLimf 𝑔)‘𝐹)))))
7775, 76sylibrd 249 . 2 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) → ((𝐹:𝑋𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹))) → 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)))
7812, 77impbid 202 1 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fClus 𝑓) → (𝐹𝐴) ∈ ((𝐾 fClusf 𝑓)‘𝐹)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  w3a 1071   = wceq 1631  wcel 2145  wral 3061  wrex 3062  wss 3724   cuni 4575  wf 6028  cfv 6032  (class class class)co 6794  fBascfbas 19950  Topctop 20919  TopOnctopon 20936   CnP ccnp 21251  Filcfil 21870   FilMap cfm 21958   fLim cflim 21959   fLimf cflf 21960   fClus cfcls 21961   fClusf cfcf 21962
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4905  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7097
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3589  df-csb 3684  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-pss 3740  df-nul 4065  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-int 4613  df-iun 4657  df-iin 4658  df-br 4788  df-opab 4848  df-mpt 4865  df-tr 4888  df-id 5158  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-we 5211  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-pred 5824  df-ord 5870  df-on 5871  df-lim 5872  df-suc 5873  df-iota 5995  df-fun 6034  df-fn 6035  df-f 6036  df-f1 6037  df-fo 6038  df-f1o 6039  df-fv 6040  df-ov 6797  df-oprab 6798  df-mpt2 6799  df-om 7214  df-1st 7316  df-2nd 7317  df-wrecs 7560  df-recs 7622  df-rdg 7660  df-1o 7714  df-oadd 7718  df-er 7897  df-map 8012  df-en 8111  df-fin 8114  df-fi 8474  df-fbas 19959  df-fg 19960  df-top 20920  df-topon 20937  df-cld 21045  df-ntr 21046  df-cls 21047  df-nei 21124  df-cnp 21254  df-fil 21871  df-fm 21963  df-flim 21964  df-flf 21965  df-fcls 21966  df-fcf 21967
This theorem is referenced by:  cnfcf  22067
  Copyright terms: Public domain W3C validator