Theorem caucfil

Description: A Cauchy sequence predicate can be expressed in terms of the Cauchy filter predicate for a suitably chosen filter. (Contributed by Mario Carneiro, 13-Oct-2015)

	Ref	Expression
Hypotheses	caucfil.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	caucfil.2	⊢ 𝐿 = ( ( 𝑋 FilMap 𝐹 ) ‘ ( ℤ≥ “ 𝑍 ) )
Assertion	caucfil	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ 𝐿 ∈ ( CauFil ‘ 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		caucfil.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		caucfil.2	⊢ 𝐿 = ( ( 𝑋 FilMap 𝐹 ) ‘ ( ℤ≥ “ 𝑍 ) )
3		df-3an	⊢ ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ↔ ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) )
4	1	uztrn2	⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
5	4	adantll	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
6		simpll3	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝐹 : 𝑍 ⟶ 𝑋 )
7	6	fdmd	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → dom 𝐹 = 𝑍 )
8	5 7	eleqtrrd	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ dom 𝐹 )
9	6 5	ffvelcdmd	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 )
10	8 9	jca	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) )
11	10	biantrurd	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ↔ ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ) )
12		uzss	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) → ( ℤ≥ ‘ 𝑘 ) ⊆ ( ℤ≥ ‘ 𝑗 ) )
13	12	adantl	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ℤ≥ ‘ 𝑘 ) ⊆ ( ℤ≥ ‘ 𝑗 ) )
14	13	sseld	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) → 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) )
15	14	pm4.71rd	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ↔ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ) ) )
16	15	imbi1d	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ↔ ( ( 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ) )
17		impexp	⊢ ( ( ( 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ↔ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) → ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ) )
18	16 17	bitrdi	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ↔ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) → ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ) ) )
19	18	ralbidv2	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ) )
20	11 19	bitr3d	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ) )
21	3 20	bitrid	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ) )
22	21	ralbidva	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ) )
23		r19.26-2	⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ∧ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) → ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ) ) ↔ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) → ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ) ) )
24		eleq1w	⊢ ( 𝑢 = 𝑘 → ( 𝑢 ∈ ( ℤ≥ ‘ 𝑚 ) ↔ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ) )
25		fveq2	⊢ ( 𝑢 = 𝑘 → ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑘 ) )
26	25	oveq2d	⊢ ( 𝑢 = 𝑘 → ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑢 ) ) = ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) )
27	26	breq1d	⊢ ( 𝑢 = 𝑘 → ( ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑢 ) ) < 𝑥 ↔ ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ) )
28	24 27	imbi12d	⊢ ( 𝑢 = 𝑘 → ( ( 𝑢 ∈ ( ℤ≥ ‘ 𝑚 ) → ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑢 ) ) < 𝑥 ) ↔ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) → ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ) ) )
29	28	cbvralvw	⊢ ( ∀ 𝑢 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑢 ∈ ( ℤ≥ ‘ 𝑚 ) → ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑢 ) ) < 𝑥 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) → ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ) )
30	29	ralbii	⊢ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑢 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑢 ∈ ( ℤ≥ ‘ 𝑚 ) → ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑢 ) ) < 𝑥 ) ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) → ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ) )
31		fveq2	⊢ ( 𝑚 = 𝑘 → ( ℤ≥ ‘ 𝑚 ) = ( ℤ≥ ‘ 𝑘 ) )
32	31	eleq2d	⊢ ( 𝑚 = 𝑘 → ( 𝑢 ∈ ( ℤ≥ ‘ 𝑚 ) ↔ 𝑢 ∈ ( ℤ≥ ‘ 𝑘 ) ) )
33		fveq2	⊢ ( 𝑚 = 𝑘 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑘 ) )
34	33	oveq1d	⊢ ( 𝑚 = 𝑘 → ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑢 ) ) = ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑢 ) ) )
35	34	breq1d	⊢ ( 𝑚 = 𝑘 → ( ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑢 ) ) < 𝑥 ↔ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑢 ) ) < 𝑥 ) )
36	32 35	imbi12d	⊢ ( 𝑚 = 𝑘 → ( ( 𝑢 ∈ ( ℤ≥ ‘ 𝑚 ) → ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑢 ) ) < 𝑥 ) ↔ ( 𝑢 ∈ ( ℤ≥ ‘ 𝑘 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑢 ) ) < 𝑥 ) ) )
37		eleq1w	⊢ ( 𝑢 = 𝑚 → ( 𝑢 ∈ ( ℤ≥ ‘ 𝑘 ) ↔ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ) )
38		fveq2	⊢ ( 𝑢 = 𝑚 → ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑚 ) )
39	38	oveq2d	⊢ ( 𝑢 = 𝑚 → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑢 ) ) = ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) )
40	39	breq1d	⊢ ( 𝑢 = 𝑚 → ( ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑢 ) ) < 𝑥 ↔ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) )
41	37 40	imbi12d	⊢ ( 𝑢 = 𝑚 → ( ( 𝑢 ∈ ( ℤ≥ ‘ 𝑘 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑢 ) ) < 𝑥 ) ↔ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ) )
42	36 41	cbvral2vw	⊢ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑢 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑢 ∈ ( ℤ≥ ‘ 𝑚 ) → ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑢 ) ) < 𝑥 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) )
43		ralcom	⊢ ( ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) → ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) → ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ) )
44	30 42 43	3bitr3i	⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) → ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ) )
45	44	anbi2i	⊢ ( ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ) ↔ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) → ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ) ) )
46		anidm	⊢ ( ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) )
47	23 45 46	3bitr2i	⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ∧ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) → ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ) ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) )
48		simpll1	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
49		simpll3	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝐹 : 𝑍 ⟶ 𝑋 )
50	1	uztrn2	⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑚 ∈ 𝑍 )
51	50	ad2ant2l	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → 𝑚 ∈ 𝑍 )
52	49 51	ffvelcdmd	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝐹 ‘ 𝑚 ) ∈ 𝑋 )
53	9	adantrr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 )
54		xmetsym	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑚 ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) )
55	48 52 53 54	syl3anc	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) = ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) )
56	55	breq1d	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ↔ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) )
57	56	imbi2d	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) → ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ) ↔ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ) )
58	57	anbi2d	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ∧ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) → ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ) ) ↔ ( ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ∧ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ) ) )
59		jaob	⊢ ( ( ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∨ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ↔ ( ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ∧ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ) )
60		eluzelz	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) → 𝑘 ∈ ℤ )
61		eluzelz	⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) → 𝑚 ∈ ℤ )
62		uztric	⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑚 ∈ ℤ ) → ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∨ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ) )
63	60 61 62	syl2an	⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∨ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ) )
64	63	adantl	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∨ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ) )
65		pm5.5	⊢ ( ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∨ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ) → ( ( ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∨ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) )
66	64 65	syl	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ∨ 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) )
67	59 66	bitr3id	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ∧ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ) ↔ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) )
68	58 67	bitrd	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) ∧ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ( ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ∧ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) → ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ) ) ↔ ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) )
69	68	2ralbidva	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ∧ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) → ( ( 𝐹 ‘ 𝑚 ) 𝐷 ( 𝐹 ‘ 𝑘 ) ) < 𝑥 ) ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) )
70	47 69	bitr3id	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) → ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) )
71	22 70	bitrd	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) )
72	71	rexbidva	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) )
73		uzf	⊢ ℤ≥ : ℤ ⟶ 𝒫 ℤ
74		ffn	⊢ ( ℤ≥ : ℤ ⟶ 𝒫 ℤ → ℤ≥ Fn ℤ )
75	73 74	ax-mp	⊢ ℤ≥ Fn ℤ
76		uzssz	⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
77	1 76	eqsstri	⊢ 𝑍 ⊆ ℤ
78		raleq	⊢ ( 𝑢 = ( ℤ≥ ‘ 𝑗 ) → ( ∀ 𝑚 ∈ 𝑢 ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ↔ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) )
79	78	raleqbi1dv	⊢ ( 𝑢 = ( ℤ≥ ‘ 𝑗 ) → ( ∀ 𝑘 ∈ 𝑢 ∀ 𝑚 ∈ 𝑢 ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) )
80	79	rexima	⊢ ( ( ℤ≥ Fn ℤ ∧ 𝑍 ⊆ ℤ ) → ( ∃ 𝑢 ∈ ( ℤ≥ “ 𝑍 ) ∀ 𝑘 ∈ 𝑢 ∀ 𝑚 ∈ 𝑢 ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) )
81	75 77 80	mp2an	⊢ ( ∃ 𝑢 ∈ ( ℤ≥ “ 𝑍 ) ∀ 𝑘 ∈ 𝑢 ∀ 𝑚 ∈ 𝑢 ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 )
82	72 81	bitr4di	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ↔ ∃ 𝑢 ∈ ( ℤ≥ “ 𝑍 ) ∀ 𝑘 ∈ 𝑢 ∀ 𝑚 ∈ 𝑢 ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) )
83	82	ralbidv	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑢 ∈ ( ℤ≥ “ 𝑍 ) ∀ 𝑘 ∈ 𝑢 ∀ 𝑚 ∈ 𝑢 ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) )
84		elfvdm	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 ∈ dom ∞Met )
85	84	adantr	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ) → 𝑋 ∈ dom ∞Met )
86		cnex	⊢ ℂ ∈ V
87	85 86	jctir	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ) → ( 𝑋 ∈ dom ∞Met ∧ ℂ ∈ V ) )
88		zsscn	⊢ ℤ ⊆ ℂ
89	77 88	sstri	⊢ 𝑍 ⊆ ℂ
90	89	jctr	⊢ ( 𝐹 : 𝑍 ⟶ 𝑋 → ( 𝐹 : 𝑍 ⟶ 𝑋 ∧ 𝑍 ⊆ ℂ ) )
91		elpm2r	⊢ ( ( ( 𝑋 ∈ dom ∞Met ∧ ℂ ∈ V ) ∧ ( 𝐹 : 𝑍 ⟶ 𝑋 ∧ 𝑍 ⊆ ℂ ) ) → 𝐹 ∈ ( 𝑋 ↑pm ℂ ) )
92	87 90 91	syl2an	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) → 𝐹 ∈ ( 𝑋 ↑pm ℂ ) )
93		simpl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
94		simpr	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ) → 𝑀 ∈ ℤ )
95	1 93 94	iscau3	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ) → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ) ) )
96	95	baibd	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ) → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ) )
97	92 96	syldan	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ) )
98	97	3impa	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑋 ∧ ∀ 𝑚 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) ) )
99	2	eleq1i	⊢ ( 𝐿 ∈ ( CauFil ‘ 𝐷 ) ↔ ( ( 𝑋 FilMap 𝐹 ) ‘ ( ℤ≥ “ 𝑍 ) ) ∈ ( CauFil ‘ 𝐷 ) )
100	1	uzfbas	⊢ ( 𝑀 ∈ ℤ → ( ℤ≥ “ 𝑍 ) ∈ ( fBas ‘ 𝑍 ) )
101		fmcfil	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( ℤ≥ “ 𝑍 ) ∈ ( fBas ‘ 𝑍 ) ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) → ( ( ( 𝑋 FilMap 𝐹 ) ‘ ( ℤ≥ “ 𝑍 ) ) ∈ ( CauFil ‘ 𝐷 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑢 ∈ ( ℤ≥ “ 𝑍 ) ∀ 𝑘 ∈ 𝑢 ∀ 𝑚 ∈ 𝑢 ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) )
102	100 101	syl3an2	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) → ( ( ( 𝑋 FilMap 𝐹 ) ‘ ( ℤ≥ “ 𝑍 ) ) ∈ ( CauFil ‘ 𝐷 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑢 ∈ ( ℤ≥ “ 𝑍 ) ∀ 𝑘 ∈ 𝑢 ∀ 𝑚 ∈ 𝑢 ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) )
103	99 102	bitrid	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) → ( 𝐿 ∈ ( CauFil ‘ 𝐷 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑢 ∈ ( ℤ≥ “ 𝑍 ) ∀ 𝑘 ∈ 𝑢 ∀ 𝑚 ∈ 𝑢 ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) )
104	83 98 103	3bitr4d	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ 𝐿 ∈ ( CauFil ‘ 𝐷 ) ) )