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

Metamath Proof Explorer

Theorem cfili

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

Ref Expression
Assertion cfili ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) → ∃ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑦 𝐷 𝑧 ) < 𝑅 )

Proof

Step Hyp Ref Expression
1 df-cfil ⊢ CauFil = ( 𝑑 ∈ ∪ ran ∞Met ↦ { 𝑓 ∈ ( Fil ‘ dom dom 𝑑 ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ 𝑓 ( 𝑑 “ ( 𝑦 × 𝑦 ) ) ⊆ ( 0 [,) 𝑥 ) } )
2 1 mptrcl ⊢ ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) → 𝐷 ∈ ∪ ran ∞Met )
3 xmetunirn ⊢ ( 𝐷 ∈ ∪ ran ∞Met ↔ 𝐷 ∈ ( ∞Met ‘ dom dom 𝐷 ) )
4 2 3 sylib ⊢ ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) → 𝐷 ∈ ( ∞Met ‘ dom dom 𝐷 ) )
5 iscfil2 ⊢ ( 𝐷 ∈ ( ∞Met ‘ dom dom 𝐷 ) → ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ↔ ( 𝐹 ∈ ( Fil ‘ dom dom 𝐷 ) ∧ ∀ 𝑟 ∈ ℝ+ ∃ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑦 𝐷 𝑧 ) < 𝑟 ) ) )
6 4 5 syl ⊢ ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) → ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ↔ ( 𝐹 ∈ ( Fil ‘ dom dom 𝐷 ) ∧ ∀ 𝑟 ∈ ℝ+ ∃ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑦 𝐷 𝑧 ) < 𝑟 ) ) )
7 6 ibi ⊢ ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) → ( 𝐹 ∈ ( Fil ‘ dom dom 𝐷 ) ∧ ∀ 𝑟 ∈ ℝ+ ∃ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑦 𝐷 𝑧 ) < 𝑟 ) )
8 7 simprd ⊢ ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) → ∀ 𝑟 ∈ ℝ+ ∃ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑦 𝐷 𝑧 ) < 𝑟 )
9 breq2 ⊢ ( 𝑟 = 𝑅 → ( ( 𝑦 𝐷 𝑧 ) < 𝑟 ↔ ( 𝑦 𝐷 𝑧 ) < 𝑅 ) )
10 9 2ralbidv ⊢ ( 𝑟 = 𝑅 → ( ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑦 𝐷 𝑧 ) < 𝑟 ↔ ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑦 𝐷 𝑧 ) < 𝑅 ) )
11 10 rexbidv ⊢ ( 𝑟 = 𝑅 → ( ∃ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑦 𝐷 𝑧 ) < 𝑟 ↔ ∃ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑦 𝐷 𝑧 ) < 𝑅 ) )
12 11 rspccva ⊢ ( ( ∀ 𝑟 ∈ ℝ+ ∃ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑦 𝐷 𝑧 ) < 𝑟 ∧ 𝑅 ∈ ℝ+ ) → ∃ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑦 𝐷 𝑧 ) < 𝑅 )
13 8 12 sylan ⊢ ( ( 𝐹 ∈ ( CauFil ‘ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) → ∃ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑦 𝐷 𝑧 ) < 𝑅 )