Theorem xmetec

Description: The equivalence classes under the finite separation equivalence relation are infinity balls. Thus, by erdisj , infinity balls are either identical or disjoint, quite unlike the usual situation with Euclidean balls which admit many kinds of overlap. (Contributed by Mario Carneiro, 24-Aug-2015)

	Ref	Expression
Hypothesis	xmeter.1	⊢ ∼ = ( ◡ 𝐷 “ ℝ )
Assertion	xmetec	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → [ 𝑃 ] ∼ = ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		xmeter.1	⊢ ∼ = ( ◡ 𝐷 “ ℝ )
2	1	xmeterval	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑃 ∼ 𝑥 ↔ ( 𝑃 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) ∈ ℝ ) ) )
3		3anass	⊢ ( ( 𝑃 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) ∈ ℝ ) ↔ ( 𝑃 ∈ 𝑋 ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) ∈ ℝ ) ) )
4	3	baib	⊢ ( 𝑃 ∈ 𝑋 → ( ( 𝑃 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) ∈ ℝ ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) ∈ ℝ ) ) )
5	2 4	sylan9bb	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝑃 ∼ 𝑥 ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) ∈ ℝ ) ) )
6		vex	⊢ 𝑥 ∈ V
7	6	a1i	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑥 ∈ V )
8		elecg	⊢ ( ( 𝑥 ∈ V ∧ 𝑃 ∈ 𝑋 ) → ( 𝑥 ∈ [ 𝑃 ] ∼ ↔ 𝑃 ∼ 𝑥 ) )
9	7 8	sylan	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝑥 ∈ [ 𝑃 ] ∼ ↔ 𝑃 ∼ 𝑥 ) )
10		xblpnf	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) ∈ ℝ ) ) )
11	5 9 10	3bitr4d	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝑥 ∈ [ 𝑃 ] ∼ ↔ 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) ) )
12	11	eqrdv	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ) → [ 𝑃 ] ∼ = ( 𝑃 ( ball ‘ 𝐷 ) +∞ ) )