Metamath Proof Explorer

Theorem fmcncfil

Description: The image of a Cauchy filter by a continuous filter map is a Cauchy filter. (Contributed by Thierry Arnoux, 12-Nov-2017)

Ref Expression
Hypotheses fmcncfil.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
fmcncfil.2 ⊢ 𝐾 = ( MetOpen ‘ 𝐸 )
Assertion fmcncfil ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝐵 ∈ ( CauFil ‘ 𝐷 ) ) → ( ( 𝑌 FilMap 𝐹 ) ‘ 𝐵 ) ∈ ( CauFil ‘ 𝐸 ) )

Proof

Step Hyp Ref Expression
1 fmcncfil.1 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 fmcncfil.2 ⊢ 𝐾 = ( MetOpen ‘ 𝐸 )
3 simpl2 ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝐵 ∈ ( CauFil ‘ 𝐷 ) ) → 𝐸 ∈ ( ∞Met ‘ 𝑌 ) )
4 simpl1 ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝐵 ∈ ( CauFil ‘ 𝐷 ) ) → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
5 1 cmetcvg ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐵 ∈ ( CauFil ‘ 𝐷 ) ) → ( 𝐽 fLim 𝐵 ) ≠ ∅ )
6 n0 ⊢ ( ( 𝐽 fLim 𝐵 ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( 𝐽 fLim 𝐵 ) )
7 5 6 sylib ⊢ ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐵 ∈ ( CauFil ‘ 𝐷 ) ) → ∃ 𝑥 𝑥 ∈ ( 𝐽 fLim 𝐵 ) )
8 4 7 sylancom ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝐵 ∈ ( CauFil ‘ 𝐷 ) ) → ∃ 𝑥 𝑥 ∈ ( 𝐽 fLim 𝐵 ) )
9 cmetmet ⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
10 metxmet ⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
11 4 9 10 3syl ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝐵 ∈ ( CauFil ‘ 𝐷 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
12 cfilfil ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ∈ ( CauFil ‘ 𝐷 ) ) → 𝐵 ∈ ( Fil ‘ 𝑋 ) )
13 11 12 sylancom ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝐵 ∈ ( CauFil ‘ 𝐷 ) ) → 𝐵 ∈ ( Fil ‘ 𝑋 ) )
14 1 mopntopon ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
15 11 14 syl ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝐵 ∈ ( CauFil ‘ 𝐷 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
16 2 mopntopon ⊢ ( 𝐸 ∈ ( ∞Met ‘ 𝑌 ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
17 3 16 syl ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝐵 ∈ ( CauFil ‘ 𝐷 ) ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
18 simpl3 ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝐵 ∈ ( CauFil ‘ 𝐷 ) ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
19 cnflf ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑏 ∈ ( Fil ‘ 𝑋 ) ∀ 𝑥 ∈ ( 𝐽 fLim 𝑏 ) ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf 𝑏 ) ‘ 𝐹 ) ) ) )
20 19 simplbda ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ∀ 𝑏 ∈ ( Fil ‘ 𝑋 ) ∀ 𝑥 ∈ ( 𝐽 fLim 𝑏 ) ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf 𝑏 ) ‘ 𝐹 ) )
21 15 17 18 20 syl21anc ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝐵 ∈ ( CauFil ‘ 𝐷 ) ) → ∀ 𝑏 ∈ ( Fil ‘ 𝑋 ) ∀ 𝑥 ∈ ( 𝐽 fLim 𝑏 ) ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf 𝑏 ) ‘ 𝐹 ) )
22 oveq2 ⊢ ( 𝑏 = 𝐵 → ( 𝐽 fLim 𝑏 ) = ( 𝐽 fLim 𝐵 ) )
23 oveq2 ⊢ ( 𝑏 = 𝐵 → ( 𝐾 fLimf 𝑏 ) = ( 𝐾 fLimf 𝐵 ) )
24 23 fveq1d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐾 fLimf 𝑏 ) ‘ 𝐹 ) = ( ( 𝐾 fLimf 𝐵 ) ‘ 𝐹 ) )
25 24 eleq2d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf 𝑏 ) ‘ 𝐹 ) ↔ ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf 𝐵 ) ‘ 𝐹 ) ) )
26 22 25 raleqbidv ⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑥 ∈ ( 𝐽 fLim 𝑏 ) ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf 𝑏 ) ‘ 𝐹 ) ↔ ∀ 𝑥 ∈ ( 𝐽 fLim 𝐵 ) ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf 𝐵 ) ‘ 𝐹 ) ) )
27 26 rspcv ⊢ ( 𝐵 ∈ ( Fil ‘ 𝑋 ) → ( ∀ 𝑏 ∈ ( Fil ‘ 𝑋 ) ∀ 𝑥 ∈ ( 𝐽 fLim 𝑏 ) ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf 𝑏 ) ‘ 𝐹 ) → ∀ 𝑥 ∈ ( 𝐽 fLim 𝐵 ) ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf 𝐵 ) ‘ 𝐹 ) ) )
28 13 21 27 sylc ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝐵 ∈ ( CauFil ‘ 𝐷 ) ) → ∀ 𝑥 ∈ ( 𝐽 fLim 𝐵 ) ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf 𝐵 ) ‘ 𝐹 ) )
29 df-ral ⊢ ( ∀ 𝑥 ∈ ( 𝐽 fLim 𝐵 ) ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf 𝐵 ) ‘ 𝐹 ) ↔ ∀ 𝑥 ( 𝑥 ∈ ( 𝐽 fLim 𝐵 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf 𝐵 ) ‘ 𝐹 ) ) )
30 28 29 sylib ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝐵 ∈ ( CauFil ‘ 𝐷 ) ) → ∀ 𝑥 ( 𝑥 ∈ ( 𝐽 fLim 𝐵 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf 𝐵 ) ‘ 𝐹 ) ) )
31 19.29r ⊢ ( ( ∃ 𝑥 𝑥 ∈ ( 𝐽 fLim 𝐵 ) ∧ ∀ 𝑥 ( 𝑥 ∈ ( 𝐽 fLim 𝐵 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf 𝐵 ) ‘ 𝐹 ) ) ) → ∃ 𝑥 ( 𝑥 ∈ ( 𝐽 fLim 𝐵 ) ∧ ( 𝑥 ∈ ( 𝐽 fLim 𝐵 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf 𝐵 ) ‘ 𝐹 ) ) ) )
32 pm3.35 ⊢ ( ( 𝑥 ∈ ( 𝐽 fLim 𝐵 ) ∧ ( 𝑥 ∈ ( 𝐽 fLim 𝐵 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf 𝐵 ) ‘ 𝐹 ) ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf 𝐵 ) ‘ 𝐹 ) )
33 32 eximi ⊢ ( ∃ 𝑥 ( 𝑥 ∈ ( 𝐽 fLim 𝐵 ) ∧ ( 𝑥 ∈ ( 𝐽 fLim 𝐵 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf 𝐵 ) ‘ 𝐹 ) ) ) → ∃ 𝑥 ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf 𝐵 ) ‘ 𝐹 ) )
34 31 33 syl ⊢ ( ( ∃ 𝑥 𝑥 ∈ ( 𝐽 fLim 𝐵 ) ∧ ∀ 𝑥 ( 𝑥 ∈ ( 𝐽 fLim 𝐵 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf 𝐵 ) ‘ 𝐹 ) ) ) → ∃ 𝑥 ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf 𝐵 ) ‘ 𝐹 ) )
35 8 30 34 syl2anc ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝐵 ∈ ( CauFil ‘ 𝐷 ) ) → ∃ 𝑥 ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf 𝐵 ) ‘ 𝐹 ) )
36 1 2 metcn ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑒 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐷 𝑦 ) < 𝑑 → ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐹 ‘ 𝑦 ) ) < 𝑒 ) ) ) )
37 36 biimpa ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑌 ) ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑒 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐷 𝑦 ) < 𝑑 → ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐹 ‘ 𝑦 ) ) < 𝑒 ) ) )
38 11 3 18 37 syl21anc ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝐵 ∈ ( CauFil ‘ 𝐷 ) ) → ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑒 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐷 𝑦 ) < 𝑑 → ( ( 𝐹 ‘ 𝑥 ) 𝐸 ( 𝐹 ‘ 𝑦 ) ) < 𝑒 ) ) )
39 38 simpld ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝐵 ∈ ( CauFil ‘ 𝐷 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
40 flfval ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐵 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ( 𝐾 fLimf 𝐵 ) ‘ 𝐹 ) = ( 𝐾 fLim ( ( 𝑌 FilMap 𝐹 ) ‘ 𝐵 ) ) )
41 17 13 39 40 syl3anc ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝐵 ∈ ( CauFil ‘ 𝐷 ) ) → ( ( 𝐾 fLimf 𝐵 ) ‘ 𝐹 ) = ( 𝐾 fLim ( ( 𝑌 FilMap 𝐹 ) ‘ 𝐵 ) ) )
42 41 eleq2d ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝐵 ∈ ( CauFil ‘ 𝐷 ) ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf 𝐵 ) ‘ 𝐹 ) ↔ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐾 fLim ( ( 𝑌 FilMap 𝐹 ) ‘ 𝐵 ) ) ) )
43 42 exbidv ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝐵 ∈ ( CauFil ‘ 𝐷 ) ) → ( ∃ 𝑥 ( 𝐹 ‘ 𝑥 ) ∈ ( ( 𝐾 fLimf 𝐵 ) ‘ 𝐹 ) ↔ ∃ 𝑥 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐾 fLim ( ( 𝑌 FilMap 𝐹 ) ‘ 𝐵 ) ) ) )
44 35 43 mpbid ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝐵 ∈ ( CauFil ‘ 𝐷 ) ) → ∃ 𝑥 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐾 fLim ( ( 𝑌 FilMap 𝐹 ) ‘ 𝐵 ) ) )
45 2 flimcfil ⊢ ( ( 𝐸 ∈ ( ∞Met ‘ 𝑌 ) ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐾 fLim ( ( 𝑌 FilMap 𝐹 ) ‘ 𝐵 ) ) ) → ( ( 𝑌 FilMap 𝐹 ) ‘ 𝐵 ) ∈ ( CauFil ‘ 𝐸 ) )
46 45 ex ⊢ ( 𝐸 ∈ ( ∞Met ‘ 𝑌 ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐾 fLim ( ( 𝑌 FilMap 𝐹 ) ‘ 𝐵 ) ) → ( ( 𝑌 FilMap 𝐹 ) ‘ 𝐵 ) ∈ ( CauFil ‘ 𝐸 ) ) )
47 46 exlimdv ⊢ ( 𝐸 ∈ ( ∞Met ‘ 𝑌 ) → ( ∃ 𝑥 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐾 fLim ( ( 𝑌 FilMap 𝐹 ) ‘ 𝐵 ) ) → ( ( 𝑌 FilMap 𝐹 ) ‘ 𝐵 ) ∈ ( CauFil ‘ 𝐸 ) ) )
48 3 44 47 sylc ⊢ ( ( ( 𝐷 ∈ ( CMet ‘ 𝑋 ) ∧ 𝐸 ∈ ( ∞Met ‘ 𝑌 ) ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ 𝐵 ∈ ( CauFil ‘ 𝐷 ) ) → ( ( 𝑌 FilMap 𝐹 ) ‘ 𝐵 ) ∈ ( CauFil ‘ 𝐸 ) )