Metamath Proof Explorer

Theorem fmcfil

Description: The Cauchy filter condition for a filter map. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Assertion fmcfil ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐡 ∈ ( fBas β€˜ π‘Œ ) ∧ 𝐹 : π‘Œ ⟢ 𝑋 ) β†’ ( ( ( 𝑋 FilMap 𝐹 ) β€˜ 𝐡 ) ∈ ( CauFil β€˜ 𝐷 ) ↔ βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑦 ∈ 𝐡 βˆ€ 𝑧 ∈ 𝑦 βˆ€ 𝑀 ∈ 𝑦 ( ( 𝐹 β€˜ 𝑧 ) 𝐷 ( 𝐹 β€˜ 𝑀 ) ) < π‘₯ ) )

Proof

Step Hyp Ref Expression
1 elfvdm ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ 𝑋 ∈ dom ∞Met )
2 fmval ⊒ ( ( 𝑋 ∈ dom ∞Met ∧ 𝐡 ∈ ( fBas β€˜ π‘Œ ) ∧ 𝐹 : π‘Œ ⟢ 𝑋 ) β†’ ( ( 𝑋 FilMap 𝐹 ) β€˜ 𝐡 ) = ( 𝑋 filGen ran ( 𝑦 ∈ 𝐡 ↦ ( 𝐹 β€œ 𝑦 ) ) ) )
3 1 2 syl3an1 ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐡 ∈ ( fBas β€˜ π‘Œ ) ∧ 𝐹 : π‘Œ ⟢ 𝑋 ) β†’ ( ( 𝑋 FilMap 𝐹 ) β€˜ 𝐡 ) = ( 𝑋 filGen ran ( 𝑦 ∈ 𝐡 ↦ ( 𝐹 β€œ 𝑦 ) ) ) )
4 3 eleq1d ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐡 ∈ ( fBas β€˜ π‘Œ ) ∧ 𝐹 : π‘Œ ⟢ 𝑋 ) β†’ ( ( ( 𝑋 FilMap 𝐹 ) β€˜ 𝐡 ) ∈ ( CauFil β€˜ 𝐷 ) ↔ ( 𝑋 filGen ran ( 𝑦 ∈ 𝐡 ↦ ( 𝐹 β€œ 𝑦 ) ) ) ∈ ( CauFil β€˜ 𝐷 ) ) )
5 simp1 ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐡 ∈ ( fBas β€˜ π‘Œ ) ∧ 𝐹 : π‘Œ ⟢ 𝑋 ) β†’ 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) )
6 simp2 ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐡 ∈ ( fBas β€˜ π‘Œ ) ∧ 𝐹 : π‘Œ ⟢ 𝑋 ) β†’ 𝐡 ∈ ( fBas β€˜ π‘Œ ) )
7 simp3 ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐡 ∈ ( fBas β€˜ π‘Œ ) ∧ 𝐹 : π‘Œ ⟢ 𝑋 ) β†’ 𝐹 : π‘Œ ⟢ 𝑋 )
8 1 3ad2ant1 ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐡 ∈ ( fBas β€˜ π‘Œ ) ∧ 𝐹 : π‘Œ ⟢ 𝑋 ) β†’ 𝑋 ∈ dom ∞Met )
9 eqid ⊒ ran ( 𝑦 ∈ 𝐡 ↦ ( 𝐹 β€œ 𝑦 ) ) = ran ( 𝑦 ∈ 𝐡 ↦ ( 𝐹 β€œ 𝑦 ) )
10 9 fbasrn ⊒ ( ( 𝐡 ∈ ( fBas β€˜ π‘Œ ) ∧ 𝐹 : π‘Œ ⟢ 𝑋 ∧ 𝑋 ∈ dom ∞Met ) β†’ ran ( 𝑦 ∈ 𝐡 ↦ ( 𝐹 β€œ 𝑦 ) ) ∈ ( fBas β€˜ 𝑋 ) )
11 6 7 8 10 syl3anc ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐡 ∈ ( fBas β€˜ π‘Œ ) ∧ 𝐹 : π‘Œ ⟢ 𝑋 ) β†’ ran ( 𝑦 ∈ 𝐡 ↦ ( 𝐹 β€œ 𝑦 ) ) ∈ ( fBas β€˜ 𝑋 ) )
12 fgcfil ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ ran ( 𝑦 ∈ 𝐡 ↦ ( 𝐹 β€œ 𝑦 ) ) ∈ ( fBas β€˜ 𝑋 ) ) β†’ ( ( 𝑋 filGen ran ( 𝑦 ∈ 𝐡 ↦ ( 𝐹 β€œ 𝑦 ) ) ) ∈ ( CauFil β€˜ 𝐷 ) ↔ βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑠 ∈ ran ( 𝑦 ∈ 𝐡 ↦ ( 𝐹 β€œ 𝑦 ) ) βˆ€ 𝑒 ∈ 𝑠 βˆ€ 𝑣 ∈ 𝑠 ( 𝑒 𝐷 𝑣 ) < π‘₯ ) )
13 5 11 12 syl2anc ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐡 ∈ ( fBas β€˜ π‘Œ ) ∧ 𝐹 : π‘Œ ⟢ 𝑋 ) β†’ ( ( 𝑋 filGen ran ( 𝑦 ∈ 𝐡 ↦ ( 𝐹 β€œ 𝑦 ) ) ) ∈ ( CauFil β€˜ 𝐷 ) ↔ βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑠 ∈ ran ( 𝑦 ∈ 𝐡 ↦ ( 𝐹 β€œ 𝑦 ) ) βˆ€ 𝑒 ∈ 𝑠 βˆ€ 𝑣 ∈ 𝑠 ( 𝑒 𝐷 𝑣 ) < π‘₯ ) )
14 imassrn ⊒ ( 𝐹 β€œ 𝑦 ) βŠ† ran 𝐹
15 frn ⊒ ( 𝐹 : π‘Œ ⟢ 𝑋 β†’ ran 𝐹 βŠ† 𝑋 )
16 15 3ad2ant3 ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐡 ∈ ( fBas β€˜ π‘Œ ) ∧ 𝐹 : π‘Œ ⟢ 𝑋 ) β†’ ran 𝐹 βŠ† 𝑋 )
17 14 16 sstrid ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐡 ∈ ( fBas β€˜ π‘Œ ) ∧ 𝐹 : π‘Œ ⟢ 𝑋 ) β†’ ( 𝐹 β€œ 𝑦 ) βŠ† 𝑋 )
18 8 17 ssexd ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐡 ∈ ( fBas β€˜ π‘Œ ) ∧ 𝐹 : π‘Œ ⟢ 𝑋 ) β†’ ( 𝐹 β€œ 𝑦 ) ∈ V )
19 18 ralrimivw ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐡 ∈ ( fBas β€˜ π‘Œ ) ∧ 𝐹 : π‘Œ ⟢ 𝑋 ) β†’ βˆ€ 𝑦 ∈ 𝐡 ( 𝐹 β€œ 𝑦 ) ∈ V )
20 eqid ⊒ ( 𝑦 ∈ 𝐡 ↦ ( 𝐹 β€œ 𝑦 ) ) = ( 𝑦 ∈ 𝐡 ↦ ( 𝐹 β€œ 𝑦 ) )
21 raleq ⊒ ( 𝑠 = ( 𝐹 β€œ 𝑦 ) β†’ ( βˆ€ 𝑣 ∈ 𝑠 ( 𝑒 𝐷 𝑣 ) < π‘₯ ↔ βˆ€ 𝑣 ∈ ( 𝐹 β€œ 𝑦 ) ( 𝑒 𝐷 𝑣 ) < π‘₯ ) )
22 21 raleqbi1dv ⊒ ( 𝑠 = ( 𝐹 β€œ 𝑦 ) β†’ ( βˆ€ 𝑒 ∈ 𝑠 βˆ€ 𝑣 ∈ 𝑠 ( 𝑒 𝐷 𝑣 ) < π‘₯ ↔ βˆ€ 𝑒 ∈ ( 𝐹 β€œ 𝑦 ) βˆ€ 𝑣 ∈ ( 𝐹 β€œ 𝑦 ) ( 𝑒 𝐷 𝑣 ) < π‘₯ ) )
23 20 22 rexrnmptw ⊒ ( βˆ€ 𝑦 ∈ 𝐡 ( 𝐹 β€œ 𝑦 ) ∈ V β†’ ( βˆƒ 𝑠 ∈ ran ( 𝑦 ∈ 𝐡 ↦ ( 𝐹 β€œ 𝑦 ) ) βˆ€ 𝑒 ∈ 𝑠 βˆ€ 𝑣 ∈ 𝑠 ( 𝑒 𝐷 𝑣 ) < π‘₯ ↔ βˆƒ 𝑦 ∈ 𝐡 βˆ€ 𝑒 ∈ ( 𝐹 β€œ 𝑦 ) βˆ€ 𝑣 ∈ ( 𝐹 β€œ 𝑦 ) ( 𝑒 𝐷 𝑣 ) < π‘₯ ) )
24 19 23 syl ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐡 ∈ ( fBas β€˜ π‘Œ ) ∧ 𝐹 : π‘Œ ⟢ 𝑋 ) β†’ ( βˆƒ 𝑠 ∈ ran ( 𝑦 ∈ 𝐡 ↦ ( 𝐹 β€œ 𝑦 ) ) βˆ€ 𝑒 ∈ 𝑠 βˆ€ 𝑣 ∈ 𝑠 ( 𝑒 𝐷 𝑣 ) < π‘₯ ↔ βˆƒ 𝑦 ∈ 𝐡 βˆ€ 𝑒 ∈ ( 𝐹 β€œ 𝑦 ) βˆ€ 𝑣 ∈ ( 𝐹 β€œ 𝑦 ) ( 𝑒 𝐷 𝑣 ) < π‘₯ ) )
25 simpl3 ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐡 ∈ ( fBas β€˜ π‘Œ ) ∧ 𝐹 : π‘Œ ⟢ 𝑋 ) ∧ 𝑦 ∈ 𝐡 ) β†’ 𝐹 : π‘Œ ⟢ 𝑋 )
26 25 ffnd ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐡 ∈ ( fBas β€˜ π‘Œ ) ∧ 𝐹 : π‘Œ ⟢ 𝑋 ) ∧ 𝑦 ∈ 𝐡 ) β†’ 𝐹 Fn π‘Œ )
27 fbelss ⊒ ( ( 𝐡 ∈ ( fBas β€˜ π‘Œ ) ∧ 𝑦 ∈ 𝐡 ) β†’ 𝑦 βŠ† π‘Œ )
28 6 27 sylan ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐡 ∈ ( fBas β€˜ π‘Œ ) ∧ 𝐹 : π‘Œ ⟢ 𝑋 ) ∧ 𝑦 ∈ 𝐡 ) β†’ 𝑦 βŠ† π‘Œ )
29 oveq1 ⊒ ( 𝑒 = ( 𝐹 β€˜ 𝑧 ) β†’ ( 𝑒 𝐷 𝑣 ) = ( ( 𝐹 β€˜ 𝑧 ) 𝐷 𝑣 ) )
30 29 breq1d ⊒ ( 𝑒 = ( 𝐹 β€˜ 𝑧 ) β†’ ( ( 𝑒 𝐷 𝑣 ) < π‘₯ ↔ ( ( 𝐹 β€˜ 𝑧 ) 𝐷 𝑣 ) < π‘₯ ) )
31 30 ralbidv ⊒ ( 𝑒 = ( 𝐹 β€˜ 𝑧 ) β†’ ( βˆ€ 𝑣 ∈ ( 𝐹 β€œ 𝑦 ) ( 𝑒 𝐷 𝑣 ) < π‘₯ ↔ βˆ€ 𝑣 ∈ ( 𝐹 β€œ 𝑦 ) ( ( 𝐹 β€˜ 𝑧 ) 𝐷 𝑣 ) < π‘₯ ) )
32 31 ralima ⊒ ( ( 𝐹 Fn π‘Œ ∧ 𝑦 βŠ† π‘Œ ) β†’ ( βˆ€ 𝑒 ∈ ( 𝐹 β€œ 𝑦 ) βˆ€ 𝑣 ∈ ( 𝐹 β€œ 𝑦 ) ( 𝑒 𝐷 𝑣 ) < π‘₯ ↔ βˆ€ 𝑧 ∈ 𝑦 βˆ€ 𝑣 ∈ ( 𝐹 β€œ 𝑦 ) ( ( 𝐹 β€˜ 𝑧 ) 𝐷 𝑣 ) < π‘₯ ) )
33 26 28 32 syl2anc ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐡 ∈ ( fBas β€˜ π‘Œ ) ∧ 𝐹 : π‘Œ ⟢ 𝑋 ) ∧ 𝑦 ∈ 𝐡 ) β†’ ( βˆ€ 𝑒 ∈ ( 𝐹 β€œ 𝑦 ) βˆ€ 𝑣 ∈ ( 𝐹 β€œ 𝑦 ) ( 𝑒 𝐷 𝑣 ) < π‘₯ ↔ βˆ€ 𝑧 ∈ 𝑦 βˆ€ 𝑣 ∈ ( 𝐹 β€œ 𝑦 ) ( ( 𝐹 β€˜ 𝑧 ) 𝐷 𝑣 ) < π‘₯ ) )
34 oveq2 ⊒ ( 𝑣 = ( 𝐹 β€˜ 𝑀 ) β†’ ( ( 𝐹 β€˜ 𝑧 ) 𝐷 𝑣 ) = ( ( 𝐹 β€˜ 𝑧 ) 𝐷 ( 𝐹 β€˜ 𝑀 ) ) )
35 34 breq1d ⊒ ( 𝑣 = ( 𝐹 β€˜ 𝑀 ) β†’ ( ( ( 𝐹 β€˜ 𝑧 ) 𝐷 𝑣 ) < π‘₯ ↔ ( ( 𝐹 β€˜ 𝑧 ) 𝐷 ( 𝐹 β€˜ 𝑀 ) ) < π‘₯ ) )
36 35 ralima ⊒ ( ( 𝐹 Fn π‘Œ ∧ 𝑦 βŠ† π‘Œ ) β†’ ( βˆ€ 𝑣 ∈ ( 𝐹 β€œ 𝑦 ) ( ( 𝐹 β€˜ 𝑧 ) 𝐷 𝑣 ) < π‘₯ ↔ βˆ€ 𝑀 ∈ 𝑦 ( ( 𝐹 β€˜ 𝑧 ) 𝐷 ( 𝐹 β€˜ 𝑀 ) ) < π‘₯ ) )
37 26 28 36 syl2anc ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐡 ∈ ( fBas β€˜ π‘Œ ) ∧ 𝐹 : π‘Œ ⟢ 𝑋 ) ∧ 𝑦 ∈ 𝐡 ) β†’ ( βˆ€ 𝑣 ∈ ( 𝐹 β€œ 𝑦 ) ( ( 𝐹 β€˜ 𝑧 ) 𝐷 𝑣 ) < π‘₯ ↔ βˆ€ 𝑀 ∈ 𝑦 ( ( 𝐹 β€˜ 𝑧 ) 𝐷 ( 𝐹 β€˜ 𝑀 ) ) < π‘₯ ) )
38 37 ralbidv ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐡 ∈ ( fBas β€˜ π‘Œ ) ∧ 𝐹 : π‘Œ ⟢ 𝑋 ) ∧ 𝑦 ∈ 𝐡 ) β†’ ( βˆ€ 𝑧 ∈ 𝑦 βˆ€ 𝑣 ∈ ( 𝐹 β€œ 𝑦 ) ( ( 𝐹 β€˜ 𝑧 ) 𝐷 𝑣 ) < π‘₯ ↔ βˆ€ 𝑧 ∈ 𝑦 βˆ€ 𝑀 ∈ 𝑦 ( ( 𝐹 β€˜ 𝑧 ) 𝐷 ( 𝐹 β€˜ 𝑀 ) ) < π‘₯ ) )
39 33 38 bitrd ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐡 ∈ ( fBas β€˜ π‘Œ ) ∧ 𝐹 : π‘Œ ⟢ 𝑋 ) ∧ 𝑦 ∈ 𝐡 ) β†’ ( βˆ€ 𝑒 ∈ ( 𝐹 β€œ 𝑦 ) βˆ€ 𝑣 ∈ ( 𝐹 β€œ 𝑦 ) ( 𝑒 𝐷 𝑣 ) < π‘₯ ↔ βˆ€ 𝑧 ∈ 𝑦 βˆ€ 𝑀 ∈ 𝑦 ( ( 𝐹 β€˜ 𝑧 ) 𝐷 ( 𝐹 β€˜ 𝑀 ) ) < π‘₯ ) )
40 39 rexbidva ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐡 ∈ ( fBas β€˜ π‘Œ ) ∧ 𝐹 : π‘Œ ⟢ 𝑋 ) β†’ ( βˆƒ 𝑦 ∈ 𝐡 βˆ€ 𝑒 ∈ ( 𝐹 β€œ 𝑦 ) βˆ€ 𝑣 ∈ ( 𝐹 β€œ 𝑦 ) ( 𝑒 𝐷 𝑣 ) < π‘₯ ↔ βˆƒ 𝑦 ∈ 𝐡 βˆ€ 𝑧 ∈ 𝑦 βˆ€ 𝑀 ∈ 𝑦 ( ( 𝐹 β€˜ 𝑧 ) 𝐷 ( 𝐹 β€˜ 𝑀 ) ) < π‘₯ ) )
41 24 40 bitrd ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐡 ∈ ( fBas β€˜ π‘Œ ) ∧ 𝐹 : π‘Œ ⟢ 𝑋 ) β†’ ( βˆƒ 𝑠 ∈ ran ( 𝑦 ∈ 𝐡 ↦ ( 𝐹 β€œ 𝑦 ) ) βˆ€ 𝑒 ∈ 𝑠 βˆ€ 𝑣 ∈ 𝑠 ( 𝑒 𝐷 𝑣 ) < π‘₯ ↔ βˆƒ 𝑦 ∈ 𝐡 βˆ€ 𝑧 ∈ 𝑦 βˆ€ 𝑀 ∈ 𝑦 ( ( 𝐹 β€˜ 𝑧 ) 𝐷 ( 𝐹 β€˜ 𝑀 ) ) < π‘₯ ) )
42 41 ralbidv ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐡 ∈ ( fBas β€˜ π‘Œ ) ∧ 𝐹 : π‘Œ ⟢ 𝑋 ) β†’ ( βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑠 ∈ ran ( 𝑦 ∈ 𝐡 ↦ ( 𝐹 β€œ 𝑦 ) ) βˆ€ 𝑒 ∈ 𝑠 βˆ€ 𝑣 ∈ 𝑠 ( 𝑒 𝐷 𝑣 ) < π‘₯ ↔ βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑦 ∈ 𝐡 βˆ€ 𝑧 ∈ 𝑦 βˆ€ 𝑀 ∈ 𝑦 ( ( 𝐹 β€˜ 𝑧 ) 𝐷 ( 𝐹 β€˜ 𝑀 ) ) < π‘₯ ) )
43 4 13 42 3bitrd ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐡 ∈ ( fBas β€˜ π‘Œ ) ∧ 𝐹 : π‘Œ ⟢ 𝑋 ) β†’ ( ( ( 𝑋 FilMap 𝐹 ) β€˜ 𝐡 ) ∈ ( CauFil β€˜ 𝐷 ) ↔ βˆ€ π‘₯ ∈ ℝ+ βˆƒ 𝑦 ∈ 𝐡 βˆ€ 𝑧 ∈ 𝑦 βˆ€ 𝑀 ∈ 𝑦 ( ( 𝐹 β€˜ 𝑧 ) 𝐷 ( 𝐹 β€˜ 𝑀 ) ) < π‘₯ ) )