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