Theorem iscauf

Description: Express the property " F is a Cauchy sequence of metric D " presupposing F is a function. (Contributed by NM, 24-Jul-2007) (Revised by Mario Carneiro, 23-Dec-2013)

	Ref	Expression
Hypotheses	iscau3.2	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	iscau3.3	⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
	iscau3.4	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	iscau4.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
	iscau4.6	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) = 𝐵 )
	iscauf.7	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ 𝑋 )
Assertion	iscauf	⊢ ( 𝜑 → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐵 𝐷 𝐴 ) < 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		iscau3.2	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		iscau3.3	⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
3		iscau3.4	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4		iscau4.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
5		iscau4.6	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) = 𝐵 )
6		iscauf.7	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ 𝑋 )
7		elfvdm	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 ∈ dom ∞Met )
8	2 7	syl	⊢ ( 𝜑 → 𝑋 ∈ dom ∞Met )
9		cnex	⊢ ℂ ∈ V
10	8 9	jctir	⊢ ( 𝜑 → ( 𝑋 ∈ dom ∞Met ∧ ℂ ∈ V ) )
11		uzssz	⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
12		zsscn	⊢ ℤ ⊆ ℂ
13	11 12	sstri	⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℂ
14	1 13	eqsstri	⊢ 𝑍 ⊆ ℂ
15	6 14	jctir	⊢ ( 𝜑 → ( 𝐹 : 𝑍 ⟶ 𝑋 ∧ 𝑍 ⊆ ℂ ) )
16		elpm2r	⊢ ( ( ( 𝑋 ∈ dom ∞Met ∧ ℂ ∈ V ) ∧ ( 𝐹 : 𝑍 ⟶ 𝑋 ∧ 𝑍 ⊆ ℂ ) ) → 𝐹 ∈ ( 𝑋 ↑pm ℂ ) )
17	10 15 16	syl2anc	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 ↑pm ℂ ) )
18	17	biantrurd	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝐵 ) < 𝑥 ) ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝐵 ) < 𝑥 ) ) ) )
19	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
20	5	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝐹 ‘ 𝑗 ) = 𝐵 )
21	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝐹 : 𝑍 ⟶ 𝑋 )
22		simprl	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝑗 ∈ 𝑍 )
23	21 22	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝐹 ‘ 𝑗 ) ∈ 𝑋 )
24	20 23	eqeltrrd	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝐵 ∈ 𝑋 )
25	1	uztrn2	⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
26	25 4	sylan2	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
27		ffvelrn	⊢ ( ( 𝐹 : 𝑍 ⟶ 𝑋 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 )
28	6 25 27	syl2an	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 )
29	26 28	eqeltrrd	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝐴 ∈ 𝑋 )
30		xmetsym	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐵 𝐷 𝐴 ) = ( 𝐴 𝐷 𝐵 ) )
31	19 24 29 30	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝐵 𝐷 𝐴 ) = ( 𝐴 𝐷 𝐵 ) )
32	31	breq1d	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( 𝐵 𝐷 𝐴 ) < 𝑥 ↔ ( 𝐴 𝐷 𝐵 ) < 𝑥 ) )
33		fdm	⊢ ( 𝐹 : 𝑍 ⟶ 𝑋 → dom 𝐹 = 𝑍 )
34	33	eleq2d	⊢ ( 𝐹 : 𝑍 ⟶ 𝑋 → ( 𝑘 ∈ dom 𝐹 ↔ 𝑘 ∈ 𝑍 ) )
35	34	biimpar	⊢ ( ( 𝐹 : 𝑍 ⟶ 𝑋 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ dom 𝐹 )
36	6 25 35	syl2an	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝑘 ∈ dom 𝐹 )
37	36 29	jca	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ) )
38	37	biantrurd	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( 𝐴 𝐷 𝐵 ) < 𝑥 ↔ ( ( 𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐴 𝐷 𝐵 ) < 𝑥 ) ) )
39		df-3an	⊢ ( ( 𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝐵 ) < 𝑥 ) ↔ ( ( 𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐴 𝐷 𝐵 ) < 𝑥 ) )
40	38 39	bitr4di	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( 𝐴 𝐷 𝐵 ) < 𝑥 ↔ ( 𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝐵 ) < 𝑥 ) ) )
41	32 40	bitrd	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( 𝐵 𝐷 𝐴 ) < 𝑥 ↔ ( 𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝐵 ) < 𝑥 ) ) )
42	41	anassrs	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝐵 𝐷 𝐴 ) < 𝑥 ↔ ( 𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝐵 ) < 𝑥 ) ) )
43	42	ralbidva	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐵 𝐷 𝐴 ) < 𝑥 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝐵 ) < 𝑥 ) ) )
44	43	rexbidva	⊢ ( 𝜑 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐵 𝐷 𝐴 ) < 𝑥 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝐵 ) < 𝑥 ) ) )
45	44	ralbidv	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐵 𝐷 𝐴 ) < 𝑥 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝐵 ) < 𝑥 ) ) )
46	1 2 3 4 5	iscau4	⊢ ( 𝜑 → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝐵 ) < 𝑥 ) ) ) )
47	18 45 46	3bitr4rd	⊢ ( 𝜑 → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐵 𝐷 𝐴 ) < 𝑥 ) )