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

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