This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝐷 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( ( 𝐹 ‘ 𝑧 ) 𝐷 ( 𝐹 ‘ 𝑤 ) ) < 𝑥 ) )