Theorem metequiv 9158

Description: Two ways of saying that two metrics generate the same topology. Two metrics satisfying the right-hand side are said to be (topologically) equivalent. (Contributed by Jeffrey Hankins, 21-Jun-2009.)

Hypotheses

Ref	Expression
metequiv.1	|- X = dom dom C
metequiv.2	|- Y = dom dom D
metequiv.3	|- J = (Open` C)
metequiv.4	|- K = (Open` D)

Assertion

Ref	Expression
metequiv	|- ((C e. Met /\ D e. Met) -> (J = K <-> (X = Y /\ A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))))

Distinct variable groups:   s,r,x,C   D,r,s,x   J,r,s,x   K,r,s,x   X,r,s,x   Y,r,s,x

Proof of Theorem metequiv

Step	Hyp	Ref	Expression
1		unieq 3185	. . . . . 6 |- (J = K -> U.J = U.K)
2	1	adantl 424	. . . . 5 |- (((C e. Met /\ D e. Met) /\ J = K) -> U.J = U.K)
3		metequiv.1	. . . . . . 7 |- X = dom dom C
4		metequiv.3	. . . . . . 7 |- J = (Open` C)
5	3, 4	uniopn2 9138	. . . . . 6 |- (C e. Met -> U.J = X)
6	5	ad2antrr 440	. . . . 5 |- (((C e. Met /\ D e. Met) /\ J = K) -> U.J = X)
7		metequiv.2	. . . . . . 7 |- Y = dom dom D
8		metequiv.4	. . . . . . 7 |- K = (Open` D)
9	7, 8	uniopn2 9138	. . . . . 6 |- (D e. Met -> U.K = Y)
10	9	ad2antlr 441	. . . . 5 |- (((C e. Met /\ D e. Met) /\ J = K) -> U.K = Y)
11	2, 6, 10	3eqtr3d 1934	. . . 4 |- (((C e. Met /\ D e. Met) /\ J = K) -> X = Y)
12	11	ex 402	. . 3 |- ((C e. Met /\ D e. Met) -> (J = K -> X = Y))
13	3, 4	blopn 9153	. . . . . . . . . . . 12 |- (((C e. Met /\ x e. X) /\ (r e. RR /\ 0 < r)) -> (x( ball ` C)r) e. J)
14	13	adantllr 433	. . . . . . . . . . 11 |- ((((C e. Met /\ D e. Met) /\ x e. X) /\ (r e. RR /\ 0 < r)) -> (x( ball ` C)r) e. J)
15	14	adantllr 433	. . . . . . . . . 10 |- (((((C e. Met /\ D e. Met) /\ J = K) /\ x e. X) /\ (r e. RR /\ 0 < r)) -> (x( ball ` C)r) e. J)
16		simpllr 453	. . . . . . . . . 10 |- (((((C e. Met /\ D e. Met) /\ J = K) /\ x e. X) /\ (r e. RR /\ 0 < r)) -> J = K)
17	15, 16	eleqtrd 1973	. . . . . . . . 9 |- (((((C e. Met /\ D e. Met) /\ J = K) /\ x e. X) /\ (r e. RR /\ 0 < r)) -> (x( ball ` C)r) e. K)
18	3	blcntr 9122	. . . . . . . . . . . 12 |- (((C e. Met /\ x e. X) /\ (r e. RR /\ 0 < r)) -> x e. (x( ball ` C)r))
19	18	adantllr 433	. . . . . . . . . . 11 |- ((((C e. Met /\ D e. Met) /\ x e. X) /\ (r e. RR /\ 0 < r)) -> x e. (x( ball ` C)r))
20	8	opni2 9142	. . . . . . . . . . . . . . 15 |- ((D e. Met /\ (x( ball ` C)r) e. K /\ x e. (x( ball ` C)r)) -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)))
21	20	3com23 1074	. . . . . . . . . . . . . 14 |- ((D e. Met /\ x e. (x( ball ` C)r) /\ (x( ball ` C)r) e. K) -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)))
22	21	3exp 1066	. . . . . . . . . . . . 13 |- (D e. Met -> (x e. (x( ball ` C)r) -> ((x( ball ` C)r) e. K -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)))))
23	22	ad2antlr 441	. . . . . . . . . . . 12 |- (((C e. Met /\ D e. Met) /\ (r e. RR /\ 0 < r)) -> (x e. (x( ball ` C)r) -> ((x( ball ` C)r) e. K -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)))))
24	23	adantlr 429	. . . . . . . . . . 11 |- ((((C e. Met /\ D e. Met) /\ x e. X) /\ (r e. RR /\ 0 < r)) -> (x e. (x( ball ` C)r) -> ((x( ball ` C)r) e. K -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)))))
25	19, 24	mpd 29	. . . . . . . . . 10 |- ((((C e. Met /\ D e. Met) /\ x e. X) /\ (r e. RR /\ 0 < r)) -> ((x( ball ` C)r) e. K -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))))
26	25	adantllr 433	. . . . . . . . 9 |- (((((C e. Met /\ D e. Met) /\ J = K) /\ x e. X) /\ (r e. RR /\ 0 < r)) -> ((x( ball ` C)r) e. K -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))))
27	17, 26	mpd 29	. . . . . . . 8 |- (((((C e. Met /\ D e. Met) /\ J = K) /\ x e. X) /\ (r e. RR /\ 0 < r)) -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)))
28	27	expr 418	. . . . . . 7 |- (((((C e. Met /\ D e. Met) /\ J = K) /\ x e. X) /\ r e. RR) -> (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))))
29	28	r19.21aiva 2176	. . . . . 6 |- ((((C e. Met /\ D e. Met) /\ J = K) /\ x e. X) -> A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))))
30	11	eleq2d 1964	. . . . . . . 8 |- (((C e. Met /\ D e. Met) /\ J = K) -> (x e. X <-> x e. Y))
31	30	biimpa 460	. . . . . . 7 |- ((((C e. Met /\ D e. Met) /\ J = K) /\ x e. X) -> x e. Y)
32	7, 8	blopn 9153	. . . . . . . . . . . . 13 |- (((D e. Met /\ x e. Y) /\ (s e. RR /\ 0 < s)) -> (x( ball ` D)s) e. K)
33	32	adantlll 432	. . . . . . . . . . . 12 |- ((((C e. Met /\ D e. Met) /\ x e. Y) /\ (s e. RR /\ 0 < s)) -> (x( ball ` D)s) e. K)
34	33	adantllr 433	. . . . . . . . . . 11 |- (((((C e. Met /\ D e. Met) /\ J = K) /\ x e. Y) /\ (s e. RR /\ 0 < s)) -> (x( ball ` D)s) e. K)
35		simpllr 453	. . . . . . . . . . 11 |- (((((C e. Met /\ D e. Met) /\ J = K) /\ x e. Y) /\ (s e. RR /\ 0 < s)) -> J = K)
36	34, 35	eleqtrrd 1974	. . . . . . . . . 10 |- (((((C e. Met /\ D e. Met) /\ J = K) /\ x e. Y) /\ (s e. RR /\ 0 < s)) -> (x( ball ` D)s) e. J)
37	7	blcntr 9122	. . . . . . . . . . . . 13 |- (((D e. Met /\ x e. Y) /\ (s e. RR /\ 0 < s)) -> x e. (x( ball ` D)s))
38	37	adantlll 432	. . . . . . . . . . . 12 |- ((((C e. Met /\ D e. Met) /\ x e. Y) /\ (s e. RR /\ 0 < s)) -> x e. (x( ball ` D)s))
39	4	opni2 9142	. . . . . . . . . . . . . . . 16 |- ((C e. Met /\ (x( ball ` D)s) e. J /\ x e. (x( ball ` D)s)) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))
40	39	3com23 1074	. . . . . . . . . . . . . . 15 |- ((C e. Met /\ x e. (x( ball ` D)s) /\ (x( ball ` D)s) e. J) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))
41	40	3exp 1066	. . . . . . . . . . . . . 14 |- (C e. Met -> (x e. (x( ball ` D)s) -> ((x( ball ` D)s) e. J -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))
42	41	ad2antrr 440	. . . . . . . . . . . . 13 |- (((C e. Met /\ D e. Met) /\ (s e. RR /\ 0 < s)) -> (x e. (x( ball ` D)s) -> ((x( ball ` D)s) e. J -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))
43	42	adantlr 429	. . . . . . . . . . . 12 |- ((((C e. Met /\ D e. Met) /\ x e. Y) /\ (s e. RR /\ 0 < s)) -> (x e. (x( ball ` D)s) -> ((x( ball ` D)s) e. J -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))
44	38, 43	mpd 29	. . . . . . . . . . 11 |- ((((C e. Met /\ D e. Met) /\ x e. Y) /\ (s e. RR /\ 0 < s)) -> ((x( ball ` D)s) e. J -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))
45	44	adantllr 433	. . . . . . . . . 10 |- (((((C e. Met /\ D e. Met) /\ J = K) /\ x e. Y) /\ (s e. RR /\ 0 < s)) -> ((x( ball ` D)s) e. J -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))
46	36, 45	mpd 29	. . . . . . . . 9 |- (((((C e. Met /\ D e. Met) /\ J = K) /\ x e. Y) /\ (s e. RR /\ 0 < s)) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))
47	46	expr 418	. . . . . . . 8 |- (((((C e. Met /\ D e. Met) /\ J = K) /\ x e. Y) /\ s e. RR) -> (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))
48	47	r19.21aiva 2176	. . . . . . 7 |- ((((C e. Met /\ D e. Met) /\ J = K) /\ x e. Y) -> A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))
49	31, 48	syldan 516	. . . . . 6 |- ((((C e. Met /\ D e. Met) /\ J = K) /\ x e. X) -> A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))
50	29, 49	jca 310	. . . . 5 |- ((((C e. Met /\ D e. Met) /\ J = K) /\ x e. X) -> (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))
51	50	r19.21aiva 2176	. . . 4 |- (((C e. Met /\ D e. Met) /\ J = K) -> A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))
52	51	ex 402	. . 3 |- ((C e. Met /\ D e. Met) -> (J = K -> A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))))
53	12, 52	jcad 661	. 2 |- ((C e. Met /\ D e. Met) -> (J = K -> (X = Y /\ A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))))
54		simprl 450	. . . . . . . . . 10 |- (((C e. Met /\ D e. Met) /\ (X = Y /\ A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))) -> X = Y)
55	54	sseq2d 2645	. . . . . . . . 9 |- (((C e. Met /\ D e. Met) /\ (X = Y /\ A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))) -> (o C_ X <-> o C_ Y))
56	55	biimpd 170	. . . . . . . 8 |- (((C e. Met /\ D e. Met) /\ (X = Y /\ A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))) -> (o C_ X -> o C_ Y))
57	56	adantrd 427	. . . . . . 7 |- (((C e. Met /\ D e. Met) /\ (X = Y /\ A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))) -> ((o C_ X /\ A.x e. o E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)) -> o C_ Y))
58		ax-17 1317	. . . . . . . . . . 11 |- ((C e. Met /\ D e. Met) -> A.x(C e. Met /\ D e. Met))
59		ax-17 1317	. . . . . . . . . . . 12 |- (X = Y -> A.x X = Y)
60		hbra1 2147	. . . . . . . . . . . 12 |- (A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))) -> A.xA.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))
61	59, 60	hban 1356	. . . . . . . . . . 11 |- ((X = Y /\ A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))) -> A.x(X = Y /\ A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))))
62	58, 61	hban 1356	. . . . . . . . . 10 |- (((C e. Met /\ D e. Met) /\ (X = Y /\ A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))) -> A.x((C e. Met /\ D e. Met) /\ (X = Y /\ A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))))
63		ax-17 1317	. . . . . . . . . . 11 |- (o C_ X -> A.x o C_ X)
64		hbra1 2147	. . . . . . . . . . 11 |- (A.x e. o E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o) -> A.xA.x e. o E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o))
65	63, 64	hban 1356	. . . . . . . . . 10 |- ((o C_ X /\ A.x e. o E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)) -> A.x(o C_ X /\ A.x e. o E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)))
66	62, 65	hban 1356	. . . . . . . . 9 |- ((((C e. Met /\ D e. Met) /\ (X = Y /\ A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))) /\ (o C_ X /\ A.x e. o E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o))) -> A.x(((C e. Met /\ D e. Met) /\ (X = Y /\ A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))) /\ (o C_ X /\ A.x e. o E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o))))
67		pm2.27 76	. . . . . . . . . . . . . 14 |- (x e. o -> ((x e. o -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)))
68		ssel2 2616	. . . . . . . . . . . . . . . . . . . . 21 |- ((o C_ X /\ x e. o) -> x e. X)
69		pm2.27 76	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x e. X -> ((x e. X -> (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))) -> (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))))
70		ax-17 1317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (x e. X -> A.r x e. X)
71		hbra1 2147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) -> A.rA.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))))
72	70, 71	hban 1356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((x e. X /\ A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)))) -> A.r(x e. X /\ A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)))))
73		ax-17 1317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((C e. Met /\ D e. Met) -> A.r(C e. Met /\ D e. Met))
74	72, 73	hban 1356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((x e. X /\ A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)))) /\ (C e. Met /\ D e. Met)) -> A.r((x e. X /\ A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)))) /\ (C e. Met /\ D e. Met)))
75		ax-17 1317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (X = Y -> A.r X = Y)
76	74, 75	hban 1356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((((x e. X /\ A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)))) /\ (C e. Met /\ D e. Met)) /\ X = Y) -> A.r(((x e. X /\ A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)))) /\ (C e. Met /\ D e. Met)) /\ X = Y))
77		ax-17 1317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((o C_ X /\ x e. o) -> A.r(o C_ X /\ x e. o))
78	76, 77	hban 1356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((((x e. X /\ A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)))) /\ (C e. Met /\ D e. Met)) /\ X = Y) /\ (o C_ X /\ x e. o)) -> A.r((((x e. X /\ A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)))) /\ (C e. Met /\ D e. Met)) /\ X = Y) /\ (o C_ X /\ x e. o)))
79		ax-17 1317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o) -> A.rE.s e. RR (0 < s /\ (x( ball ` D)s) C_ o))
80		pm2.27 76	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (r e. RR -> ((r e. RR -> (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)))) -> (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)))))
81		pm2.27 76	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (0 < r -> ((0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))))
82		sstr 2625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 |- (((x( ball ` D)s) C_ (x( ball ` C)r) /\ (x( ball ` C)r) C_ o) -> (x( ball ` D)s) C_ o)
83	82	expcom 403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 |- ((x( ball ` C)r) C_ o -> ((x( ball ` D)s) C_ (x( ball ` C)r) -> (x( ball ` D)s) C_ o))
84	83	anim2d 620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 |- ((x( ball ` C)r) C_ o -> ((0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)) -> (0 < s /\ (x( ball ` D)s) C_ o)))
85	84	a1d 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- ((x( ball ` C)r) C_ o -> (s e. RR -> ((0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)) -> (0 < s /\ (x( ball ` D)s) C_ o))))
86	85	reximdvai 2201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- ((x( ball ` C)r) C_ o -> (E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)) -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)))
87	86	a1dd 53	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ((x( ball ` C)r) C_ o -> (E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)) -> (X = Y -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o))))
88	87	a1d 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ((x( ball ` C)r) C_ o -> (x e. X -> (E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)) -> (X = Y -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)))))
89	88	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- (r e. RR -> ((x( ball ` C)r) C_ o -> (x e. X -> (E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)) -> (X = Y -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o))))))
90	89	a1i12 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ((C e. Met /\ D e. Met) -> ((o C_ X /\ x e. o) -> (r e. RR -> ((x( ball ` C)r) C_ o -> (x e. X -> (E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)) -> (X = Y -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o))))))))
91	90	com24 41	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ((C e. Met /\ D e. Met) -> ((x( ball ` C)r) C_ o -> (r e. RR -> ((o C_ X /\ x e. o) -> (x e. X -> (E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)) -> (X = Y -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o))))))))
92	91	3imp 1061	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (((C e. Met /\ D e. Met) /\ (x( ball ` C)r) C_ o /\ r e. RR) -> ((o C_ X /\ x e. o) -> (x e. X -> (E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)) -> (X = Y -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o))))))
93	92	com24 41	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (((C e. Met /\ D e. Met) /\ (x( ball ` C)r) C_ o /\ r e. RR) -> (E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)) -> (x e. X -> ((o C_ X /\ x e. o) -> (X = Y -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o))))))
94	93	3exp 1066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ((C e. Met /\ D e. Met) -> ((x( ball ` C)r) C_ o -> (r e. RR -> (E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)) -> (x e. X -> ((o C_ X /\ x e. o) -> (X = Y -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o))))))))
95	94	com14 42	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- (E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)) -> ((x( ball ` C)r) C_ o -> (r e. RR -> ((C e. Met /\ D e. Met) -> (x e. X -> ((o C_ X /\ x e. o) -> (X = Y -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o))))))))
96	81, 95	syl6 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (0 < r -> ((0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) -> ((x( ball ` C)r) C_ o -> (r e. RR -> ((C e. Met /\ D e. Met) -> (x e. X -> ((o C_ X /\ x e. o) -> (X = Y -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)))))))))
97	96	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (0 < r -> ((x( ball ` C)r) C_ o -> ((0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) -> (r e. RR -> ((C e. Met /\ D e. Met) -> (x e. X -> ((o C_ X /\ x e. o) -> (X = Y -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)))))))))
98	97	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- ((0 < r /\ (x( ball ` C)r) C_ o) -> ((0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) -> (r e. RR -> ((C e. Met /\ D e. Met) -> (x e. X -> ((o C_ X /\ x e. o) -> (X = Y -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o))))))))
99	98	com13 37	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (r e. RR -> ((0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) -> ((0 < r /\ (x( ball ` C)r) C_ o) -> ((C e. Met /\ D e. Met) -> (x e. X -> ((o C_ X /\ x e. o) -> (X = Y -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o))))))))
100	80, 99	syld 30	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (r e. RR -> ((r e. RR -> (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)))) -> ((0 < r /\ (x( ball ` C)r) C_ o) -> ((C e. Met /\ D e. Met) -> (x e. X -> ((o C_ X /\ x e. o) -> (X = Y -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o))))))))
101	100	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (r e. RR -> ((0 < r /\ (x( ball ` C)r) C_ o) -> ((r e. RR -> (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)))) -> ((C e. Met /\ D e. Met) -> (x e. X -> ((o C_ X /\ x e. o) -> (X = Y -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o))))))))
102	101	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((r e. RR /\ (0 < r /\ (x( ball ` C)r) C_ o)) -> ((r e. RR -> (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)))) -> ((C e. Met /\ D e. Met) -> (x e. X -> ((o C_ X /\ x e. o) -> (X = Y -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)))))))
103	102	com14 42	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (x e. X -> ((r e. RR -> (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)))) -> ((C e. Met /\ D e. Met) -> ((r e. RR /\ (0 < r /\ (x( ball ` C)r) C_ o)) -> ((o C_ X /\ x e. o) -> (X = Y -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)))))))
104	103	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((x e. X /\ (r e. RR -> (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))))) -> ((C e. Met /\ D e. Met) -> ((r e. RR /\ (0 < r /\ (x( ball ` C)r) C_ o)) -> ((o C_ X /\ x e. o) -> (X = Y -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o))))))
105		ra4 2155	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) -> (r e. RR -> (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)))))
106	104, 105	sylan2 500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((x e. X /\ A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)))) -> ((C e. Met /\ D e. Met) -> ((r e. RR /\ (0 < r /\ (x( ball ` C)r) C_ o)) -> ((o C_ X /\ x e. o) -> (X = Y -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o))))))
107	106	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((x e. X /\ A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)))) /\ (C e. Met /\ D e. Met)) -> ((r e. RR /\ (0 < r /\ (x( ball ` C)r) C_ o)) -> ((o C_ X /\ x e. o) -> (X = Y -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)))))
108	107	com24 41	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((x e. X /\ A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)))) /\ (C e. Met /\ D e. Met)) -> (X = Y -> ((o C_ X /\ x e. o) -> ((r e. RR /\ (0 < r /\ (x( ball ` C)r) C_ o)) -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)))))
109	108	imp31 389	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((((x e. X /\ A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)))) /\ (C e. Met /\ D e. Met)) /\ X = Y) /\ (o C_ X /\ x e. o)) -> ((r e. RR /\ (0 < r /\ (x( ball ` C)r) C_ o)) -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)))
110	109	exp3a 405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((((x e. X /\ A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)))) /\ (C e. Met /\ D e. Met)) /\ X = Y) /\ (o C_ X /\ x e. o)) -> (r e. RR -> ((0 < r /\ (x( ball ` C)r) C_ o) -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o))))
111	78, 79, 110	r19.23ad 2213	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((((x e. X /\ A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)))) /\ (C e. Met /\ D e. Met)) /\ X = Y) /\ (o C_ X /\ x e. o)) -> (E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o) -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)))
112	111	exp31 407	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((x e. X /\ A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r)))) /\ (C e. Met /\ D e. Met)) -> (X = Y -> ((o C_ X /\ x e. o) -> (E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o) -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)))))
113	112	adantlrr 435	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((x e. X /\ (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))) /\ (C e. Met /\ D e. Met)) -> (X = Y -> ((o C_ X /\ x e. o) -> (E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o) -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)))))
114	113	exp31 407	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x e. X -> ((A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))) -> ((C e. Met /\ D e. Met) -> (X = Y -> ((o C_ X /\ x e. o) -> (E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o) -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)))))))
115	69, 114	syld 30	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (x e. X -> ((x e. X -> (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))) -> ((C e. Met /\ D e. Met) -> (X = Y -> ((o C_ X /\ x e. o) -> (E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o) -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)))))))
116	115	com14 42	. . . . . . . . . . . . . . . . . . . . . . 23 |- (X = Y -> ((x e. X -> (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))) -> ((C e. Met /\ D e. Met) -> (x e. X -> ((o C_ X /\ x e. o) -> (E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o) -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)))))))
117	116	imp31 389	. . . . . . . . . . . . . . . . . . . . . 22 |- (((X = Y /\ (x e. X -> (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))) /\ (C e. Met /\ D e. Met)) -> (x e. X -> ((o C_ X /\ x e. o) -> (E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o) -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)))))
118	117	com13 37	. . . . . . . . . . . . . . . . . . . . 21 |- ((o C_ X /\ x e. o) -> (x e. X -> (((X = Y /\ (x e. X -> (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))) /\ (C e. Met /\ D e. Met)) -> (E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o) -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)))))
119	68, 118	mpd 29	. . . . . . . . . . . . . . . . . . . 20 |- ((o C_ X /\ x e. o) -> (((X = Y /\ (x e. X -> (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))) /\ (C e. Met /\ D e. Met)) -> (E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o) -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o))))
120	119	ex 402	. . . . . . . . . . . . . . . . . . 19 |- (o C_ X -> (x e. o -> (((X = Y /\ (x e. X -> (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))) /\ (C e. Met /\ D e. Met)) -> (E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o) -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)))))
121	120	com4t 44	. . . . . . . . . . . . . . . . . 18 |- (((X = Y /\ (x e. X -> (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))) /\ (C e. Met /\ D e. Met)) -> (E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o) -> (o C_ X -> (x e. o -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)))))
122	121	ex 402	. . . . . . . . . . . . . . . . 17 |- ((X = Y /\ (x e. X -> (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))) -> ((C e. Met /\ D e. Met) -> (E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o) -> (o C_ X -> (x e. o -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o))))))
123		ra4 2155	. . . . . . . . . . . . . . . . 17 |- (A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))) -> (x e. X -> (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))))
124	122, 123	sylan2 500	. . . . . . . . . . . . . . . 16 |- ((X = Y /\ A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))) -> ((C e. Met /\ D e. Met) -> (E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o) -> (o C_ X -> (x e. o -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o))))))
125	124	impcom 378	. . . . . . . . . . . . . . 15 |- (((C e. Met /\ D e. Met) /\ (X = Y /\ A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))) -> (E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o) -> (o C_ X -> (x e. o -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)))))
126	125	com14 42	. . . . . . . . . . . . . 14 |- (x e. o -> (E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o) -> (o C_ X -> (((C e. Met /\ D e. Met) /\ (X = Y /\ A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))) -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)))))
127	67, 126	syld 30	. . . . . . . . . . . . 13 |- (x e. o -> ((x e. o -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)) -> (o C_ X -> (((C e. Met /\ D e. Met) /\ (X = Y /\ A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))) -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)))))
128	127	com4l 43	. . . . . . . . . . . 12 |- ((x e. o -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)) -> (o C_ X -> (((C e. Met /\ D e. Met) /\ (X = Y /\ A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))) -> (x e. o -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)))))
129	128	impcom 378	. . . . . . . . . . 11 |- ((o C_ X /\ (x e. o -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o))) -> (((C e. Met /\ D e. Met) /\ (X = Y /\ A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))) -> (x e. o -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o))))
130		ra4 2155	. . . . . . . . . . 11 |- (A.x e. o E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o) -> (x e. o -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)))
131	129, 130	sylan2 500	. . . . . . . . . 10 |- ((o C_ X /\ A.x e. o E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)) -> (((C e. Met /\ D e. Met) /\ (X = Y /\ A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))) -> (x e. o -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o))))
132	131	impcom 378	. . . . . . . . 9 |- ((((C e. Met /\ D e. Met) /\ (X = Y /\ A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))) /\ (o C_ X /\ A.x e. o E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o))) -> (x e. o -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)))
133	66, 132	r19.21ai 2174	. . . . . . . 8 |- ((((C e. Met /\ D e. Met) /\ (X = Y /\ A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))) /\ (o C_ X /\ A.x e. o E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o))) -> A.x e. o E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o))
134	133	ex 402	. . . . . . 7 |- (((C e. Met /\ D e. Met) /\ (X = Y /\ A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))) -> ((o C_ X /\ A.x e. o E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)) -> A.x e. o E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)))
135	57, 134	jcad 661	. . . . . 6 |- (((C e. Met /\ D e. Met) /\ (X = Y /\ A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))) -> ((o C_ X /\ A.x e. o E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)) -> (o C_ Y /\ A.x e. o E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o))))
136		raleq 2266	. . . . . . . . 9 |- (X = Y -> (A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))) <-> A.x e. Y (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))))
137	136	biimpa 460	. . . . . . . 8 |- ((X = Y /\ A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))) -> A.x e. Y (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))
138		simprl 450	. . . . . . . . . . . . 13 |- (((C e. Met /\ D e. Met) /\ (X = Y /\ A.x e. Y (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))) -> X = Y)
139	138	sseq2d 2645	. . . . . . . . . . . 12 |- (((C e. Met /\ D e. Met) /\ (X = Y /\ A.x e. Y (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))) -> (o C_ X <-> o C_ Y))
140	139	biimprd 171	. . . . . . . . . . 11 |- (((C e. Met /\ D e. Met) /\ (X = Y /\ A.x e. Y (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))) -> (o C_ Y -> o C_ X))
141	140	adantrd 427	. . . . . . . . . 10 |- (((C e. Met /\ D e. Met) /\ (X = Y /\ A.x e. Y (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))) -> ((o C_ Y /\ A.x e. o E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)) -> o C_ X))
142		hbra1 2147	. . . . . . . . . . . . . . 15 |- (A.x e. Y (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))) -> A.xA.x e. Y (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))
143	58, 142	hban 1356	. . . . . . . . . . . . . 14 |- (((C e. Met /\ D e. Met) /\ A.x e. Y (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))) -> A.x((C e. Met /\ D e. Met) /\ A.x e. Y (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))))
144		ax-17 1317	. . . . . . . . . . . . . . 15 |- (o C_ Y -> A.x o C_ Y)
145		hbra1 2147	. . . . . . . . . . . . . . 15 |- (A.x e. o E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o) -> A.xA.x e. o E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o))
146	144, 145	hban 1356	. . . . . . . . . . . . . 14 |- ((o C_ Y /\ A.x e. o E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)) -> A.x(o C_ Y /\ A.x e. o E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)))
147	143, 146	hban 1356	. . . . . . . . . . . . 13 |- ((((C e. Met /\ D e. Met) /\ A.x e. Y (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))) /\ (o C_ Y /\ A.x e. o E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o))) -> A.x(((C e. Met /\ D e. Met) /\ A.x e. Y (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))) /\ (o C_ Y /\ A.x e. o E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o))))
148		pm2.27 76	. . . . . . . . . . . . . . . . . 18 |- (x e. o -> ((x e. o -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)) -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)))
149		ssel2 2616	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((o C_ Y /\ x e. o) -> x e. Y)
150		pm2.27 76	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x e. Y -> ((x e. Y -> (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))) -> (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))))
151		ax-17 1317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (x e. Y -> A.s x e. Y)
152		hbra1 2147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))) -> A.sA.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))
153	151, 152	hban 1356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((x e. Y /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))) -> A.s(x e. Y /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))
154		ax-17 1317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((C e. Met /\ D e. Met) -> A.s(C e. Met /\ D e. Met))
155	153, 154	hban 1356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((x e. Y /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))) /\ (C e. Met /\ D e. Met)) -> A.s((x e. Y /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))) /\ (C e. Met /\ D e. Met)))
156		ax-17 1317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((o C_ Y /\ x e. o) -> A.s(o C_ Y /\ x e. o))
157	155, 156	hban 1356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((((x e. Y /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))) /\ (C e. Met /\ D e. Met)) /\ (o C_ Y /\ x e. o)) -> A.s(((x e. Y /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))) /\ (C e. Met /\ D e. Met)) /\ (o C_ Y /\ x e. o)))
158		ax-17 1317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o) -> A.sE.r e. RR (0 < r /\ (x( ball ` C)r) C_ o))
159		pm2.27 76	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (s e. RR -> ((s e. RR -> (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))) -> (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))
160		pm2.27 76	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (0 < s -> ((0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))
161		sstr 2625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 |- (((x( ball ` C)r) C_ (x( ball ` D)s) /\ (x( ball ` D)s) C_ o) -> (x( ball ` C)r) C_ o)
162	161	expcom 403	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 |- ((x( ball ` D)s) C_ o -> ((x( ball ` C)r) C_ (x( ball ` D)s) -> (x( ball ` C)r) C_ o))
163	162	anim2d 620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 |- ((x( ball ` D)s) C_ o -> ((0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)) -> (0 < r /\ (x( ball ` C)r) C_ o)))
164	163	a1d 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 |- ((x( ball ` D)s) C_ o -> (r e. RR -> ((0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)) -> (0 < r /\ (x( ball ` C)r) C_ o))))
165	164	reximdvai 2201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 |- ((x( ball ` D)s) C_ o -> (E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)))
166	165	com12 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- (E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)) -> ((x( ball ` D)s) C_ o -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)))
167	166	a1d 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- (E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)) -> (x e. Y -> ((x( ball ` D)s) C_ o -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o))))
168	167	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ((o C_ Y /\ x e. o) -> (E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)) -> (x e. Y -> ((x( ball ` D)s) C_ o -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)))))
169	168	com14 42	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ((x( ball ` D)s) C_ o -> (E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)) -> (x e. Y -> ((o C_ Y /\ x e. o) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)))))
170	169	a1d 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- ((x( ball ` D)s) C_ o -> (s e. RR -> (E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)) -> (x e. Y -> ((o C_ Y /\ x e. o) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o))))))
171	170	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- ((C e. Met /\ D e. Met) -> ((x( ball ` D)s) C_ o -> (s e. RR -> (E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)) -> (x e. Y -> ((o C_ Y /\ x e. o) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)))))))
172	171	com14 42	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)) -> ((x( ball ` D)s) C_ o -> (s e. RR -> ((C e. Met /\ D e. Met) -> (x e. Y -> ((o C_ Y /\ x e. o) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)))))))
173	160, 172	syl6 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- (0 < s -> ((0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))) -> ((x( ball ` D)s) C_ o -> (s e. RR -> ((C e. Met /\ D e. Met) -> (x e. Y -> ((o C_ Y /\ x e. o) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o))))))))
174	173	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- (0 < s -> ((x( ball ` D)s) C_ o -> ((0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))) -> (s e. RR -> ((C e. Met /\ D e. Met) -> (x e. Y -> ((o C_ Y /\ x e. o) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o))))))))
175	174	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ((0 < s /\ (x( ball ` D)s) C_ o) -> ((0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))) -> (s e. RR -> ((C e. Met /\ D e. Met) -> (x e. Y -> ((o C_ Y /\ x e. o) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)))))))
176	175	com13 37	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- (s e. RR -> ((0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))) -> ((0 < s /\ (x( ball ` D)s) C_ o) -> ((C e. Met /\ D e. Met) -> (x e. Y -> ((o C_ Y /\ x e. o) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)))))))
177	159, 176	syld 30	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 |- (s e. RR -> ((s e. RR -> (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))) -> ((0 < s /\ (x( ball ` D)s) C_ o) -> ((C e. Met /\ D e. Met) -> (x e. Y -> ((o C_ Y /\ x e. o) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)))))))
178	177	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- (s e. RR -> ((0 < s /\ (x( ball ` D)s) C_ o) -> ((s e. RR -> (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))) -> ((C e. Met /\ D e. Met) -> (x e. Y -> ((o C_ Y /\ x e. o) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)))))))
179	178	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((s e. RR /\ (0 < s /\ (x( ball ` D)s) C_ o)) -> ((s e. RR -> (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))) -> ((C e. Met /\ D e. Met) -> (x e. Y -> ((o C_ Y /\ x e. o) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o))))))
180	179	com14 42	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (x e. Y -> ((s e. RR -> (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))) -> ((C e. Met /\ D e. Met) -> ((s e. RR /\ (0 < s /\ (x( ball ` D)s) C_ o)) -> ((o C_ Y /\ x e. o) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o))))))
181	180	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((x e. Y /\ (s e. RR -> (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))) -> ((C e. Met /\ D e. Met) -> ((s e. RR /\ (0 < s /\ (x( ball ` D)s) C_ o)) -> ((o C_ Y /\ x e. o) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)))))
182		ra4 2155	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))) -> (s e. RR -> (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))
183	181, 182	sylan2 500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((x e. Y /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))) -> ((C e. Met /\ D e. Met) -> ((s e. RR /\ (0 < s /\ (x( ball ` D)s) C_ o)) -> ((o C_ Y /\ x e. o) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)))))
184	183	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((x e. Y /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))) /\ (C e. Met /\ D e. Met)) -> ((s e. RR /\ (0 < s /\ (x( ball ` D)s) C_ o)) -> ((o C_ Y /\ x e. o) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o))))
185	184	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((x e. Y /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))) /\ (C e. Met /\ D e. Met)) -> ((o C_ Y /\ x e. o) -> ((s e. RR /\ (0 < s /\ (x( ball ` D)s) C_ o)) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o))))
186	185	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((((x e. Y /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))) /\ (C e. Met /\ D e. Met)) /\ (o C_ Y /\ x e. o)) -> ((s e. RR /\ (0 < s /\ (x( ball ` D)s) C_ o)) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)))
187	186	exp3a 405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((((x e. Y /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))) /\ (C e. Met /\ D e. Met)) /\ (o C_ Y /\ x e. o)) -> (s e. RR -> ((0 < s /\ (x( ball ` D)s) C_ o) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o))))
188	157, 158, 187	r19.23ad 2213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((((x e. Y /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))) /\ (C e. Met /\ D e. Met)) /\ (o C_ Y /\ x e. o)) -> (E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)))
189	188	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((x e. Y /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))) /\ (C e. Met /\ D e. Met)) -> ((o C_ Y /\ x e. o) -> (E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o))))
190	189	adantlrl 434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((x e. Y /\ (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))) /\ (C e. Met /\ D e. Met)) -> ((o C_ Y /\ x e. o) -> (E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o))))
191	190	exp31 407	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x e. Y -> ((A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))) -> ((C e. Met /\ D e. Met) -> ((o C_ Y /\ x e. o) -> (E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o))))))
192	150, 191	syld 30	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x e. Y -> ((x e. Y -> (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))) -> ((C e. Met /\ D e. Met) -> ((o C_ Y /\ x e. o) -> (E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o))))))
193	192	com3l 38	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((x e. Y -> (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))) -> ((C e. Met /\ D e. Met) -> (x e. Y -> ((o C_ Y /\ x e. o) -> (E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o))))))
194	193	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((x e. Y -> (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))) /\ (C e. Met /\ D e. Met)) -> (x e. Y -> ((o C_ Y /\ x e. o) -> (E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)))))
195	194	com13 37	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((o C_ Y /\ x e. o) -> (x e. Y -> (((x e. Y -> (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))) /\ (C e. Met /\ D e. Met)) -> (E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)))))
196	149, 195	mpd 29	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((o C_ Y /\ x e. o) -> (((x e. Y -> (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))) /\ (C e. Met /\ D e. Met)) -> (E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o))))
197	196	ex 402	. . . . . . . . . . . . . . . . . . . . . 22 |- (o C_ Y -> (x e. o -> (((x e. Y -> (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))) /\ (C e. Met /\ D e. Met)) -> (E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)))))
198	197	com4t 44	. . . . . . . . . . . . . . . . . . . . 21 |- (((x e. Y -> (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))) /\ (C e. Met /\ D e. Met)) -> (E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o) -> (o C_ Y -> (x e. o -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)))))
199	198	ancoms 484	. . . . . . . . . . . . . . . . . . . 20 |- (((C e. Met /\ D e. Met) /\ (x e. Y -> (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))) -> (E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o) -> (o C_ Y -> (x e. o -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)))))
200		ra4 2155	. . . . . . . . . . . . . . . . . . . 20 |- (A.x e. Y (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))) -> (x e. Y -> (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))))
201	199, 200	sylan2 500	. . . . . . . . . . . . . . . . . . 19 |- (((C e. Met /\ D e. Met) /\ A.x e. Y (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))) -> (E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o) -> (o C_ Y -> (x e. o -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)))))
202	201	com14 42	. . . . . . . . . . . . . . . . . 18 |- (x e. o -> (E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o) -> (o C_ Y -> (((C e. Met /\ D e. Met) /\ A.x e. Y (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)))))
203	148, 202	syld 30	. . . . . . . . . . . . . . . . 17 |- (x e. o -> ((x e. o -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)) -> (o C_ Y -> (((C e. Met /\ D e. Met) /\ A.x e. Y (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))) -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)))))
204	203	com4l 43	. . . . . . . . . . . . . . . 16 |- ((x e. o -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)) -> (o C_ Y -> (((C e. Met /\ D e. Met) /\ A.x e. Y (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))) -> (x e. o -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)))))
205	204	impcom 378	. . . . . . . . . . . . . . 15 |- ((o C_ Y /\ (x e. o -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o))) -> (((C e. Met /\ D e. Met) /\ A.x e. Y (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))) -> (x e. o -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o))))
206		ra4 2155	. . . . . . . . . . . . . . 15 |- (A.x e. o E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o) -> (x e. o -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)))
207	205, 206	sylan2 500	. . . . . . . . . . . . . 14 |- ((o C_ Y /\ A.x e. o E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)) -> (((C e. Met /\ D e. Met) /\ A.x e. Y (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))) -> (x e. o -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o))))
208	207	impcom 378	. . . . . . . . . . . . 13 |- ((((C e. Met /\ D e. Met) /\ A.x e. Y (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))) /\ (o C_ Y /\ A.x e. o E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o))) -> (x e. o -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)))
209	147, 208	r19.21ai 2174	. . . . . . . . . . . 12 |- ((((C e. Met /\ D e. Met) /\ A.x e. Y (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))) /\ (o C_ Y /\ A.x e. o E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o))) -> A.x e. o E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o))
210	209	ex 402	. . . . . . . . . . 11 |- (((C e. Met /\ D e. Met) /\ A.x e. Y (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))) -> ((o C_ Y /\ A.x e. o E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)) -> A.x e. o E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)))
211	210	adantrl 430	. . . . . . . . . 10 |- (((C e. Met /\ D e. Met) /\ (X = Y /\ A.x e. Y (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))) -> ((o C_ Y /\ A.x e. o E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)) -> A.x e. o E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)))
212	141, 211	jcad 661	. . . . . . . . 9 |- (((C e. Met /\ D e. Met) /\ (X = Y /\ A.x e. Y (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))) -> ((o C_ Y /\ A.x e. o E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)) -> (o C_ X /\ A.x e. o E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o))))
213	212	expcom 403	. . . . . . . 8 |- ((X = Y /\ A.x e. Y (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))) -> ((C e. Met /\ D e. Met) -> ((o C_ Y /\ A.x e. o E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)) -> (o C_ X /\ A.x e. o E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)))))
214	137, 213	syldan 516	. . . . . . 7 |- ((X = Y /\ A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))) -> ((C e. Met /\ D e. Met) -> ((o C_ Y /\ A.x e. o E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)) -> (o C_ X /\ A.x e. o E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)))))
215	214	impcom 378	. . . . . 6 |- (((C e. Met /\ D e. Met) /\ (X = Y /\ A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))) -> ((o C_ Y /\ A.x e. o E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o)) -> (o C_ X /\ A.x e. o E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o))))
216	135, 215	impbid 574	. . . . 5 |- (((C e. Met /\ D e. Met) /\ (X = Y /\ A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))) -> ((o C_ X /\ A.x e. o E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o)) <-> (o C_ Y /\ A.x e. o E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o))))
217	3, 4	isopn4 9139	. . . . . 6 |- (C e. Met -> (o e. J <-> (o C_ X /\ A.x e. o E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o))))
218	217	ad2antrr 440	. . . . 5 |- (((C e. Met /\ D e. Met) /\ (X = Y /\ A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))) -> (o e. J <-> (o C_ X /\ A.x e. o E.r e. RR (0 < r /\ (x( ball ` C)r) C_ o))))
219	7, 8	isopn4 9139	. . . . . 6 |- (D e. Met -> (o e. K <-> (o C_ Y /\ A.x e. o E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o))))
220	219	ad2antlr 441	. . . . 5 |- (((C e. Met /\ D e. Met) /\ (X = Y /\ A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))) -> (o e. K <-> (o C_ Y /\ A.x e. o E.s e. RR (0 < s /\ (x( ball ` D)s) C_ o))))
221	216, 218, 220	3bitr4d 609	. . . 4 |- (((C e. Met /\ D e. Met) /\ (X = Y /\ A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))) -> (o e. J <-> o e. K))
222	221	eqrdv 1882	. . 3 |- (((C e. Met /\ D e. Met) /\ (X = Y /\ A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))) -> J = K)
223	222	ex 402	. 2 |- ((C e. Met /\ D e. Met) -> ((X = Y /\ A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s))))) -> J = K))
224	53, 223	impbid 574	1 |- ((C e. Met /\ D e. Met) -> (J = K <-> (X = Y /\ A.x e. X (A.r e. RR (0 < r -> E.s e. RR (0 < s /\ (x( ball ` D)s) C_ (x( ball ` C)r))) /\ A.s e. RR (0 < s -> E.r e. RR (0 < r /\ (x( ball ` C)r) C_ (x( ball ` D)s)))))))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  E.wrex 2106   C_ wss 2593  U.cuni 3177   class class class wbr 3338  dom cdm 3986  ` cfv 3998  (class class class)co 4884  RRcr 6385  0cc0 6386   < clt 6653  Metcme 9066   ball cbl 9068  Opencopn 9069

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-inf2 5731

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-nel 2020  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-mpt 5006  df-1st 5020  df-2nd 5021  df-iota 5089  df-rdg 5140  df-1o 5177  df-oadd 5179  df-omul 5180  df-er 5318  df-ec 5320  df-qs 5323  df-en 5427  df-dom 5428  df-sdom 5429  df-undef 5556  df-riota 5560  df-ni 6152  df-pli 6153  df-mi 6154  df-lti 6155  df-plpq 6187  df-mpq 6188  df-enq 6189  df-nq 6190  df-plq 6191  df-mq 6192  df-rq 6193  df-ltq 6194  df-1q 6195  df-np 6238  df-1p 6239  df-plp 6240  df-mp 6241  df-ltp 6242  df-plpr 6316  df-mpr 6317  df-enr 6318  df-nr 6319  df-plr 6320  df-mr 6321  df-ltr 6322  df-0r 6323  df-1r 6324  df-m1r 6325  df-c 6392  df-0 6393  df-1 6394  df-i 6395  df-r 6396  df-plus 6397  df-mul 6398  df-lt 6399  df-sub 6511  df-neg 6513  df-pnf 6654  df-mnf 6655  df-xr 6656  df-ltxr 6657  df-le 6658  df-met 9070  df-bl 9072  df-opn 9073

Copyright terms: Public domain