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 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 β€˜ 𝐷 ) ) )