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

Metamath Proof Explorer

Theorem fmucnd

Description: The image of a Cauchy filter base by an uniformly continuous function is a Cauchy filter base. Deduction form. Proposition 3 of BourbakiTop1 p. II.13. (Contributed by Thierry Arnoux, 18-Nov-2017)

Ref Expression
Hypotheses fmucnd.1 ⊢ ( 𝜑 → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
fmucnd.2 ⊢ ( 𝜑 → 𝑉 ∈ ( UnifOn ‘ 𝑌 ) )
fmucnd.3 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 Cnu 𝑉 ) )
fmucnd.4 ⊢ ( 𝜑 → 𝐶 ∈ ( CauFilu ‘ 𝑈 ) )
fmucnd.5 ⊢ 𝐷 = ran ( 𝑎 ∈ 𝐶 ↦ ( 𝐹 “ 𝑎 ) )
Assertion fmucnd ( 𝜑 → 𝐷 ∈ ( CauFilu ‘ 𝑉 ) )

Proof

Step Hyp Ref Expression
1 fmucnd.1 ⊢ ( 𝜑 → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
2 fmucnd.2 ⊢ ( 𝜑 → 𝑉 ∈ ( UnifOn ‘ 𝑌 ) )
3 fmucnd.3 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 Cnu 𝑉 ) )
4 fmucnd.4 ⊢ ( 𝜑 → 𝐶 ∈ ( CauFilu ‘ 𝑈 ) )
5 fmucnd.5 ⊢ 𝐷 = ran ( 𝑎 ∈ 𝐶 ↦ ( 𝐹 “ 𝑎 ) )
6 cfilufbas ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐶 ∈ ( CauFilu ‘ 𝑈 ) ) → 𝐶 ∈ ( fBas ‘ 𝑋 ) )
7 1 4 6 syl2anc ⊢ ( 𝜑 → 𝐶 ∈ ( fBas ‘ 𝑋 ) )
8 isucn ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ ( UnifOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝑈 Cnu 𝑉 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑣 ∈ 𝑉 ∃ 𝑟 ∈ 𝑈 ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝑟 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑣 ( 𝐹 ‘ 𝑦 ) ) ) ) )
9 8 simprbda ⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ ( UnifOn ‘ 𝑌 ) ) ∧ 𝐹 ∈ ( 𝑈 Cnu 𝑉 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
10 1 2 3 9 syl21anc ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑌 )
11 2 elfvexd ⊢ ( 𝜑 → 𝑌 ∈ V )
12 5 fbasrn ⊢ ( ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑌 ∈ V ) → 𝐷 ∈ ( fBas ‘ 𝑌 ) )
13 7 10 11 12 syl3anc ⊢ ( 𝜑 → 𝐷 ∈ ( fBas ‘ 𝑌 ) )
14 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐶 ) ∧ ( 𝑎 × 𝑎 ) ⊆ ( ◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) “ 𝑣 ) ) → 𝑎 ∈ 𝐶 )
15 eqid ⊢ ( 𝐹 “ 𝑎 ) = ( 𝐹 “ 𝑎 )
16 imaeq2 ⊢ ( 𝑐 = 𝑎 → ( 𝐹 “ 𝑐 ) = ( 𝐹 “ 𝑎 ) )
17 16 rspceeqv ⊢ ( ( 𝑎 ∈ 𝐶 ∧ ( 𝐹 “ 𝑎 ) = ( 𝐹 “ 𝑎 ) ) → ∃ 𝑐 ∈ 𝐶 ( 𝐹 “ 𝑎 ) = ( 𝐹 “ 𝑐 ) )
18 14 15 17 sylancl ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐶 ) ∧ ( 𝑎 × 𝑎 ) ⊆ ( ◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) “ 𝑣 ) ) → ∃ 𝑐 ∈ 𝐶 ( 𝐹 “ 𝑎 ) = ( 𝐹 “ 𝑐 ) )
19 imaexg ⊢ ( 𝐹 ∈ ( 𝑈 Cnu 𝑉 ) → ( 𝐹 “ 𝑎 ) ∈ V )
20 eqid ⊢ ( 𝑐 ∈ 𝐶 ↦ ( 𝐹 “ 𝑐 ) ) = ( 𝑐 ∈ 𝐶 ↦ ( 𝐹 “ 𝑐 ) )
21 20 elrnmpt ⊢ ( ( 𝐹 “ 𝑎 ) ∈ V → ( ( 𝐹 “ 𝑎 ) ∈ ran ( 𝑐 ∈ 𝐶 ↦ ( 𝐹 “ 𝑐 ) ) ↔ ∃ 𝑐 ∈ 𝐶 ( 𝐹 “ 𝑎 ) = ( 𝐹 “ 𝑐 ) ) )
22 3 19 21 3syl ⊢ ( 𝜑 → ( ( 𝐹 “ 𝑎 ) ∈ ran ( 𝑐 ∈ 𝐶 ↦ ( 𝐹 “ 𝑐 ) ) ↔ ∃ 𝑐 ∈ 𝐶 ( 𝐹 “ 𝑎 ) = ( 𝐹 “ 𝑐 ) ) )
23 22 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐶 ) ∧ ( 𝑎 × 𝑎 ) ⊆ ( ◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) “ 𝑣 ) ) → ( ( 𝐹 “ 𝑎 ) ∈ ran ( 𝑐 ∈ 𝐶 ↦ ( 𝐹 “ 𝑐 ) ) ↔ ∃ 𝑐 ∈ 𝐶 ( 𝐹 “ 𝑎 ) = ( 𝐹 “ 𝑐 ) ) )
24 18 23 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐶 ) ∧ ( 𝑎 × 𝑎 ) ⊆ ( ◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) “ 𝑣 ) ) → ( 𝐹 “ 𝑎 ) ∈ ran ( 𝑐 ∈ 𝐶 ↦ ( 𝐹 “ 𝑐 ) ) )
25 imaeq2 ⊢ ( 𝑎 = 𝑐 → ( 𝐹 “ 𝑎 ) = ( 𝐹 “ 𝑐 ) )
26 25 cbvmptv ⊢ ( 𝑎 ∈ 𝐶 ↦ ( 𝐹 “ 𝑎 ) ) = ( 𝑐 ∈ 𝐶 ↦ ( 𝐹 “ 𝑐 ) )
27 26 rneqi ⊢ ran ( 𝑎 ∈ 𝐶 ↦ ( 𝐹 “ 𝑎 ) ) = ran ( 𝑐 ∈ 𝐶 ↦ ( 𝐹 “ 𝑐 ) )
28 5 27 eqtri ⊢ 𝐷 = ran ( 𝑐 ∈ 𝐶 ↦ ( 𝐹 “ 𝑐 ) )
29 24 28 eleqtrrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐶 ) ∧ ( 𝑎 × 𝑎 ) ⊆ ( ◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) “ 𝑣 ) ) → ( 𝐹 “ 𝑎 ) ∈ 𝐷 )
30 10 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝑋 )
31 30 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐶 ) ∧ ( 𝑎 × 𝑎 ) ⊆ ( ◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) “ 𝑣 ) ) → 𝐹 Fn 𝑋 )
32 fbelss ⊢ ( ( 𝐶 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑎 ∈ 𝐶 ) → 𝑎 ⊆ 𝑋 )
33 7 32 sylan ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐶 ) → 𝑎 ⊆ 𝑋 )
34 33 ad4ant13 ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐶 ) ∧ ( 𝑎 × 𝑎 ) ⊆ ( ◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) “ 𝑣 ) ) → 𝑎 ⊆ 𝑋 )
35 fmucndlem ⊢ ( ( 𝐹 Fn 𝑋 ∧ 𝑎 ⊆ 𝑋 ) → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) “ ( 𝑎 × 𝑎 ) ) = ( ( 𝐹 “ 𝑎 ) × ( 𝐹 “ 𝑎 ) ) )
36 31 34 35 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐶 ) ∧ ( 𝑎 × 𝑎 ) ⊆ ( ◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) “ 𝑣 ) ) → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) “ ( 𝑎 × 𝑎 ) ) = ( ( 𝐹 “ 𝑎 ) × ( 𝐹 “ 𝑎 ) ) )
37 eqid ⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ )
38 37 mpofun ⊢ Fun ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ )
39 funimass2 ⊢ ( ( Fun ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) ∧ ( 𝑎 × 𝑎 ) ⊆ ( ◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) “ 𝑣 ) ) → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) “ ( 𝑎 × 𝑎 ) ) ⊆ 𝑣 )
40 38 39 mpan ⊢ ( ( 𝑎 × 𝑎 ) ⊆ ( ◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) “ 𝑣 ) → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) “ ( 𝑎 × 𝑎 ) ) ⊆ 𝑣 )
41 40 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐶 ) ∧ ( 𝑎 × 𝑎 ) ⊆ ( ◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) “ 𝑣 ) ) → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) “ ( 𝑎 × 𝑎 ) ) ⊆ 𝑣 )
42 36 41 eqsstrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐶 ) ∧ ( 𝑎 × 𝑎 ) ⊆ ( ◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) “ 𝑣 ) ) → ( ( 𝐹 “ 𝑎 ) × ( 𝐹 “ 𝑎 ) ) ⊆ 𝑣 )
43 id ⊢ ( 𝑏 = ( 𝐹 “ 𝑎 ) → 𝑏 = ( 𝐹 “ 𝑎 ) )
44 43 sqxpeqd ⊢ ( 𝑏 = ( 𝐹 “ 𝑎 ) → ( 𝑏 × 𝑏 ) = ( ( 𝐹 “ 𝑎 ) × ( 𝐹 “ 𝑎 ) ) )
45 44 sseq1d ⊢ ( 𝑏 = ( 𝐹 “ 𝑎 ) → ( ( 𝑏 × 𝑏 ) ⊆ 𝑣 ↔ ( ( 𝐹 “ 𝑎 ) × ( 𝐹 “ 𝑎 ) ) ⊆ 𝑣 ) )
46 45 rspcev ⊢ ( ( ( 𝐹 “ 𝑎 ) ∈ 𝐷 ∧ ( ( 𝐹 “ 𝑎 ) × ( 𝐹 “ 𝑎 ) ) ⊆ 𝑣 ) → ∃ 𝑏 ∈ 𝐷 ( 𝑏 × 𝑏 ) ⊆ 𝑣 )
47 29 42 46 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐶 ) ∧ ( 𝑎 × 𝑎 ) ⊆ ( ◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) “ 𝑣 ) ) → ∃ 𝑏 ∈ 𝐷 ( 𝑏 × 𝑏 ) ⊆ 𝑣 )
48 1 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
49 4 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → 𝐶 ∈ ( CauFilu ‘ 𝑈 ) )
50 2 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → 𝑉 ∈ ( UnifOn ‘ 𝑌 ) )
51 3 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → 𝐹 ∈ ( 𝑈 Cnu 𝑉 ) )
52 simpr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ 𝑉 )
53 nfcv ⊢ Ⅎ 𝑠 ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩
54 nfcv ⊢ Ⅎ 𝑡 ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩
55 nfcv ⊢ Ⅎ 𝑥 ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐹 ‘ 𝑡 ) ⟩
56 nfcv ⊢ Ⅎ 𝑦 ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐹 ‘ 𝑡 ) ⟩
57 simpl ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 𝑡 ) → 𝑥 = 𝑠 )
58 57 fveq2d ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 𝑡 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑠 ) )
59 simpr ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 𝑡 ) → 𝑦 = 𝑡 )
60 59 fveq2d ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 𝑡 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑡 ) )
61 58 60 opeq12d ⊢ ( ( 𝑥 = 𝑠 ∧ 𝑦 = 𝑡 ) → ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ = ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐹 ‘ 𝑡 ) ⟩ )
62 53 54 55 56 61 cbvmpo ⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) = ( 𝑠 ∈ 𝑋 , 𝑡 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑠 ) , ( 𝐹 ‘ 𝑡 ) ⟩ )
63 48 50 51 52 62 ucnprima ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ( ◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) “ 𝑣 ) ∈ 𝑈 )
64 cfiluexsm ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝐶 ∈ ( CauFilu ‘ 𝑈 ) ∧ ( ◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) “ 𝑣 ) ∈ 𝑈 ) → ∃ 𝑎 ∈ 𝐶 ( 𝑎 × 𝑎 ) ⊆ ( ◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) “ 𝑣 ) )
65 48 49 63 64 syl3anc ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ∃ 𝑎 ∈ 𝐶 ( 𝑎 × 𝑎 ) ⊆ ( ◡ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ) “ 𝑣 ) )
66 47 65 r19.29a ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑉 ) → ∃ 𝑏 ∈ 𝐷 ( 𝑏 × 𝑏 ) ⊆ 𝑣 )
67 66 ralrimiva ⊢ ( 𝜑 → ∀ 𝑣 ∈ 𝑉 ∃ 𝑏 ∈ 𝐷 ( 𝑏 × 𝑏 ) ⊆ 𝑣 )
68 iscfilu ⊢ ( 𝑉 ∈ ( UnifOn ‘ 𝑌 ) → ( 𝐷 ∈ ( CauFilu ‘ 𝑉 ) ↔ ( 𝐷 ∈ ( fBas ‘ 𝑌 ) ∧ ∀ 𝑣 ∈ 𝑉 ∃ 𝑏 ∈ 𝐷 ( 𝑏 × 𝑏 ) ⊆ 𝑣 ) ) )
69 2 68 syl ⊢ ( 𝜑 → ( 𝐷 ∈ ( CauFilu ‘ 𝑉 ) ↔ ( 𝐷 ∈ ( fBas ‘ 𝑌 ) ∧ ∀ 𝑣 ∈ 𝑉 ∃ 𝑏 ∈ 𝐷 ( 𝑏 × 𝑏 ) ⊆ 𝑣 ) ) )
70 13 67 69 mpbir2and ⊢ ( 𝜑 → 𝐷 ∈ ( CauFilu ‘ 𝑉 ) )