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

Metamath Proof Explorer

Definition df-lm

Description: Define a function on topologies whose value is the convergence relation for sequences into the given topological space. Although f is typically a sequence (a function from an upperset of integers) with values in the topological space, it need not be. Note, however, that the limit property concerns only values at integers, so that the real-valued function ( x e. RR |-> ( sin( _pi x. x ) ) ) converges to zero (in the standard topology on the reals) with this definition. (Contributed by NM, 7-Sep-2006)

Ref Expression
Assertion df-lm ⇝𝑡 = ( 𝑗 ∈ Top ↦ { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( 𝑓 ∈ ( ∪ 𝑗 ↑pm ℂ ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀ 𝑢 ∈ 𝑗 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clm ⊢ ⇝𝑡
1 vj ⊢ 𝑗
2 ctop ⊢ Top
3 vf ⊢ 𝑓
4 vx ⊢ 𝑥
5 3 cv ⊢ 𝑓
6 1 cv ⊢ 𝑗
7 6 cuni ⊢ ∪ 𝑗
8 cpm ⊢ ↑pm
9 cc ⊢ ℂ
10 7 9 8 co ⊢ ( ∪ 𝑗 ↑pm ℂ )
11 5 10 wcel ⊢ 𝑓 ∈ ( ∪ 𝑗 ↑pm ℂ )
12 4 cv ⊢ 𝑥
13 12 7 wcel ⊢ 𝑥 ∈ ∪ 𝑗
14 vu ⊢ 𝑢
15 14 cv ⊢ 𝑢
16 12 15 wcel ⊢ 𝑥 ∈ 𝑢
17 vy ⊢ 𝑦
18 cuz ⊢ ℤ≥
19 18 crn ⊢ ran ℤ≥
20 17 cv ⊢ 𝑦
21 5 20 cres ⊢ ( 𝑓 ↾ 𝑦 )
22 20 15 21 wf ⊢ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢
23 22 17 19 wrex ⊢ ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢
24 16 23 wi ⊢ ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 )
25 24 14 6 wral ⊢ ∀ 𝑢 ∈ 𝑗 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 )
26 11 13 25 w3a ⊢ ( 𝑓 ∈ ( ∪ 𝑗 ↑pm ℂ ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀ 𝑢 ∈ 𝑗 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) )
27 26 3 4 copab ⊢ { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( 𝑓 ∈ ( ∪ 𝑗 ↑pm ℂ ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀ 𝑢 ∈ 𝑗 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) }
28 1 2 27 cmpt ⊢ ( 𝑗 ∈ Top ↦ { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( 𝑓 ∈ ( ∪ 𝑗 ↑pm ℂ ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀ 𝑢 ∈ 𝑗 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) } )
29 0 28 wceq ⊢ ⇝𝑡 = ( 𝑗 ∈ Top ↦ { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( 𝑓 ∈ ( ∪ 𝑗 ↑pm ℂ ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀ 𝑢 ∈ 𝑗 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) } )