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 ‘ 𝐷 ) ∧ 𝑅 ∈ ℝ+ ) → ∃ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑦 𝐷 𝑧 ) < 𝑅 )