Theorem lmflf

Description: The topological limit relation on functions can be written in terms of the filter limit along the filter generated by the upper integer sets. (Contributed by Mario Carneiro, 13-Oct-2015)

	Ref	Expression
Hypotheses	lmflf.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	lmflf.2	⊢ 𝐿 = ( 𝑍 filGen ( ℤ≥ “ 𝑍 ) )
Assertion	lmflf	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ 𝑃 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lmflf.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		lmflf.2	⊢ 𝐿 = ( 𝑍 filGen ( ℤ≥ “ 𝑍 ) )
3		uzf	⊢ ℤ≥ : ℤ ⟶ 𝒫 ℤ
4		ffn	⊢ ( ℤ≥ : ℤ ⟶ 𝒫 ℤ → ℤ≥ Fn ℤ )
5	3 4	ax-mp	⊢ ℤ≥ Fn ℤ
6		uzssz	⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
7	1 6	eqsstri	⊢ 𝑍 ⊆ ℤ
8		imaeq2	⊢ ( 𝑦 = ( ℤ≥ ‘ 𝑗 ) → ( 𝐹 “ 𝑦 ) = ( 𝐹 “ ( ℤ≥ ‘ 𝑗 ) ) )
9	8	sseq1d	⊢ ( 𝑦 = ( ℤ≥ ‘ 𝑗 ) → ( ( 𝐹 “ 𝑦 ) ⊆ 𝑥 ↔ ( 𝐹 “ ( ℤ≥ ‘ 𝑗 ) ) ⊆ 𝑥 ) )
10	9	rexima	⊢ ( ( ℤ≥ Fn ℤ ∧ 𝑍 ⊆ ℤ ) → ( ∃ 𝑦 ∈ ( ℤ≥ “ 𝑍 ) ( 𝐹 “ 𝑦 ) ⊆ 𝑥 ↔ ∃ 𝑗 ∈ 𝑍 ( 𝐹 “ ( ℤ≥ ‘ 𝑗 ) ) ⊆ 𝑥 ) )
11	5 7 10	mp2an	⊢ ( ∃ 𝑦 ∈ ( ℤ≥ “ 𝑍 ) ( 𝐹 “ 𝑦 ) ⊆ 𝑥 ↔ ∃ 𝑗 ∈ 𝑍 ( 𝐹 “ ( ℤ≥ ‘ 𝑗 ) ) ⊆ 𝑥 )
12		simpl3	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) → 𝐹 : 𝑍 ⟶ 𝑋 )
13	12	ffund	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) → Fun 𝐹 )
14		uzss	⊢ ( 𝑗 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ℤ≥ ‘ 𝑗 ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
15	14 1	eleq2s	⊢ ( 𝑗 ∈ 𝑍 → ( ℤ≥ ‘ 𝑗 ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
16	15	adantl	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) → ( ℤ≥ ‘ 𝑗 ) ⊆ ( ℤ≥ ‘ 𝑀 ) )
17	12	fdmd	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) → dom 𝐹 = 𝑍 )
18	17 1	eqtrdi	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) → dom 𝐹 = ( ℤ≥ ‘ 𝑀 ) )
19	16 18	sseqtrrd	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) → ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 )
20		funimass4	⊢ ( ( Fun 𝐹 ∧ ( ℤ≥ ‘ 𝑗 ) ⊆ dom 𝐹 ) → ( ( 𝐹 “ ( ℤ≥ ‘ 𝑗 ) ) ⊆ 𝑥 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑥 ) )
21	13 19 20	syl2anc	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) → ( ( 𝐹 “ ( ℤ≥ ‘ 𝑗 ) ) ⊆ 𝑥 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑥 ) )
22	21	rexbidva	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) → ( ∃ 𝑗 ∈ 𝑍 ( 𝐹 “ ( ℤ≥ ‘ 𝑗 ) ) ⊆ 𝑥 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑥 ) )
23	11 22	bitr2id	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑥 ↔ ∃ 𝑦 ∈ ( ℤ≥ “ 𝑍 ) ( 𝐹 “ 𝑦 ) ⊆ 𝑥 ) )
24	23	imbi2d	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) → ( ( 𝑃 ∈ 𝑥 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑥 ) ↔ ( 𝑃 ∈ 𝑥 → ∃ 𝑦 ∈ ( ℤ≥ “ 𝑍 ) ( 𝐹 “ 𝑦 ) ⊆ 𝑥 ) ) )
25	24	ralbidv	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) → ( ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑦 ∈ ( ℤ≥ “ 𝑍 ) ( 𝐹 “ 𝑦 ) ⊆ 𝑥 ) ) )
26	25	anbi2d	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) → ( ( 𝑃 ∈ 𝑋 ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑥 ) ) ↔ ( 𝑃 ∈ 𝑋 ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑦 ∈ ( ℤ≥ “ 𝑍 ) ( 𝐹 “ 𝑦 ) ⊆ 𝑥 ) ) ) )
27		simp1	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
28		simp2	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) → 𝑀 ∈ ℤ )
29		simp3	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) → 𝐹 : 𝑍 ⟶ 𝑋 )
30		eqidd	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
31	27 1 28 29 30	lmbrf	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ ( 𝑃 ∈ 𝑋 ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ∈ 𝑥 ) ) ) )
32	1	uzfbas	⊢ ( 𝑀 ∈ ℤ → ( ℤ≥ “ 𝑍 ) ∈ ( fBas ‘ 𝑍 ) )
33	2	flffbas	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( ℤ≥ “ 𝑍 ) ∈ ( fBas ‘ 𝑍 ) ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) → ( 𝑃 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ↔ ( 𝑃 ∈ 𝑋 ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑦 ∈ ( ℤ≥ “ 𝑍 ) ( 𝐹 “ 𝑦 ) ⊆ 𝑥 ) ) ) )
34	32 33	syl3an2	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) → ( 𝑃 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ↔ ( 𝑃 ∈ 𝑋 ∧ ∀ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 → ∃ 𝑦 ∈ ( ℤ≥ “ 𝑍 ) ( 𝐹 “ 𝑦 ) ⊆ 𝑥 ) ) ) )
35	26 31 34	3bitr4d	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ 𝑃 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ) )