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 ) )