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

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 
|- .~ = ( `' D " RR )
Assertion xmetec 
|- ( ( D e. ( *Met ` X ) /\ P e. X ) -> [ P ] .~ = ( P ( ball ` D ) +oo ) )

Proof

Step Hyp Ref Expression
1 xmeter.1 
 |-  .~ = ( `' D " RR )
2 1 xmeterval 
 |-  ( D e. ( *Met ` X ) -> ( P .~ x <-> ( P e. X /\ x e. X /\ ( P D x ) e. RR ) ) )
3 3anass 
 |-  ( ( P e. X /\ x e. X /\ ( P D x ) e. RR ) <-> ( P e. X /\ ( x e. X /\ ( P D x ) e. RR ) ) )
4 3 baib 
 |-  ( P e. X -> ( ( P e. X /\ x e. X /\ ( P D x ) e. RR ) <-> ( x e. X /\ ( P D x ) e. RR ) ) )
5 2 4 sylan9bb 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X ) -> ( P .~ x <-> ( x e. X /\ ( P D x ) e. RR ) ) )
6 vex 
 |-  x e. _V
7 6 a1i 
 |-  ( D e. ( *Met ` X ) -> x e. _V )
8 elecg 
 |-  ( ( x e. _V /\ P e. X ) -> ( x e. [ P ] .~ <-> P .~ x ) )
9 7 8 sylan 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X ) -> ( x e. [ P ] .~ <-> P .~ x ) )
10 xblpnf 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X ) -> ( x e. ( P ( ball ` D ) +oo ) <-> ( x e. X /\ ( P D x ) e. RR ) ) )
11 5 9 10 3bitr4d 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X ) -> ( x e. [ P ] .~ <-> x e. ( P ( ball ` D ) +oo ) ) )
12 11 eqrdv 
 |-  ( ( D e. ( *Met ` X ) /\ P e. X ) -> [ P ] .~ = ( P ( ball ` D ) +oo ) )