Metamath Proof Explorer

Theorem lmbr2

Description: Express the binary relation "sequence F converges to point P " in a metric space using an arbitrary upper set of integers. (Contributed by Mario Carneiro, 14-Nov-2013)

Ref Expression
Hypotheses lmbr.2 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
lmbr2.4 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
lmbr2.5 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
Assertion lmbr2 ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 lmbr.2 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2 lmbr2.4 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 lmbr2.5 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4 1 lmbr ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑧 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑧 ) : 𝑧 ⟶ 𝑢 ) ) ) )
5 uzf ⊢ ℤ≥ : ℤ ⟶ 𝒫 ℤ
6 ffn ⊢ ( ℤ≥ : ℤ ⟶ 𝒫 ℤ → ℤ≥ Fn ℤ )
7 reseq2 ⊢ ( 𝑧 = ( ℤ≥ ‘ 𝑗 ) → ( 𝐹 ↾ 𝑧 ) = ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) )
8 id ⊢ ( 𝑧 = ( ℤ≥ ‘ 𝑗 ) → 𝑧 = ( ℤ≥ ‘ 𝑗 ) )
9 7 8 feq12d ⊢ ( 𝑧 = ( ℤ≥ ‘ 𝑗 ) → ( ( 𝐹 ↾ 𝑧 ) : 𝑧 ⟶ 𝑢 ↔ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ 𝑢 ) )
10 9 rexrn ⊢ ( ℤ≥ Fn ℤ → ( ∃ 𝑧 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑧 ) : 𝑧 ⟶ 𝑢 ↔ ∃ 𝑗 ∈ ℤ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ 𝑢 ) )
11 5 6 10 mp2b ⊢ ( ∃ 𝑧 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑧 ) : 𝑧 ⟶ 𝑢 ↔ ∃ 𝑗 ∈ ℤ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ 𝑢 )
12 pmfun ⊢ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) → Fun 𝐹 )
13 12 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ) ) → Fun 𝐹 )
14 ffvresb ⊢ ( Fun 𝐹 → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ 𝑢 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
15 13 14 syl ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ) ) → ( ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ 𝑢 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
16 15 rexbidv ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ) ) → ( ∃ 𝑗 ∈ ℤ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ 𝑢 ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
17 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ) ) → 𝑀 ∈ ℤ )
18 2 rexuz3 ⊢ ( 𝑀 ∈ ℤ → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
19 17 18 syl ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ) ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
20 16 19 bitr4d ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ) ) → ( ∃ 𝑗 ∈ ℤ ( 𝐹 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ 𝑢 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
21 11 20 syl5bb ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ) ) → ( ∃ 𝑧 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑧 ) : 𝑧 ⟶ 𝑢 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
22 21 imbi2d ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ) ) → ( ( 𝑃 ∈ 𝑢 → ∃ 𝑧 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑧 ) : 𝑧 ⟶ 𝑢 ) ↔ ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) ) )
23 22 ralbidv ⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ) ) → ( ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑧 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑧 ) : 𝑧 ⟶ 𝑢 ) ↔ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) ) )
24 23 pm5.32da ⊢ ( 𝜑 → ( ( ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ) ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑧 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑧 ) : 𝑧 ⟶ 𝑢 ) ) ↔ ( ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ) ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ) )
25 df-3an ⊢ ( ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑧 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑧 ) : 𝑧 ⟶ 𝑢 ) ) ↔ ( ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ) ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑧 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑧 ) : 𝑧 ⟶ 𝑢 ) ) )
26 df-3an ⊢ ( ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ↔ ( ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ) ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) ) )
27 24 25 26 3bitr4g ⊢ ( 𝜑 → ( ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑧 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑧 ) : 𝑧 ⟶ 𝑢 ) ) ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ) )
28 4 27 bitrd ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ) )