Metamath Proof Explorer


Theorem lmmbr2

Description: Express the binary relation "sequence F converges to point P " in a metric space. Definition 1.4-1 of Kreyszig p. 25. The condition F C_ ( CC X. X ) allows us to use objects more general than sequences when convenient; see the comment in df-lm . (Contributed by NM, 7-Dec-2006) (Revised by Mario Carneiro, 1-May-2014)

Ref Expression
Hypotheses lmmbr.2 𝐽 = ( MetOpen ‘ 𝐷 )
lmmbr.3 ( 𝜑𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
Assertion lmmbr2 ( 𝜑 → ( 𝐹 ( ⇝𝑡𝐽 ) 𝑃 ↔ ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ 𝑃𝑋 ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 lmmbr.2 𝐽 = ( MetOpen ‘ 𝐷 )
2 lmmbr.3 ( 𝜑𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
3 1 2 lmmbr ( 𝜑 → ( 𝐹 ( ⇝𝑡𝐽 ) 𝑃 ↔ ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ 𝑃𝑋 ∧ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ran ℤ ( 𝐹𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) ) )
4 df-3an ( ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ 𝑃𝑋 ∧ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ran ℤ ( 𝐹𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) ↔ ( ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ 𝑃𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ran ℤ ( 𝐹𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) )
5 uzf : ℤ ⟶ 𝒫 ℤ
6 ffn ( ℤ : ℤ ⟶ 𝒫 ℤ → ℤ Fn ℤ )
7 reseq2 ( 𝑦 = ( ℤ𝑗 ) → ( 𝐹𝑦 ) = ( 𝐹 ↾ ( ℤ𝑗 ) ) )
8 id ( 𝑦 = ( ℤ𝑗 ) → 𝑦 = ( ℤ𝑗 ) )
9 7 8 feq12d ( 𝑦 = ( ℤ𝑗 ) → ( ( 𝐹𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ↔ ( 𝐹 ↾ ( ℤ𝑗 ) ) : ( ℤ𝑗 ) ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) )
10 9 rexrn ( ℤ Fn ℤ → ( ∃ 𝑦 ∈ ran ℤ ( 𝐹𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ↔ ∃ 𝑗 ∈ ℤ ( 𝐹 ↾ ( ℤ𝑗 ) ) : ( ℤ𝑗 ) ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) )
11 5 6 10 mp2b ( ∃ 𝑦 ∈ ran ℤ ( 𝐹𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ↔ ∃ 𝑗 ∈ ℤ ( 𝐹 ↾ ( ℤ𝑗 ) ) : ( ℤ𝑗 ) ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) )
12 simp2l ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ 𝑃𝑋 ) ∧ 𝑥 ∈ ℝ+ ) → 𝐹 ∈ ( 𝑋pm ℂ ) )
13 elfvdm ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 ∈ dom ∞Met )
14 13 3ad2ant1 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ 𝑃𝑋 ) ∧ 𝑥 ∈ ℝ+ ) → 𝑋 ∈ dom ∞Met )
15 cnex ℂ ∈ V
16 elpmg ( ( 𝑋 ∈ dom ∞Met ∧ ℂ ∈ V ) → ( 𝐹 ∈ ( 𝑋pm ℂ ) ↔ ( Fun 𝐹𝐹 ⊆ ( ℂ × 𝑋 ) ) ) )
17 14 15 16 sylancl ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ 𝑃𝑋 ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐹 ∈ ( 𝑋pm ℂ ) ↔ ( Fun 𝐹𝐹 ⊆ ( ℂ × 𝑋 ) ) ) )
18 12 17 mpbid ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ 𝑃𝑋 ) ∧ 𝑥 ∈ ℝ+ ) → ( Fun 𝐹𝐹 ⊆ ( ℂ × 𝑋 ) ) )
19 18 simpld ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ 𝑃𝑋 ) ∧ 𝑥 ∈ ℝ+ ) → Fun 𝐹 )
20 ffvresb ( Fun 𝐹 → ( ( 𝐹 ↾ ( ℤ𝑗 ) ) : ( ℤ𝑗 ) ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ↔ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) ) )
21 19 20 syl ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ 𝑃𝑋 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝐹 ↾ ( ℤ𝑗 ) ) : ( ℤ𝑗 ) ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ↔ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) ) )
22 rpxr ( 𝑥 ∈ ℝ+𝑥 ∈ ℝ* )
23 elbl ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑥 ∈ ℝ* ) → ( ( 𝐹𝑘 ) ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ↔ ( ( 𝐹𝑘 ) ∈ 𝑋 ∧ ( 𝑃 𝐷 ( 𝐹𝑘 ) ) < 𝑥 ) ) )
24 22 23 syl3an3 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑥 ∈ ℝ+ ) → ( ( 𝐹𝑘 ) ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ↔ ( ( 𝐹𝑘 ) ∈ 𝑋 ∧ ( 𝑃 𝐷 ( 𝐹𝑘 ) ) < 𝑥 ) ) )
25 xmetsym ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋 ∧ ( 𝐹𝑘 ) ∈ 𝑋 ) → ( 𝑃 𝐷 ( 𝐹𝑘 ) ) = ( ( 𝐹𝑘 ) 𝐷 𝑃 ) )
26 25 breq1d ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋 ∧ ( 𝐹𝑘 ) ∈ 𝑋 ) → ( ( 𝑃 𝐷 ( 𝐹𝑘 ) ) < 𝑥 ↔ ( ( 𝐹𝑘 ) 𝐷 𝑃 ) < 𝑥 ) )
27 26 3expa ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) ∧ ( 𝐹𝑘 ) ∈ 𝑋 ) → ( ( 𝑃 𝐷 ( 𝐹𝑘 ) ) < 𝑥 ↔ ( ( 𝐹𝑘 ) 𝐷 𝑃 ) < 𝑥 ) )
28 27 pm5.32da ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋 ) → ( ( ( 𝐹𝑘 ) ∈ 𝑋 ∧ ( 𝑃 𝐷 ( 𝐹𝑘 ) ) < 𝑥 ) ↔ ( ( 𝐹𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) )
29 28 3adant3 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑥 ∈ ℝ+ ) → ( ( ( 𝐹𝑘 ) ∈ 𝑋 ∧ ( 𝑃 𝐷 ( 𝐹𝑘 ) ) < 𝑥 ) ↔ ( ( 𝐹𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) )
30 24 29 bitrd ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑥 ∈ ℝ+ ) → ( ( 𝐹𝑘 ) ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ↔ ( ( 𝐹𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) )
31 30 3adant2l ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ 𝑃𝑋 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝐹𝑘 ) ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ↔ ( ( 𝐹𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) )
32 31 anbi2d ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ 𝑃𝑋 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) ↔ ( 𝑘 ∈ dom 𝐹 ∧ ( ( 𝐹𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) ) )
33 3anass ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ↔ ( 𝑘 ∈ dom 𝐹 ∧ ( ( 𝐹𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) )
34 32 33 bitr4di ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ 𝑃𝑋 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) ↔ ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) )
35 34 ralbidv ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ 𝑃𝑋 ) ∧ 𝑥 ∈ ℝ+ ) → ( ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) ↔ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) )
36 21 35 bitrd ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ 𝑃𝑋 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝐹 ↾ ( ℤ𝑗 ) ) : ( ℤ𝑗 ) ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ↔ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) )
37 36 rexbidv ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ 𝑃𝑋 ) ∧ 𝑥 ∈ ℝ+ ) → ( ∃ 𝑗 ∈ ℤ ( 𝐹 ↾ ( ℤ𝑗 ) ) : ( ℤ𝑗 ) ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) )
38 11 37 syl5bb ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ 𝑃𝑋 ) ∧ 𝑥 ∈ ℝ+ ) → ( ∃ 𝑦 ∈ ran ℤ ( 𝐹𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) )
39 38 3expa ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ 𝑃𝑋 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( ∃ 𝑦 ∈ ran ℤ ( 𝐹𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) )
40 39 ralbidva ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ 𝑃𝑋 ) ) → ( ∀ 𝑥 ∈ ℝ+𝑦 ∈ ran ℤ ( 𝐹𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) )
41 40 pm5.32da ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ( ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ 𝑃𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ran ℤ ( 𝐹𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) ↔ ( ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ 𝑃𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) ) )
42 2 41 syl ( 𝜑 → ( ( ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ 𝑃𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ran ℤ ( 𝐹𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) ↔ ( ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ 𝑃𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) ) )
43 4 42 syl5bb ( 𝜑 → ( ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ 𝑃𝑋 ∧ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ran ℤ ( 𝐹𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) ↔ ( ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ 𝑃𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) ) )
44 df-3an ( ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ 𝑃𝑋 ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) ↔ ( ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ 𝑃𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) )
45 43 44 bitr4di ( 𝜑 → ( ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ 𝑃𝑋 ∧ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ran ℤ ( 𝐹𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) ↔ ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ 𝑃𝑋 ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) ) )
46 3 45 bitrd ( 𝜑 → ( 𝐹 ( ⇝𝑡𝐽 ) 𝑃 ↔ ( 𝐹 ∈ ( 𝑋pm ℂ ) ∧ 𝑃𝑋 ∧ ∀ 𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) ) )