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

Metamath Proof Explorer

Theorem cnflf2

Description: A function is continuous iff it respects filter limits. (Contributed by Mario Carneiro, 9-Apr-2015) (Revised by Stefan O'Rear, 8-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 cnflf ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∀ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf 𝑓 ) ‘ 𝐹 ) ) ) )
2 ffun ⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → Fun 𝐹 )
3 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
4 3 flimelbas ⊢ ( 𝑥 ∈ ( 𝐽 fLim 𝑓 ) → 𝑥 ∈ ∪ 𝐽 )
5 4 ssriv ⊢ ( 𝐽 fLim 𝑓 ) ⊆ ∪ 𝐽
6 fdm ⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → dom 𝐹 = 𝑋 )
7 6 adantl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → dom 𝐹 = 𝑋 )
8 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
9 8 ad2antrr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → 𝑋 = ∪ 𝐽 )
10 7 9 eqtrd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → dom 𝐹 = ∪ 𝐽 )
11 5 10 sseqtrrid ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( 𝐽 fLim 𝑓 ) ⊆ dom 𝐹 )
12 funimass4 ⊢ ( ( Fun 𝐹 ∧ ( 𝐽 fLim 𝑓 ) ⊆ dom 𝐹 ) → ( ( 𝐹 “ ( 𝐽 fLim 𝑓 ) ) ⊆ ( ( 𝐾 fLimf 𝑓 ) ‘ 𝐹 ) ↔ ∀ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf 𝑓 ) ‘ 𝐹 ) ) )
13 2 11 12 syl2an2 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ( 𝐹 “ ( 𝐽 fLim 𝑓 ) ) ⊆ ( ( 𝐾 fLimf 𝑓 ) ‘ 𝐹 ) ↔ ∀ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf 𝑓 ) ‘ 𝐹 ) ) )
14 13 ralbidv ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 “ ( 𝐽 fLim 𝑓 ) ) ⊆ ( ( 𝐾 fLimf 𝑓 ) ‘ 𝐹 ) ↔ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∀ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf 𝑓 ) ‘ 𝐹 ) ) )
15 14 pm5.32da ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 “ ( 𝐽 fLim 𝑓 ) ) ⊆ ( ( 𝐾 fLimf 𝑓 ) ‘ 𝐹 ) ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∀ 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf 𝑓 ) ‘ 𝐹 ) ) ) )
16 1 15 bitr4d ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐹 “ ( 𝐽 fLim 𝑓 ) ) ⊆ ( ( 𝐾 fLimf 𝑓 ) ‘ 𝐹 ) ) ) )