Metamath Proof Explorer

Theorem lmmbr

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 lmmbr ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 lmmbr.2 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 lmmbr.3 ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
3 1 mopntopon ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
4 2 3 syl ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
5 4 lmbr ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) ) )
6 rpxr ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ* )
7 1 blopn ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑥 ∈ ℝ* ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ∈ 𝐽 )
8 6 7 syl3an3 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ∈ 𝐽 )
9 blcntr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑥 ∈ ℝ+ ) → 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) )
10 eleq2 ⊢ ( 𝑢 = ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) → ( 𝑃 ∈ 𝑢 ↔ 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) )
11 feq3 ⊢ ( 𝑢 = ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) → ( ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ↔ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) )
12 11 rexbidv ⊢ ( 𝑢 = ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) → ( ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ↔ ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) )
13 10 12 imbi12d ⊢ ( 𝑢 = ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) → ( ( 𝑃 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ↔ ( 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) ) )
14 13 rspcva ⊢ ( ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ∈ 𝐽 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) → ( 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) )
15 14 impancom ⊢ ( ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ∈ 𝐽 ∧ 𝑃 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) → ( ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) )
16 8 9 15 syl2anc ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑥 ∈ ℝ+ ) → ( ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) )
17 16 3expa ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) ∧ 𝑥 ∈ ℝ+ ) → ( ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) )
18 17 adantlrl ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) )
19 18 impancom ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ) ) ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) → ( 𝑥 ∈ ℝ+ → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) )
20 19 ralrimiv ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ) ) ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) → ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) )
21 1 mopni2 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑢 ∈ 𝐽 ∧ 𝑃 ∈ 𝑢 ) → ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝑢 )
22 r19.29 ⊢ ( ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ∧ ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝑢 ) → ∃ 𝑥 ∈ ℝ+ ( ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝑢 ) )
23 fss ⊢ ( ( ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝑢 ) → ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 )
24 23 expcom ⊢ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝑢 → ( ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) → ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) )
25 24 reximdv ⊢ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝑢 → ( ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) )
26 25 impcom ⊢ ( ( ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝑢 ) → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 )
27 26 rexlimivw ⊢ ( ∃ 𝑥 ∈ ℝ+ ( ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ∧ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝑢 ) → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 )
28 22 27 syl ⊢ ( ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ∧ ∃ 𝑥 ∈ ℝ+ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ⊆ 𝑢 ) → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 )
29 21 28 sylan2 ⊢ ( ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ∧ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑢 ∈ 𝐽 ∧ 𝑃 ∈ 𝑢 ) ) → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 )
30 29 3exp2 ⊢ ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) → ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑢 ∈ 𝐽 → ( 𝑃 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) ) )
31 30 impcom ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) → ( 𝑢 ∈ 𝐽 → ( 𝑃 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) )
32 31 adantlr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ) ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) → ( 𝑢 ∈ 𝐽 → ( 𝑃 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) )
33 32 ralrimiv ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ) ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) → ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) )
34 20 33 impbida ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ) ) → ( ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) )
35 34 pm5.32da ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ( ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ) ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) ↔ ( ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) ) )
36 df-3an ⊢ ( ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) ↔ ( ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ) ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) )
37 df-3an ⊢ ( ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) ↔ ( ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) )
38 35 36 37 3bitr4g ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) ) )
39 2 38 syl ⊢ ( 𝜑 → ( ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) ) )
40 5 39 bitrd ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ ( 𝑃 ( ball ‘ 𝐷 ) 𝑥 ) ) ) )