Theorem lmmbrf

Description: Express the binary relation "sequence F converges to point P " in a metric space using an arbitrary upper set of integers. This version of lmmbr2 presupposes that F is a function. (Contributed by NM, 20-Jul-2007) (Revised by Mario Carneiro, 1-May-2014)

	Ref	Expression
Hypotheses	lmmbr.2	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
	lmmbr.3	⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
	lmmbr3.5	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	lmmbr3.6	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	lmmbrf.7	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
	lmmbrf.8	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ 𝑋 )
Assertion	lmmbrf	⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ ( 𝑃 ∈ 𝑋 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐴 𝐷 𝑃 ) < 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lmmbr.2	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2		lmmbr.3	⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
3		lmmbr3.5	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4		lmmbr3.6	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
5		lmmbrf.7	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
6		lmmbrf.8	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ 𝑋 )
7		elfvdm	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 ∈ dom ∞Met )
8		cnex	⊢ ℂ ∈ V
9	7 8	jctir	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑋 ∈ dom ∞Met ∧ ℂ ∈ V ) )
10		uzssz	⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
11		zsscn	⊢ ℤ ⊆ ℂ
12	10 11	sstri	⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℂ
13	3 12	eqsstri	⊢ 𝑍 ⊆ ℂ
14	13	jctr	⊢ ( 𝐹 : 𝑍 ⟶ 𝑋 → ( 𝐹 : 𝑍 ⟶ 𝑋 ∧ 𝑍 ⊆ ℂ ) )
15		elpm2r	⊢ ( ( ( 𝑋 ∈ dom ∞Met ∧ ℂ ∈ V ) ∧ ( 𝐹 : 𝑍 ⟶ 𝑋 ∧ 𝑍 ⊆ ℂ ) ) → 𝐹 ∈ ( 𝑋 ↑pm ℂ ) )
16	9 14 15	syl2an	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) → 𝐹 ∈ ( 𝑋 ↑pm ℂ ) )
17	2 6 16	syl2anc	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 ↑pm ℂ ) )
18	17	biantrurd	⊢ ( 𝜑 → ( ( 𝑃 ∈ 𝑋 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ ( 𝑃 ∈ 𝑋 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) ) ) )
19	3	uztrn2	⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
20	19	adantll	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
21	5	oveq1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) = ( 𝐴 𝐷 𝑃 ) )
22	21	breq1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 ↔ ( 𝐴 𝐷 𝑃 ) < 𝑥 ) )
23	22	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍 ) ) → ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 ↔ ( 𝐴 𝐷 𝑃 ) < 𝑥 ) )
24	6	fdmd	⊢ ( 𝜑 → dom 𝐹 = 𝑍 )
25	24	eleq2d	⊢ ( 𝜑 → ( 𝑘 ∈ dom 𝐹 ↔ 𝑘 ∈ 𝑍 ) )
26	25	biimpar	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ dom 𝐹 )
27	6	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 )
28	26 27	jca	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) )
29	28	biantrurd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 ↔ ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) )
30		df-3an	⊢ ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ↔ ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 ) )
31	29 30	bitr4di	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 ↔ ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) )
32	31	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍 ) ) → ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 ↔ ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) )
33	23 32	bitr3d	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ 𝑍 ) ) → ( ( 𝐴 𝐷 𝑃 ) < 𝑥 ↔ ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) )
34	33	anassrs	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝐴 𝐷 𝑃 ) < 𝑥 ↔ ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) )
35	20 34	syldan	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝐴 𝐷 𝑃 ) < 𝑥 ↔ ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) )
36	35	ralbidva	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐴 𝐷 𝑃 ) < 𝑥 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) )
37	36	rexbidva	⊢ ( 𝜑 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐴 𝐷 𝑃 ) < 𝑥 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) )
38	37	ralbidv	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐴 𝐷 𝑃 ) < 𝑥 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) )
39	38	anbi2d	⊢ ( 𝜑 → ( ( 𝑃 ∈ 𝑋 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐴 𝐷 𝑃 ) < 𝑥 ) ↔ ( 𝑃 ∈ 𝑋 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) ) )
40	1 2 3 4	lmmbr3	⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) ) )
41		3anass	⊢ ( ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ ( 𝑃 ∈ 𝑋 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) ) )
42	40 41	bitrdi	⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ ( 𝑃 ∈ 𝑋 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝑘 ) 𝐷 𝑃 ) < 𝑥 ) ) ) ) )
43	18 39 42	3bitr4rd	⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ ( 𝑃 ∈ 𝑋 ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐴 𝐷 𝑃 ) < 𝑥 ) ) )