Metamath Proof Explorer

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 ffvelrnd ⊢ ( ( ( ( 𝐷 ∈ ( ∞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 syl5bb ⊢ ( ( ( ( 𝐷 ∈ ( ∞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 ffvelrnd ⊢ ( ( ( ( 𝐷 ∈ ( ∞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 syl5bb ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) → ( 𝐿 ∈ ( CauFil ‘ 𝐷 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑢 ∈ ( ℤ≥ “ 𝑍 ) ∀ 𝑘 ∈ 𝑢 ∀ 𝑚 ∈ 𝑢 ( ( 𝐹 ‘ 𝑘 ) 𝐷 ( 𝐹 ‘ 𝑚 ) ) < 𝑥 ) )
104 83 98 103 3bitr4d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑀 ∈ ℤ ∧ 𝐹 : 𝑍 ⟶ 𝑋 ) → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ 𝐿 ∈ ( CauFil ‘ 𝐷 ) ) )