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 𝑓 ) ‘ 𝐹 ) ) ) )