This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lmbr3

Description: Express the binary relation "sequence F converges to point P " in a metric space using an arbitrary upper set of integers. (Contributed by Glauco Siliprandi, 5-Feb-2022)

Ref Expression
Hypotheses lmbr3.1 ⊢ Ⅎ 𝑘 𝐹
lmbr3.2 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
Assertion lmbr3 ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 lmbr3.1 ⊢ Ⅎ 𝑘 𝐹
2 lmbr3.2 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3 2 lmbr3v ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ∧ ∀ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 → ∃ 𝑖 ∈ ℤ ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝑙 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑙 ) ∈ 𝑣 ) ) ) ) )
4 eleq2w ⊢ ( 𝑣 = 𝑢 → ( 𝑃 ∈ 𝑣 ↔ 𝑃 ∈ 𝑢 ) )
5 eleq2w ⊢ ( 𝑣 = 𝑢 → ( ( 𝐹 ‘ 𝑙 ) ∈ 𝑣 ↔ ( 𝐹 ‘ 𝑙 ) ∈ 𝑢 ) )
6 5 anbi2d ⊢ ( 𝑣 = 𝑢 → ( ( 𝑙 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑙 ) ∈ 𝑣 ) ↔ ( 𝑙 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑙 ) ∈ 𝑢 ) ) )
7 6 rexralbidv ⊢ ( 𝑣 = 𝑢 → ( ∃ 𝑖 ∈ ℤ ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝑙 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑙 ) ∈ 𝑣 ) ↔ ∃ 𝑖 ∈ ℤ ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝑙 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑙 ) ∈ 𝑢 ) ) )
8 fveq2 ⊢ ( 𝑖 = 𝑗 → ( ℤ≥ ‘ 𝑖 ) = ( ℤ≥ ‘ 𝑗 ) )
9 8 raleqdv ⊢ ( 𝑖 = 𝑗 → ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝑙 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑙 ) ∈ 𝑢 ) ↔ ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑙 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑙 ) ∈ 𝑢 ) ) )
10 nfcv ⊢ Ⅎ 𝑘 𝑙
11 1 nfdm ⊢ Ⅎ 𝑘 dom 𝐹
12 10 11 nfel ⊢ Ⅎ 𝑘 𝑙 ∈ dom 𝐹
13 1 10 nffv ⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑙 )
14 nfcv ⊢ Ⅎ 𝑘 𝑢
15 13 14 nfel ⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑙 ) ∈ 𝑢
16 12 15 nfan ⊢ Ⅎ 𝑘 ( 𝑙 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑙 ) ∈ 𝑢 )
17 nfv ⊢ Ⅎ 𝑙 ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 )
18 eleq1w ⊢ ( 𝑙 = 𝑘 → ( 𝑙 ∈ dom 𝐹 ↔ 𝑘 ∈ dom 𝐹 ) )
19 fveq2 ⊢ ( 𝑙 = 𝑘 → ( 𝐹 ‘ 𝑙 ) = ( 𝐹 ‘ 𝑘 ) )
20 19 eleq1d ⊢ ( 𝑙 = 𝑘 → ( ( 𝐹 ‘ 𝑙 ) ∈ 𝑢 ↔ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) )
21 18 20 anbi12d ⊢ ( 𝑙 = 𝑘 → ( ( 𝑙 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑙 ) ∈ 𝑢 ) ↔ ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
22 16 17 21 cbvralw ⊢ ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑙 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑙 ) ∈ 𝑢 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) )
23 9 22 bitrdi ⊢ ( 𝑖 = 𝑗 → ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝑙 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑙 ) ∈ 𝑢 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
24 23 cbvrexvw ⊢ ( ∃ 𝑖 ∈ ℤ ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝑙 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑙 ) ∈ 𝑢 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) )
25 7 24 bitrdi ⊢ ( 𝑣 = 𝑢 → ( ∃ 𝑖 ∈ ℤ ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝑙 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑙 ) ∈ 𝑣 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
26 4 25 imbi12d ⊢ ( 𝑣 = 𝑢 → ( ( 𝑃 ∈ 𝑣 → ∃ 𝑖 ∈ ℤ ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝑙 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑙 ) ∈ 𝑣 ) ) ↔ ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) ) )
27 26 cbvralvw ⊢ ( ∀ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 → ∃ 𝑖 ∈ ℤ ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝑙 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑙 ) ∈ 𝑣 ) ) ↔ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
28 27 3anbi3i ⊢ ( ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ∧ ∀ 𝑣 ∈ 𝐽 ( 𝑃 ∈ 𝑣 → ∃ 𝑖 ∈ ℤ ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝑙 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑙 ) ∈ 𝑣 ) ) ) ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) ) )
29 3 28 bitrdi ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ) )