This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnflf

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)

Ref Expression
Assertion cnflf ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∀ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf 𝑓 ) ‘ 𝐹 ) ) ) )

Proof

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