# Metamath Proof Explorer

## Theorem lmff

Description: If F converges, there is some upper integer set on which F is a total function. (Contributed by Mario Carneiro, 31-Dec-2013)

Ref Expression
Hypotheses lmff.1 𝑍 = ( ℤ𝑀 )
lmff.3 ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
lmff.4 ( 𝜑𝑀 ∈ ℤ )
lmff.5 ( 𝜑𝐹 ∈ dom ( ⇝𝑡𝐽 ) )
Assertion lmff ( 𝜑 → ∃ 𝑗𝑍 ( 𝐹 ↾ ( ℤ𝑗 ) ) : ( ℤ𝑗 ) ⟶ 𝑋 )

### Proof

Step Hyp Ref Expression
1 lmff.1 𝑍 = ( ℤ𝑀 )
2 lmff.3 ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3 lmff.4 ( 𝜑𝑀 ∈ ℤ )
4 lmff.5 ( 𝜑𝐹 ∈ dom ( ⇝𝑡𝐽 ) )
5 eldm2g ( 𝐹 ∈ dom ( ⇝𝑡𝐽 ) → ( 𝐹 ∈ dom ( ⇝𝑡𝐽 ) ↔ ∃ 𝑦𝐹 , 𝑦 ⟩ ∈ ( ⇝𝑡𝐽 ) ) )
6 5 ibi ( 𝐹 ∈ dom ( ⇝𝑡𝐽 ) → ∃ 𝑦𝐹 , 𝑦 ⟩ ∈ ( ⇝𝑡𝐽 ) )
7 4 6 syl ( 𝜑 → ∃ 𝑦𝐹 , 𝑦 ⟩ ∈ ( ⇝𝑡𝐽 ) )
8 df-br ( 𝐹 ( ⇝𝑡𝐽 ) 𝑦 ↔ ⟨ 𝐹 , 𝑦 ⟩ ∈ ( ⇝𝑡𝐽 ) )
9 8 exbii ( ∃ 𝑦 𝐹 ( ⇝𝑡𝐽 ) 𝑦 ↔ ∃ 𝑦𝐹 , 𝑦 ⟩ ∈ ( ⇝𝑡𝐽 ) )
10 7 9 sylibr ( 𝜑 → ∃ 𝑦 𝐹 ( ⇝𝑡𝐽 ) 𝑦 )
11 lmcl ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ( ⇝𝑡𝐽 ) 𝑦 ) → 𝑦𝑋 )
12 2 11 sylan ( ( 𝜑𝐹 ( ⇝𝑡𝐽 ) 𝑦 ) → 𝑦𝑋 )
13 eleq2 ( 𝑗 = 𝑋 → ( 𝑦𝑗𝑦𝑋 ) )
14 feq3 ( 𝑗 = 𝑋 → ( ( 𝐹𝑥 ) : 𝑥𝑗 ↔ ( 𝐹𝑥 ) : 𝑥𝑋 ) )
15 14 rexbidv ( 𝑗 = 𝑋 → ( ∃ 𝑥 ∈ ran ℤ ( 𝐹𝑥 ) : 𝑥𝑗 ↔ ∃ 𝑥 ∈ ran ℤ ( 𝐹𝑥 ) : 𝑥𝑋 ) )
16 13 15 imbi12d ( 𝑗 = 𝑋 → ( ( 𝑦𝑗 → ∃ 𝑥 ∈ ran ℤ ( 𝐹𝑥 ) : 𝑥𝑗 ) ↔ ( 𝑦𝑋 → ∃ 𝑥 ∈ ran ℤ ( 𝐹𝑥 ) : 𝑥𝑋 ) ) )
17 2 lmbr ( 𝜑 → ( 𝐹 ( ⇝𝑡𝐽 ) 𝑦 ↔ ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ 𝑦𝑋 ∧ ∀ 𝑗𝐽 ( 𝑦𝑗 → ∃ 𝑥 ∈ ran ℤ ( 𝐹𝑥 ) : 𝑥𝑗 ) ) ) )
18 17 biimpa ( ( 𝜑𝐹 ( ⇝𝑡𝐽 ) 𝑦 ) → ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ 𝑦𝑋 ∧ ∀ 𝑗𝐽 ( 𝑦𝑗 → ∃ 𝑥 ∈ ran ℤ ( 𝐹𝑥 ) : 𝑥𝑗 ) ) )
19 18 simp3d ( ( 𝜑𝐹 ( ⇝𝑡𝐽 ) 𝑦 ) → ∀ 𝑗𝐽 ( 𝑦𝑗 → ∃ 𝑥 ∈ ran ℤ ( 𝐹𝑥 ) : 𝑥𝑗 ) )
20 toponmax ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋𝐽 )
21 2 20 syl ( 𝜑𝑋𝐽 )
22 21 adantr ( ( 𝜑𝐹 ( ⇝𝑡𝐽 ) 𝑦 ) → 𝑋𝐽 )
23 16 19 22 rspcdva ( ( 𝜑𝐹 ( ⇝𝑡𝐽 ) 𝑦 ) → ( 𝑦𝑋 → ∃ 𝑥 ∈ ran ℤ ( 𝐹𝑥 ) : 𝑥𝑋 ) )
24 12 23 mpd ( ( 𝜑𝐹 ( ⇝𝑡𝐽 ) 𝑦 ) → ∃ 𝑥 ∈ ran ℤ ( 𝐹𝑥 ) : 𝑥𝑋 )
25 10 24 exlimddv ( 𝜑 → ∃ 𝑥 ∈ ran ℤ ( 𝐹𝑥 ) : 𝑥𝑋 )
26 uzf : ℤ ⟶ 𝒫 ℤ
27 ffn ( ℤ : ℤ ⟶ 𝒫 ℤ → ℤ Fn ℤ )
28 reseq2 ( 𝑥 = ( ℤ𝑗 ) → ( 𝐹𝑥 ) = ( 𝐹 ↾ ( ℤ𝑗 ) ) )
29 id ( 𝑥 = ( ℤ𝑗 ) → 𝑥 = ( ℤ𝑗 ) )
30 28 29 feq12d ( 𝑥 = ( ℤ𝑗 ) → ( ( 𝐹𝑥 ) : 𝑥𝑋 ↔ ( 𝐹 ↾ ( ℤ𝑗 ) ) : ( ℤ𝑗 ) ⟶ 𝑋 ) )
31 30 rexrn ( ℤ Fn ℤ → ( ∃ 𝑥 ∈ ran ℤ ( 𝐹𝑥 ) : 𝑥𝑋 ↔ ∃ 𝑗 ∈ ℤ ( 𝐹 ↾ ( ℤ𝑗 ) ) : ( ℤ𝑗 ) ⟶ 𝑋 ) )
32 26 27 31 mp2b ( ∃ 𝑥 ∈ ran ℤ ( 𝐹𝑥 ) : 𝑥𝑋 ↔ ∃ 𝑗 ∈ ℤ ( 𝐹 ↾ ( ℤ𝑗 ) ) : ( ℤ𝑗 ) ⟶ 𝑋 )
33 25 32 sylib ( 𝜑 → ∃ 𝑗 ∈ ℤ ( 𝐹 ↾ ( ℤ𝑗 ) ) : ( ℤ𝑗 ) ⟶ 𝑋 )
34 1 rexuz3 ( 𝑀 ∈ ℤ → ( ∃ 𝑗𝑍𝑥 ∈ ( ℤ𝑗 ) ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹𝑥 ) ∈ 𝑋 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑥 ∈ ( ℤ𝑗 ) ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹𝑥 ) ∈ 𝑋 ) ) )
35 3 34 syl ( 𝜑 → ( ∃ 𝑗𝑍𝑥 ∈ ( ℤ𝑗 ) ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹𝑥 ) ∈ 𝑋 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑥 ∈ ( ℤ𝑗 ) ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹𝑥 ) ∈ 𝑋 ) ) )
36 18 simp1d ( ( 𝜑𝐹 ( ⇝𝑡𝐽 ) 𝑦 ) → 𝐹 ∈ ( 𝑋pm ℂ ) )
37 10 36 exlimddv ( 𝜑𝐹 ∈ ( 𝑋pm ℂ ) )
38 pmfun ( 𝐹 ∈ ( 𝑋pm ℂ ) → Fun 𝐹 )
39 37 38 syl ( 𝜑 → Fun 𝐹 )
40 ffvresb ( Fun 𝐹 → ( ( 𝐹 ↾ ( ℤ𝑗 ) ) : ( ℤ𝑗 ) ⟶ 𝑋 ↔ ∀ 𝑥 ∈ ( ℤ𝑗 ) ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹𝑥 ) ∈ 𝑋 ) ) )
41 39 40 syl ( 𝜑 → ( ( 𝐹 ↾ ( ℤ𝑗 ) ) : ( ℤ𝑗 ) ⟶ 𝑋 ↔ ∀ 𝑥 ∈ ( ℤ𝑗 ) ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹𝑥 ) ∈ 𝑋 ) ) )
42 41 rexbidv ( 𝜑 → ( ∃ 𝑗𝑍 ( 𝐹 ↾ ( ℤ𝑗 ) ) : ( ℤ𝑗 ) ⟶ 𝑋 ↔ ∃ 𝑗𝑍𝑥 ∈ ( ℤ𝑗 ) ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹𝑥 ) ∈ 𝑋 ) ) )
43 41 rexbidv ( 𝜑 → ( ∃ 𝑗 ∈ ℤ ( 𝐹 ↾ ( ℤ𝑗 ) ) : ( ℤ𝑗 ) ⟶ 𝑋 ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑥 ∈ ( ℤ𝑗 ) ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹𝑥 ) ∈ 𝑋 ) ) )
44 35 42 43 3bitr4d ( 𝜑 → ( ∃ 𝑗𝑍 ( 𝐹 ↾ ( ℤ𝑗 ) ) : ( ℤ𝑗 ) ⟶ 𝑋 ↔ ∃ 𝑗 ∈ ℤ ( 𝐹 ↾ ( ℤ𝑗 ) ) : ( ℤ𝑗 ) ⟶ 𝑋 ) )
45 33 44 mpbird ( 𝜑 → ∃ 𝑗𝑍 ( 𝐹 ↾ ( ℤ𝑗 ) ) : ( ℤ𝑗 ) ⟶ 𝑋 )