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 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ) )