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 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) ) )