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	imbitrrid	⊢ ( ( ( 𝐽 ∈ ( 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 𝑓 ) ‘ 𝐹 ) ) ) )