Metamath Proof Explorer

Theorem iscfil2

Description: The property of being a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015)

Ref Expression
Assertion iscfil2 ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ↔ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐹 ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( 𝑧 𝐷 𝑤 ) < 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 iscfil ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ↔ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐹 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ) )
2 xmetf ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
3 2 ad3antrrr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐹 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
4 3 ffund ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐹 ) → Fun 𝐷 )
5 filelss ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐹 ) → 𝑦 ⊆ 𝑋 )
6 5 ad4ant24 ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐹 ) → 𝑦 ⊆ 𝑋 )
7 xpss12 ⊢ ( ( 𝑦 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑋 ) → ( 𝑦 × 𝑦 ) ⊆ ( 𝑋 × 𝑋 ) )
8 6 6 7 syl2anc ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐹 ) → ( 𝑦 × 𝑦 ) ⊆ ( 𝑋 × 𝑋 ) )
9 3 fdmd ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐹 ) → dom 𝐷 = ( 𝑋 × 𝑋 ) )
10 8 9 sseqtrrd ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐹 ) → ( 𝑦 × 𝑦 ) ⊆ dom 𝐷 )
11 funimassov ⊢ ( ( Fun 𝐷 ∧ ( 𝑦 × 𝑦 ) ⊆ dom 𝐷 ) → ( ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ↔ ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( 𝑧 𝐷 𝑤 ) ∈ ( 0 [,) 𝑥 ) ) )
12 4 10 11 syl2anc ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐹 ) → ( ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ↔ ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( 𝑧 𝐷 𝑤 ) ∈ ( 0 [,) 𝑥 ) ) )
13 0xr ⊢ 0 ∈ ℝ*
14 13 a1i ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐹 ) ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦 ) ) → 0 ∈ ℝ* )
15 simpllr ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐹 ) ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦 ) ) → 𝑥 ∈ ℝ+ )
16 15 rpxrd ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐹 ) ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦 ) ) → 𝑥 ∈ ℝ* )
17 simp-4l ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐹 ) ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
18 6 sselda ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐹 ) ∧ 𝑧 ∈ 𝑦 ) → 𝑧 ∈ 𝑋 )
19 18 adantrr ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐹 ) ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦 ) ) → 𝑧 ∈ 𝑋 )
20 6 sselda ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐹 ) ∧ 𝑤 ∈ 𝑦 ) → 𝑤 ∈ 𝑋 )
21 20 adantrl ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐹 ) ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦 ) ) → 𝑤 ∈ 𝑋 )
22 xmetcl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) → ( 𝑧 𝐷 𝑤 ) ∈ ℝ* )
23 17 19 21 22 syl3anc ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐹 ) ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦 ) ) → ( 𝑧 𝐷 𝑤 ) ∈ ℝ* )
24 xmetge0 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) → 0 ≤ ( 𝑧 𝐷 𝑤 ) )
25 17 19 21 24 syl3anc ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐹 ) ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦 ) ) → 0 ≤ ( 𝑧 𝐷 𝑤 ) )
26 elico1 ⊢ ( ( 0 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) → ( ( 𝑧 𝐷 𝑤 ) ∈ ( 0 [,) 𝑥 ) ↔ ( ( 𝑧 𝐷 𝑤 ) ∈ ℝ* ∧ 0 ≤ ( 𝑧 𝐷 𝑤 ) ∧ ( 𝑧 𝐷 𝑤 ) < 𝑥 ) ) )
27 df-3an ⊢ ( ( ( 𝑧 𝐷 𝑤 ) ∈ ℝ* ∧ 0 ≤ ( 𝑧 𝐷 𝑤 ) ∧ ( 𝑧 𝐷 𝑤 ) < 𝑥 ) ↔ ( ( ( 𝑧 𝐷 𝑤 ) ∈ ℝ* ∧ 0 ≤ ( 𝑧 𝐷 𝑤 ) ) ∧ ( 𝑧 𝐷 𝑤 ) < 𝑥 ) )
28 26 27 bitrdi ⊢ ( ( 0 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) → ( ( 𝑧 𝐷 𝑤 ) ∈ ( 0 [,) 𝑥 ) ↔ ( ( ( 𝑧 𝐷 𝑤 ) ∈ ℝ* ∧ 0 ≤ ( 𝑧 𝐷 𝑤 ) ) ∧ ( 𝑧 𝐷 𝑤 ) < 𝑥 ) ) )
29 28 baibd ⊢ ( ( ( 0 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) ∧ ( ( 𝑧 𝐷 𝑤 ) ∈ ℝ* ∧ 0 ≤ ( 𝑧 𝐷 𝑤 ) ) ) → ( ( 𝑧 𝐷 𝑤 ) ∈ ( 0 [,) 𝑥 ) ↔ ( 𝑧 𝐷 𝑤 ) < 𝑥 ) )
30 14 16 23 25 29 syl22anc ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐹 ) ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦 ) ) → ( ( 𝑧 𝐷 𝑤 ) ∈ ( 0 [,) 𝑥 ) ↔ ( 𝑧 𝐷 𝑤 ) < 𝑥 ) )
31 30 2ralbidva ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐹 ) → ( ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( 𝑧 𝐷 𝑤 ) ∈ ( 0 [,) 𝑥 ) ↔ ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( 𝑧 𝐷 𝑤 ) < 𝑥 ) )
32 12 31 bitrd ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝐹 ) → ( ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ↔ ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( 𝑧 𝐷 𝑤 ) < 𝑥 ) )
33 32 rexbidva ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) ∧ 𝑥 ∈ ℝ+ ) → ( ∃ 𝑦 ∈ 𝐹 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ↔ ∃ 𝑦 ∈ 𝐹 ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( 𝑧 𝐷 𝑤 ) < 𝑥 ) )
34 33 ralbidva ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐹 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐹 ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( 𝑧 𝐷 𝑤 ) < 𝑥 ) )
35 34 pm5.32da ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐹 ( 𝐷 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) ) ↔ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐹 ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( 𝑧 𝐷 𝑤 ) < 𝑥 ) ) )
36 1 35 bitrd ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ↔ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝐹 ∀ 𝑧 ∈ 𝑦 ∀ 𝑤 ∈ 𝑦 ( 𝑧 𝐷 𝑤 ) < 𝑥 ) ) )