Metamath Proof Explorer

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 β€˜ 𝐷 ) +∞ ) )