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 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 bitrid ⊢ ( ( 𝐷 ∈ ( ∞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 bitrid ⊢ ( 𝜑 → ( ( 𝐹 ∈ ( 𝑋 ↑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 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) ) )