Metamath Proof Explorer


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