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 ⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ 𝑋 )