Metamath Proof Explorer


Theorem cnfcf

Description: Continuity of a function in terms of cluster points of a function. (Contributed by Jeff Hankins, 28-Nov-2009) (Revised by Stefan O'Rear, 9-Aug-2015)

Ref Expression
Assertion cnfcf ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋𝑌 ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∀ 𝑥 ∈ ( 𝐽 fClus 𝑓 ) ( 𝐹𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ) )

Proof

Step Hyp Ref Expression
1 cncnp ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋𝑌 ∧ ∀ 𝑥𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) )
2 simplr ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋𝑌 ) ∧ 𝑥𝑋 ) → 𝐹 : 𝑋𝑌 )
3 cnpfcf ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑥𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ↔ ( 𝐹 : 𝑋𝑌 ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝑥 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ) ) )
4 3 ad4ant124 ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋𝑌 ) ∧ 𝑥𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ↔ ( 𝐹 : 𝑋𝑌 ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝑥 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ) ) )
5 2 4 mpbirand ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋𝑌 ) ∧ 𝑥𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ↔ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝑥 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ) )
6 5 ralbidva ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋𝑌 ) → ( ∀ 𝑥𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ↔ ∀ 𝑥𝑋𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝑥 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ) )
7 ralcom ( ∀ 𝑥𝑋𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝑥 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ↔ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∀ 𝑥𝑋 ( 𝑥 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) )
8 eqid 𝐽 = 𝐽
9 8 fclselbas ( 𝑥 ∈ ( 𝐽 fClus 𝑓 ) → 𝑥 𝐽 )
10 toponuni ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = 𝐽 )
11 10 ad2antrr ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋𝑌 ) → 𝑋 = 𝐽 )
12 11 eleq2d ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋𝑌 ) → ( 𝑥𝑋𝑥 𝐽 ) )
13 9 12 syl5ibr ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋𝑌 ) → ( 𝑥 ∈ ( 𝐽 fClus 𝑓 ) → 𝑥𝑋 ) )
14 13 pm4.71rd ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋𝑌 ) → ( 𝑥 ∈ ( 𝐽 fClus 𝑓 ) ↔ ( 𝑥𝑋𝑥 ∈ ( 𝐽 fClus 𝑓 ) ) ) )
15 14 imbi1d ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋𝑌 ) → ( ( 𝑥 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ↔ ( ( 𝑥𝑋𝑥 ∈ ( 𝐽 fClus 𝑓 ) ) → ( 𝐹𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ) )
16 impexp ( ( ( 𝑥𝑋𝑥 ∈ ( 𝐽 fClus 𝑓 ) ) → ( 𝐹𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ↔ ( 𝑥𝑋 → ( 𝑥 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ) )
17 15 16 bitrdi ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋𝑌 ) → ( ( 𝑥 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ↔ ( 𝑥𝑋 → ( 𝑥 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ) ) )
18 17 ralbidv2 ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋𝑌 ) → ( ∀ 𝑥 ∈ ( 𝐽 fClus 𝑓 ) ( 𝐹𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ↔ ∀ 𝑥𝑋 ( 𝑥 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ) )
19 18 ralbidv ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋𝑌 ) → ( ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∀ 𝑥 ∈ ( 𝐽 fClus 𝑓 ) ( 𝐹𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ↔ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∀ 𝑥𝑋 ( 𝑥 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ) )
20 7 19 bitr4id ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋𝑌 ) → ( ∀ 𝑥𝑋𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝑥 ∈ ( 𝐽 fClus 𝑓 ) → ( 𝐹𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ↔ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∀ 𝑥 ∈ ( 𝐽 fClus 𝑓 ) ( 𝐹𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) )
21 6 20 bitrd ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋𝑌 ) → ( ∀ 𝑥𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ↔ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∀ 𝑥 ∈ ( 𝐽 fClus 𝑓 ) ( 𝐹𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) )
22 21 pm5.32da ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( ( 𝐹 : 𝑋𝑌 ∧ ∀ 𝑥𝑋 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ↔ ( 𝐹 : 𝑋𝑌 ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∀ 𝑥 ∈ ( 𝐽 fClus 𝑓 ) ( 𝐹𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ) )
23 1 22 bitrd ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋𝑌 ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∀ 𝑥 ∈ ( 𝐽 fClus 𝑓 ) ( 𝐹𝑥 ) ∈ ( ( 𝐾 fClusf 𝑓 ) ‘ 𝐹 ) ) ) )