Theorem reconnlem2 18811

Description: Lemma for reconn 18812. (Contributed by Jeff Hankins, 17-Aug-2009.) (Proof shortened by Mario Carneiro, 9-Sep-2015.)

Hypotheses

Ref	Expression
reconnlem2.1	|- ( ph -> A C_ RR )
reconnlem2.2	|- ( ph -> U e. ( topGen ` ran (,) ) )
reconnlem2.3	|- ( ph -> V e. ( topGen ` ran (,) ) )
reconnlem2.4	|- ( ph -> A. x e. A A. y e. A ( x [,] y ) C_ A )
reconnlem2.5	|- ( ph -> B e. ( U i^i A ) )
reconnlem2.6	|- ( ph -> C e. ( V i^i A ) )
reconnlem2.7	|- ( ph -> ( U i^i V ) C_ ( RR \ A ) )
reconnlem2.8	|- ( ph -> B <_ C )
reconnlem2.9	|- S = sup ( ( U i^i ( B [,] C ) ) , RR , < )

Assertion

Ref	Expression
reconnlem2	|- ( ph -> -. A C_ ( U u. V ) )

Distinct variable groups:   x, y, A   x, B, y   y, C

Allowed substitution hints:   ph( x, y)   C( x)   S( x, y)   U( x, y)   V( x, y)

Proof of Theorem reconnlem2

Dummy variables w z r are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		reconnlem2.9	. . . . . . . . . . 11 |- S = sup ( ( U i^i ( B [,] C ) ) , RR , < )
2		inss2 3522	. . . . . . . . . . . . 13 |- ( U i^i ( B [,] C ) ) C_ ( B [,] C )
3		inss2 3522	. . . . . . . . . . . . . . . 16 |- ( U i^i A ) C_ A
4		reconnlem2.5	. . . . . . . . . . . . . . . 16 |- ( ph -> B e. ( U i^i A ) )
5	3, 4	sseldi 3306	. . . . . . . . . . . . . . 15 |- ( ph -> B e. A )
6		inss2 3522	. . . . . . . . . . . . . . . 16 |- ( V i^i A ) C_ A
7		reconnlem2.6	. . . . . . . . . . . . . . . 16 |- ( ph -> C e. ( V i^i A ) )
8	6, 7	sseldi 3306	. . . . . . . . . . . . . . 15 |- ( ph -> C e. A )
9		reconnlem2.4	. . . . . . . . . . . . . . 15 |- ( ph -> A. x e. A A. y e. A ( x [,] y ) C_ A )
10		oveq1 6047	. . . . . . . . . . . . . . . . 17 |- ( x = B -> ( x [,] y ) = ( B [,] y ) )
11	10	sseq1d 3335	. . . . . . . . . . . . . . . 16 |- ( x = B -> ( ( x [,] y ) C_ A <-> ( B [,] y ) C_ A ) )
12		oveq2 6048	. . . . . . . . . . . . . . . . 17 |- ( y = C -> ( B [,] y ) = ( B [,] C ) )
13	12	sseq1d 3335	. . . . . . . . . . . . . . . 16 |- ( y = C -> ( ( B [,] y ) C_ A <-> ( B [,] C ) C_ A ) )
14	11, 13	rspc2va 3019	. . . . . . . . . . . . . . 15 |- ( ( ( B e. A /\ C e. A ) /\ A. x e. A A. y e. A ( x [,] y ) C_ A ) -> ( B [,] C ) C_ A )
15	5, 8, 9, 14	syl21anc 1183	. . . . . . . . . . . . . 14 |- ( ph -> ( B [,] C ) C_ A )
16		reconnlem2.1	. . . . . . . . . . . . . 14 |- ( ph -> A C_ RR )
17	15, 16	sstrd 3318	. . . . . . . . . . . . 13 |- ( ph -> ( B [,] C ) C_ RR )
18	2, 17	syl5ss 3319	. . . . . . . . . . . 12 |- ( ph -> ( U i^i ( B [,] C ) ) C_ RR )
19		inss1 3521	. . . . . . . . . . . . . . 15 |- ( U i^i A ) C_ U
20	19, 4	sseldi 3306	. . . . . . . . . . . . . 14 |- ( ph -> B e. U )
21	16, 5	sseldd 3309	. . . . . . . . . . . . . . . 16 |- ( ph -> B e. RR )
22	21	rexrd 9090	. . . . . . . . . . . . . . 15 |- ( ph -> B e. RR* )
23	16, 8	sseldd 3309	. . . . . . . . . . . . . . . 16 |- ( ph -> C e. RR )
24	23	rexrd 9090	. . . . . . . . . . . . . . 15 |- ( ph -> C e. RR* )
25		reconnlem2.8	. . . . . . . . . . . . . . 15 |- ( ph -> B <_ C )
26		lbicc2 10969	. . . . . . . . . . . . . . 15 |- ( ( B e. RR* /\ C e. RR* /\ B <_ C ) -> B e. ( B [,] C ) )
27	22, 24, 25, 26	syl3anc 1184	. . . . . . . . . . . . . 14 |- ( ph -> B e. ( B [,] C ) )
28		elin 3490	. . . . . . . . . . . . . 14 |- ( B e. ( U i^i ( B [,] C ) ) <-> ( B e. U /\ B e. ( B [,] C ) ) )
29	20, 27, 28	sylanbrc 646	. . . . . . . . . . . . 13 |- ( ph -> B e. ( U i^i ( B [,] C ) ) )
30		ne0i 3594	. . . . . . . . . . . . 13 |- ( B e. ( U i^i ( B [,] C ) ) -> ( U i^i ( B [,] C ) ) =/= (/) )
31	29, 30	syl 16	. . . . . . . . . . . 12 |- ( ph -> ( U i^i ( B [,] C ) ) =/= (/) )
32	2	sseli 3304	. . . . . . . . . . . . . . 15 |- ( w e. ( U i^i ( B [,] C ) ) -> w e. ( B [,] C ) )
33		elicc2 10931	. . . . . . . . . . . . . . . . 17 |- ( ( B e. RR /\ C e. RR ) -> ( w e. ( B [,] C ) <-> ( w e. RR /\ B <_ w /\ w <_ C ) ) )
34	21, 23, 33	syl2anc 643	. . . . . . . . . . . . . . . 16 |- ( ph -> ( w e. ( B [,] C ) <-> ( w e. RR /\ B <_ w /\ w <_ C ) ) )
35		simp3 959	. . . . . . . . . . . . . . . 16 |- ( ( w e. RR /\ B <_ w /\ w <_ C ) -> w <_ C )
36	34, 35	syl6bi 220	. . . . . . . . . . . . . . 15 |- ( ph -> ( w e. ( B [,] C ) -> w <_ C ) )
37	32, 36	syl5 30	. . . . . . . . . . . . . 14 |- ( ph -> ( w e. ( U i^i ( B [,] C ) ) -> w <_ C ) )
38	37	ralrimiv 2748	. . . . . . . . . . . . 13 |- ( ph -> A. w e. ( U i^i ( B [,] C ) ) w <_ C )
39		breq2 4176	. . . . . . . . . . . . . . 15 |- ( z = C -> ( w <_ z <-> w <_ C ) )
40	39	ralbidv 2686	. . . . . . . . . . . . . 14 |- ( z = C -> ( A. w e. ( U i^i ( B [,] C ) ) w <_ z <-> A. w e. ( U i^i ( B [,] C ) ) w <_ C ) )
41	40	rspcev 3012	. . . . . . . . . . . . 13 |- ( ( C e. RR /\ A. w e. ( U i^i ( B [,] C ) ) w <_ C ) -> E. z e. RR A. w e. ( U i^i ( B [,] C ) ) w <_ z )
42	23, 38, 41	syl2anc 643	. . . . . . . . . . . 12 |- ( ph -> E. z e. RR A. w e. ( U i^i ( B [,] C ) ) w <_ z )
43		suprcl 9924	. . . . . . . . . . . 12 |- ( ( ( U i^i ( B [,] C ) ) C_ RR /\ ( U i^i ( B [,] C ) ) =/= (/) /\ E. z e. RR A. w e. ( U i^i ( B [,] C ) ) w <_ z ) -> sup ( ( U i^i ( B [,] C ) ) , RR , < ) e. RR )
44	18, 31, 42, 43	syl3anc 1184	. . . . . . . . . . 11 |- ( ph -> sup ( ( U i^i ( B [,] C ) ) , RR , < ) e. RR )
45	1, 44	syl5eqel 2488	. . . . . . . . . 10 |- ( ph -> S e. RR )
46		rphalfcl 10592	. . . . . . . . . 10 |- ( r e. RR+ -> ( r / 2 ) e. RR+ )
47		ltaddrp 10600	. . . . . . . . . 10 |- ( ( S e. RR /\ ( r / 2 ) e. RR+ ) -> S < ( S + ( r / 2 ) ) )
48	45, 46, 47	syl2an 464	. . . . . . . . 9 |- ( ( ph /\ r e. RR+ ) -> S < ( S + ( r / 2 ) ) )
49	45	adantr 452	. . . . . . . . . 10 |- ( ( ph /\ r e. RR+ ) -> S e. RR )
50	46	rpred 10604	. . . . . . . . . . 11 |- ( r e. RR+ -> ( r / 2 ) e. RR )
51		readdcl 9029	. . . . . . . . . . 11 |- ( ( S e. RR /\ ( r / 2 ) e. RR ) -> ( S + ( r / 2 ) ) e. RR )
52	45, 50, 51	syl2an 464	. . . . . . . . . 10 |- ( ( ph /\ r e. RR+ ) -> ( S + ( r / 2 ) ) e. RR )
53	49, 52	ltnled 9176	. . . . . . . . 9 |- ( ( ph /\ r e. RR+ ) -> ( S < ( S + ( r / 2 ) ) <-> -. ( S + ( r / 2 ) ) <_ S ) )
54	48, 53	mpbid 202	. . . . . . . 8 |- ( ( ph /\ r e. RR+ ) -> -. ( S + ( r / 2 ) ) <_ S )
55	18	ad2antrr 707	. . . . . . . . . 10 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> ( U i^i ( B [,] C ) ) C_ RR )
56	31	ad2antrr 707	. . . . . . . . . 10 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> ( U i^i ( B [,] C ) ) =/= (/) )
57	42	ad2antrr 707	. . . . . . . . . 10 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> E. z e. RR A. w e. ( U i^i ( B [,] C ) ) w <_ z )
58		inss1 3521	. . . . . . . . . . . 12 |- ( U i^i ( -oo (,) C ) ) C_ U
59		simpr 448	. . . . . . . . . . . 12 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) )
60	58, 59	sseldi 3306	. . . . . . . . . . 11 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> ( S + ( r / 2 ) ) e. U )
61	52	adantr 452	. . . . . . . . . . . 12 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> ( S + ( r / 2 ) ) e. RR )
62	21	ad2antrr 707	. . . . . . . . . . . . 13 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> B e. RR )
63	45	ad2antrr 707	. . . . . . . . . . . . 13 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> S e. RR )
64		suprub 9925	. . . . . . . . . . . . . . . 16 |- ( ( ( ( U i^i ( B [,] C ) ) C_ RR /\ ( U i^i ( B [,] C ) ) =/= (/) /\ E. z e. RR A. w e. ( U i^i ( B [,] C ) ) w <_ z ) /\ B e. ( U i^i ( B [,] C ) ) ) -> B <_ sup ( ( U i^i ( B [,] C ) ) , RR , < ) )
65	18, 31, 42, 29, 64	syl31anc 1187	. . . . . . . . . . . . . . 15 |- ( ph -> B <_ sup ( ( U i^i ( B [,] C ) ) , RR , < ) )
66	65, 1	syl6breqr 4212	. . . . . . . . . . . . . 14 |- ( ph -> B <_ S )
67	66	ad2antrr 707	. . . . . . . . . . . . 13 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> B <_ S )
68	48	adantr 452	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> S < ( S + ( r / 2 ) ) )
69	63, 61, 68	ltled 9177	. . . . . . . . . . . . 13 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> S <_ ( S + ( r / 2 ) ) )
70	62, 63, 61, 67, 69	letrd 9183	. . . . . . . . . . . 12 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> B <_ ( S + ( r / 2 ) ) )
71	23	ad2antrr 707	. . . . . . . . . . . . 13 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> C e. RR )
72		inss2 3522	. . . . . . . . . . . . . . 15 |- ( U i^i ( -oo (,) C ) ) C_ ( -oo (,) C )
73	72, 59	sseldi 3306	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> ( S + ( r / 2 ) ) e. ( -oo (,) C ) )
74		eliooord 10926	. . . . . . . . . . . . . . 15 |- ( ( S + ( r / 2 ) ) e. ( -oo (,) C ) -> ( -oo < ( S + ( r / 2 ) ) /\ ( S + ( r / 2 ) ) < C ) )
75	74	simprd 450	. . . . . . . . . . . . . 14 |- ( ( S + ( r / 2 ) ) e. ( -oo (,) C ) -> ( S + ( r / 2 ) ) < C )
76	73, 75	syl 16	. . . . . . . . . . . . 13 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> ( S + ( r / 2 ) ) < C )
77	61, 71, 76	ltled 9177	. . . . . . . . . . . 12 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> ( S + ( r / 2 ) ) <_ C )
78		elicc2 10931	. . . . . . . . . . . . 13 |- ( ( B e. RR /\ C e. RR ) -> ( ( S + ( r / 2 ) ) e. ( B [,] C ) <-> ( ( S + ( r / 2 ) ) e. RR /\ B <_ ( S + ( r / 2 ) ) /\ ( S + ( r / 2 ) ) <_ C ) ) )
79	62, 71, 78	syl2anc 643	. . . . . . . . . . . 12 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> ( ( S + ( r / 2 ) ) e. ( B [,] C ) <-> ( ( S + ( r / 2 ) ) e. RR /\ B <_ ( S + ( r / 2 ) ) /\ ( S + ( r / 2 ) ) <_ C ) ) )
80	61, 70, 77, 79	mpbir3and 1137	. . . . . . . . . . 11 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> ( S + ( r / 2 ) ) e. ( B [,] C ) )
81		elin 3490	. . . . . . . . . . 11 |- ( ( S + ( r / 2 ) ) e. ( U i^i ( B [,] C ) ) <-> ( ( S + ( r / 2 ) ) e. U /\ ( S + ( r / 2 ) ) e. ( B [,] C ) ) )
82	60, 80, 81	sylanbrc 646	. . . . . . . . . 10 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> ( S + ( r / 2 ) ) e. ( U i^i ( B [,] C ) ) )
83		suprub 9925	. . . . . . . . . 10 |- ( ( ( ( U i^i ( B [,] C ) ) C_ RR /\ ( U i^i ( B [,] C ) ) =/= (/) /\ E. z e. RR A. w e. ( U i^i ( B [,] C ) ) w <_ z ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( B [,] C ) ) ) -> ( S + ( r / 2 ) ) <_ sup ( ( U i^i ( B [,] C ) ) , RR , < ) )
84	55, 56, 57, 82, 83	syl31anc 1187	. . . . . . . . 9 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> ( S + ( r / 2 ) ) <_ sup ( ( U i^i ( B [,] C ) ) , RR , < ) )
85	84, 1	syl6breqr 4212	. . . . . . . 8 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> ( S + ( r / 2 ) ) <_ S )
86	54, 85	mtand 641	. . . . . . 7 |- ( ( ph /\ r e. RR+ ) -> -. ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) )
87		eqid 2404	. . . . . . . . . . . . 13 |- ( ( abs o. - ) |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) )
88	87	remetdval 18773	. . . . . . . . . . . 12 |- ( ( ( S + ( r / 2 ) ) e. RR /\ S e. RR ) -> ( ( S + ( r / 2 ) ) ( ( abs o. - ) |` ( RR X. RR ) ) S ) = ( abs ` ( ( S + ( r / 2 ) ) - S ) ) )
89	52, 49, 88	syl2anc 643	. . . . . . . . . . 11 |- ( ( ph /\ r e. RR+ ) -> ( ( S + ( r / 2 ) ) ( ( abs o. - ) |` ( RR X. RR ) ) S ) = ( abs ` ( ( S + ( r / 2 ) ) - S ) ) )
90	49	recnd 9070	. . . . . . . . . . . . 13 |- ( ( ph /\ r e. RR+ ) -> S e. CC )
91	50	adantl 453	. . . . . . . . . . . . . 14 |- ( ( ph /\ r e. RR+ ) -> ( r / 2 ) e. RR )
92	91	recnd 9070	. . . . . . . . . . . . 13 |- ( ( ph /\ r e. RR+ ) -> ( r / 2 ) e. CC )
93	90, 92	pncan2d 9369	. . . . . . . . . . . 12 |- ( ( ph /\ r e. RR+ ) -> ( ( S + ( r / 2 ) ) - S ) = ( r / 2 ) )
94	93	fveq2d 5691	. . . . . . . . . . 11 |- ( ( ph /\ r e. RR+ ) -> ( abs ` ( ( S + ( r / 2 ) ) - S ) ) = ( abs ` ( r / 2 ) ) )
95	46	adantl 453	. . . . . . . . . . . 12 |- ( ( ph /\ r e. RR+ ) -> ( r / 2 ) e. RR+ )
96		rpre 10574	. . . . . . . . . . . . 13 |- ( ( r / 2 ) e. RR+ -> ( r / 2 ) e. RR )
97		rpge0 10580	. . . . . . . . . . . . 13 |- ( ( r / 2 ) e. RR+ -> 0 <_ ( r / 2 ) )
98	96, 97	absidd 12180	. . . . . . . . . . . 12 |- ( ( r / 2 ) e. RR+ -> ( abs ` ( r / 2 ) ) = ( r / 2 ) )
99	95, 98	syl 16	. . . . . . . . . . 11 |- ( ( ph /\ r e. RR+ ) -> ( abs ` ( r / 2 ) ) = ( r / 2 ) )
100	89, 94, 99	3eqtrd 2440	. . . . . . . . . 10 |- ( ( ph /\ r e. RR+ ) -> ( ( S + ( r / 2 ) ) ( ( abs o. - ) |` ( RR X. RR ) ) S ) = ( r / 2 ) )
101		rphalflt 10594	. . . . . . . . . . 11 |- ( r e. RR+ -> ( r / 2 ) < r )
102	101	adantl 453	. . . . . . . . . 10 |- ( ( ph /\ r e. RR+ ) -> ( r / 2 ) < r )
103	100, 102	eqbrtrd 4192	. . . . . . . . 9 |- ( ( ph /\ r e. RR+ ) -> ( ( S + ( r / 2 ) ) ( ( abs o. - ) |` ( RR X. RR ) ) S ) < r )
104	87	rexmet 18775	. . . . . . . . . . 11 |- ( ( abs o. - ) |` ( RR X. RR ) ) e. ( * Met ` RR )
105	104	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ r e. RR+ ) -> ( ( abs o. - ) |` ( RR X. RR ) ) e. ( * Met ` RR ) )
106		rpxr 10575	. . . . . . . . . . 11 |- ( r e. RR+ -> r e. RR* )
107	106	adantl 453	. . . . . . . . . 10 |- ( ( ph /\ r e. RR+ ) -> r e. RR* )
108		elbl3 18375	. . . . . . . . . 10 |- ( ( ( ( ( abs o. - ) |` ( RR X. RR ) ) e. ( * Met ` RR ) /\ r e. RR* ) /\ ( S e. RR /\ ( S + ( r / 2 ) ) e. RR ) ) -> ( ( S + ( r / 2 ) ) e. ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) <-> ( ( S + ( r / 2 ) ) ( ( abs o. - ) |` ( RR X. RR ) ) S ) < r ) )
109	105, 107, 49, 52, 108	syl22anc 1185	. . . . . . . . 9 |- ( ( ph /\ r e. RR+ ) -> ( ( S + ( r / 2 ) ) e. ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) <-> ( ( S + ( r / 2 ) ) ( ( abs o. - ) |` ( RR X. RR ) ) S ) < r ) )
110	103, 109	mpbird 224	. . . . . . . 8 |- ( ( ph /\ r e. RR+ ) -> ( S + ( r / 2 ) ) e. ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) )
111		ssel 3302	. . . . . . . 8 |- ( ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ ( U i^i ( -oo (,) C ) ) -> ( ( S + ( r / 2 ) ) e. ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) -> ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) )
112	110, 111	syl5com 28	. . . . . . 7 |- ( ( ph /\ r e. RR+ ) -> ( ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ ( U i^i ( -oo (,) C ) ) -> ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) )
113	86, 112	mtod 170	. . . . . 6 |- ( ( ph /\ r e. RR+ ) -> -. ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ ( U i^i ( -oo (,) C ) ) )
114	113	nrexdv 2769	. . . . 5 |- ( ph -> -. E. r e. RR+ ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ ( U i^i ( -oo (,) C ) ) )
115	45	adantr 452	. . . . . . . . 9 |- ( ( ph /\ S e. U ) -> S e. RR )
116		mnflt 10678	. . . . . . . . . 10 |- ( S e. RR -> -oo < S )
117	115, 116	syl 16	. . . . . . . . 9 |- ( ( ph /\ S e. U ) -> -oo < S )
118		suprleub 9928	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( U i^i ( B [,] C ) ) C_ RR /\ ( U i^i ( B [,] C ) ) =/= (/) /\ E. z e. RR A. w e. ( U i^i ( B [,] C ) ) w <_ z ) /\ C e. RR ) -> ( sup ( ( U i^i ( B [,] C ) ) , RR , < ) <_ C <-> A. w e. ( U i^i ( B [,] C ) ) w <_ C ) )
119	18, 31, 42, 23, 118	syl31anc 1187	. . . . . . . . . . . . . . . 16 |- ( ph -> ( sup ( ( U i^i ( B [,] C ) ) , RR , < ) <_ C <-> A. w e. ( U i^i ( B [,] C ) ) w <_ C ) )
120	38, 119	mpbird 224	. . . . . . . . . . . . . . 15 |- ( ph -> sup ( ( U i^i ( B [,] C ) ) , RR , < ) <_ C )
121	1, 120	syl5eqbr 4205	. . . . . . . . . . . . . 14 |- ( ph -> S <_ C )
122	45, 23	leloed 9172	. . . . . . . . . . . . . 14 |- ( ph -> ( S <_ C <-> ( S < C \/ S = C ) ) )
123	121, 122	mpbid 202	. . . . . . . . . . . . 13 |- ( ph -> ( S < C \/ S = C ) )
124	123	ord 367	. . . . . . . . . . . 12 |- ( ph -> ( -. S < C -> S = C ) )
125		elndif 3431	. . . . . . . . . . . . . . 15 |- ( C e. A -> -. C e. ( RR \ A ) )
126	8, 125	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> -. C e. ( RR \ A ) )
127		inss1 3521	. . . . . . . . . . . . . . . 16 |- ( V i^i A ) C_ V
128	127, 7	sseldi 3306	. . . . . . . . . . . . . . 15 |- ( ph -> C e. V )
129		elin 3490	. . . . . . . . . . . . . . . 16 |- ( C e. ( U i^i V ) <-> ( C e. U /\ C e. V ) )
130		reconnlem2.7	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( U i^i V ) C_ ( RR \ A ) )
131	130	sseld 3307	. . . . . . . . . . . . . . . 16 |- ( ph -> ( C e. ( U i^i V ) -> C e. ( RR \ A ) ) )
132	129, 131	syl5bir 210	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( C e. U /\ C e. V ) -> C e. ( RR \ A ) ) )
133	128, 132	mpan2d 656	. . . . . . . . . . . . . 14 |- ( ph -> ( C e. U -> C e. ( RR \ A ) ) )
134	126, 133	mtod 170	. . . . . . . . . . . . 13 |- ( ph -> -. C e. U )
135		eleq1 2464	. . . . . . . . . . . . . 14 |- ( S = C -> ( S e. U <-> C e. U ) )
136	135	notbid 286	. . . . . . . . . . . . 13 |- ( S = C -> ( -. S e. U <-> -. C e. U ) )
137	134, 136	syl5ibrcom 214	. . . . . . . . . . . 12 |- ( ph -> ( S = C -> -. S e. U ) )
138	124, 137	syld 42	. . . . . . . . . . 11 |- ( ph -> ( -. S < C -> -. S e. U ) )
139	138	con4d 99	. . . . . . . . . 10 |- ( ph -> ( S e. U -> S < C ) )
140	139	imp 419	. . . . . . . . 9 |- ( ( ph /\ S e. U ) -> S < C )
141		mnfxr 10670	. . . . . . . . . . 11 |- -oo e. RR*
142		elioo2 10913	. . . . . . . . . . 11 |- ( ( -oo e. RR* /\ C e. RR* ) -> ( S e. ( -oo (,) C ) <-> ( S e. RR /\ -oo < S /\ S < C ) ) )
143	141, 24, 142	sylancr 645	. . . . . . . . . 10 |- ( ph -> ( S e. ( -oo (,) C ) <-> ( S e. RR /\ -oo < S /\ S < C ) ) )
144	143	adantr 452	. . . . . . . . 9 |- ( ( ph /\ S e. U ) -> ( S e. ( -oo (,) C ) <-> ( S e. RR /\ -oo < S /\ S < C ) ) )
145	115, 117, 140, 144	mpbir3and 1137	. . . . . . . 8 |- ( ( ph /\ S e. U ) -> S e. ( -oo (,) C ) )
146	145	ex 424	. . . . . . 7 |- ( ph -> ( S e. U -> S e. ( -oo (,) C ) ) )
147	146	ancld 537	. . . . . 6 |- ( ph -> ( S e. U -> ( S e. U /\ S e. ( -oo (,) C ) ) ) )
148		elin 3490	. . . . . . 7 |- ( S e. ( U i^i ( -oo (,) C ) ) <-> ( S e. U /\ S e. ( -oo (,) C ) ) )
149		reconnlem2.2	. . . . . . . 8 |- ( ph -> U e. ( topGen ` ran (,) ) )
150		retop 18748	. . . . . . . . 9 |- ( topGen ` ran (,) ) e. Top
151		iooretop 18753	. . . . . . . . 9 |- ( -oo (,) C ) e. ( topGen ` ran (,) )
152		inopn 16927	. . . . . . . . 9 |- ( ( ( topGen ` ran (,) ) e. Top /\ U e. ( topGen ` ran (,) ) /\ ( -oo (,) C ) e. ( topGen ` ran (,) ) ) -> ( U i^i ( -oo (,) C ) ) e. ( topGen ` ran (,) ) )
153	150, 151, 152	mp3an13 1270	. . . . . . . 8 |- ( U e. ( topGen ` ran (,) ) -> ( U i^i ( -oo (,) C ) ) e. ( topGen ` ran (,) ) )
154		eqid 2404	. . . . . . . . . . . 12 |- ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
155	87, 154	tgioo 18780	. . . . . . . . . . 11 |- ( topGen ` ran (,) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
156	155	mopni2 18476	. . . . . . . . . 10 |- ( ( ( ( abs o. - ) |` ( RR X. RR ) ) e. ( * Met ` RR ) /\ ( U i^i ( -oo (,) C ) ) e. ( topGen ` ran (,) ) /\ S e. ( U i^i ( -oo (,) C ) ) ) -> E. r e. RR+ ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ ( U i^i ( -oo (,) C ) ) )
157	104, 156	mp3an1 1266	. . . . . . . . 9 |- ( ( ( U i^i ( -oo (,) C ) ) e. ( topGen ` ran (,) ) /\ S e. ( U i^i ( -oo (,) C ) ) ) -> E. r e. RR+ ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ ( U i^i ( -oo (,) C ) ) )
158	157	ex 424	. . . . . . . 8 |- ( ( U i^i ( -oo (,) C ) ) e. ( topGen ` ran (,) ) -> ( S e. ( U i^i ( -oo (,) C ) ) -> E. r e. RR+ ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ ( U i^i ( -oo (,) C ) ) ) )
159	149, 153, 158	3syl 19	. . . . . . 7 |- ( ph -> ( S e. ( U i^i ( -oo (,) C ) ) -> E. r e. RR+ ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ ( U i^i ( -oo (,) C ) ) ) )
160	148, 159	syl5bir 210	. . . . . 6 |- ( ph -> ( ( S e. U /\ S e. ( -oo (,) C ) ) -> E. r e. RR+ ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ ( U i^i ( -oo (,) C ) ) ) )
161	147, 160	syld 42	. . . . 5 |- ( ph -> ( S e. U -> E. r e. RR+ ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ ( U i^i ( -oo (,) C ) ) ) )
162	114, 161	mtod 170	. . . 4 |- ( ph -> -. S e. U )
163		ltsubrp 10599	. . . . . . . . 9 |- ( ( S e. RR /\ r e. RR+ ) -> ( S - r ) < S )
164	45, 163	sylan 458	. . . . . . . 8 |- ( ( ph /\ r e. RR+ ) -> ( S - r ) < S )
165		rpre 10574	. . . . . . . . . 10 |- ( r e. RR+ -> r e. RR )
166		resubcl 9321	. . . . . . . . . 10 |- ( ( S e. RR /\ r e. RR ) -> ( S - r ) e. RR )
167	45, 165, 166	syl2an 464	. . . . . . . . 9 |- ( ( ph /\ r e. RR+ ) -> ( S - r ) e. RR )
168	167, 49	ltnled 9176	. . . . . . . 8 |- ( ( ph /\ r e. RR+ ) -> ( ( S - r ) < S <-> -. S <_ ( S - r ) ) )
169	164, 168	mpbid 202	. . . . . . 7 |- ( ( ph /\ r e. RR+ ) -> -. S <_ ( S - r ) )
170	87	bl2ioo 18776	. . . . . . . . . 10 |- ( ( S e. RR /\ r e. RR ) -> ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) = ( ( S - r ) (,) ( S + r ) ) )
171	45, 165, 170	syl2an 464	. . . . . . . . 9 |- ( ( ph /\ r e. RR+ ) -> ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) = ( ( S - r ) (,) ( S + r ) ) )
172	171	sseq1d 3335	. . . . . . . 8 |- ( ( ph /\ r e. RR+ ) -> ( ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ V <-> ( ( S - r ) (,) ( S + r ) ) C_ V ) )
173	15	ad2antrr 707	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) -> ( B [,] C ) C_ A )
174	2, 173	syl5ss 3319	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) -> ( U i^i ( B [,] C ) ) C_ A )
175	174	sselda 3308	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ w e. ( U i^i ( B [,] C ) ) ) -> w e. A )
176		elndif 3431	. . . . . . . . . . . . . . 15 |- ( w e. A -> -. w e. ( RR \ A ) )
177	175, 176	syl 16	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ w e. ( U i^i ( B [,] C ) ) ) -> -. w e. ( RR \ A ) )
178	130	ad3antrrr 711	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> ( U i^i V ) C_ ( RR \ A ) )
179		inss1 3521	. . . . . . . . . . . . . . . . . 18 |- ( U i^i ( B [,] C ) ) C_ U
180		simprl 733	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> w e. ( U i^i ( B [,] C ) ) )
181	179, 180	sseldi 3306	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> w e. U )
182		simplr 732	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> ( ( S - r ) (,) ( S + r ) ) C_ V )
183	18	ad3antrrr 711	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ w e. ( U i^i ( B [,] C ) ) ) -> ( U i^i ( B [,] C ) ) C_ RR )
184		simpr 448	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ w e. ( U i^i ( B [,] C ) ) ) -> w e. ( U i^i ( B [,] C ) ) )
185	183, 184	sseldd 3309	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ w e. ( U i^i ( B [,] C ) ) ) -> w e. RR )
186	185	adantrr 698	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> w e. RR )
187		simprr 734	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> ( S - r ) < w )
188	49	ad2antrr 707	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> S e. RR )
189		simpllr 736	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> r e. RR+ )
190	189	rpred 10604	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> r e. RR )
191	188, 190	readdcld 9071	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> ( S + r ) e. RR )
192	183	adantrr 698	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> ( U i^i ( B [,] C ) ) C_ RR )
193	31	ad3antrrr 711	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> ( U i^i ( B [,] C ) ) =/= (/) )
194	42	ad3antrrr 711	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> E. z e. RR A. w e. ( U i^i ( B [,] C ) ) w <_ z )
195		suprub 9925	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( U i^i ( B [,] C ) ) C_ RR /\ ( U i^i ( B [,] C ) ) =/= (/) /\ E. z e. RR A. w e. ( U i^i ( B [,] C ) ) w <_ z ) /\ w e. ( U i^i ( B [,] C ) ) ) -> w <_ sup ( ( U i^i ( B [,] C ) ) , RR , < ) )
196	192, 193, 194, 180, 195	syl31anc 1187	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> w <_ sup ( ( U i^i ( B [,] C ) ) , RR , < ) )
197	196, 1	syl6breqr 4212	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> w <_ S )
198	188, 189	ltaddrpd 10633	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> S < ( S + r ) )
199	186, 188, 191, 197, 198	lelttrd 9184	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> w < ( S + r ) )
200	167	ad2antrr 707	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> ( S - r ) e. RR )
201		rexr 9086	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( S - r ) e. RR -> ( S - r ) e. RR* )
202		rexr 9086	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( S + r ) e. RR -> ( S + r ) e. RR* )
203		elioo2 10913	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( S - r ) e. RR* /\ ( S + r ) e. RR* ) -> ( w e. ( ( S - r ) (,) ( S + r ) ) <-> ( w e. RR /\ ( S - r ) < w /\ w < ( S + r ) ) ) )
204	201, 202, 203	syl2an 464	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( S - r ) e. RR /\ ( S + r ) e. RR ) -> ( w e. ( ( S - r ) (,) ( S + r ) ) <-> ( w e. RR /\ ( S - r ) < w /\ w < ( S + r ) ) ) )
205	200, 191, 204	syl2anc 643	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> ( w e. ( ( S - r ) (,) ( S + r ) ) <-> ( w e. RR /\ ( S - r ) < w /\ w < ( S + r ) ) ) )
206	186, 187, 199, 205	mpbir3and 1137	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> w e. ( ( S - r ) (,) ( S + r ) ) )
207	182, 206	sseldd 3309	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> w e. V )
208		elin 3490	. . . . . . . . . . . . . . . . 17 |- ( w e. ( U i^i V ) <-> ( w e. U /\ w e. V ) )
209	181, 207, 208	sylanbrc 646	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> w e. ( U i^i V ) )
210	178, 209	sseldd 3309	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> w e. ( RR \ A ) )
211	210	expr 599	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ w e. ( U i^i ( B [,] C ) ) ) -> ( ( S - r ) < w -> w e. ( RR \ A ) ) )
212	177, 211	mtod 170	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ w e. ( U i^i ( B [,] C ) ) ) -> -. ( S - r ) < w )
213	167	ad2antrr 707	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ w e. ( U i^i ( B [,] C ) ) ) -> ( S - r ) e. RR )
214	185, 213	lenltd 9175	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ w e. ( U i^i ( B [,] C ) ) ) -> ( w <_ ( S - r ) <-> -. ( S - r ) < w ) )
215	212, 214	mpbird 224	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ w e. ( U i^i ( B [,] C ) ) ) -> w <_ ( S - r ) )
216	215	ralrimiva 2749	. . . . . . . . . . 11 |- ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) -> A. w e. ( U i^i ( B [,] C ) ) w <_ ( S - r ) )
217	18	ad2antrr 707	. . . . . . . . . . . 12 |- ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) -> ( U i^i ( B [,] C ) ) C_ RR )
218	31	ad2antrr 707	. . . . . . . . . . . 12 |- ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) -> ( U i^i ( B [,] C ) ) =/= (/) )
219	42	ad2antrr 707	. . . . . . . . . . . 12 |- ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) -> E. z e. RR A. w e. ( U i^i ( B [,] C ) ) w <_ z )
220	167	adantr 452	. . . . . . . . . . . 12 |- ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) -> ( S - r ) e. RR )
221		suprleub 9928	. . . . . . . . . . . 12 |- ( ( ( ( U i^i ( B [,] C ) ) C_ RR /\ ( U i^i ( B [,] C ) ) =/= (/) /\ E. z e. RR A. w e. ( U i^i ( B [,] C ) ) w <_ z ) /\ ( S - r ) e. RR ) -> ( sup ( ( U i^i ( B [,] C ) ) , RR , < ) <_ ( S - r ) <-> A. w e. ( U i^i ( B [,] C ) ) w <_ ( S - r ) ) )
222	217, 218, 219, 220, 221	syl31anc 1187	. . . . . . . . . . 11 |- ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) -> ( sup ( ( U i^i ( B [,] C ) ) , RR , < ) <_ ( S - r ) <-> A. w e. ( U i^i ( B [,] C ) ) w <_ ( S - r ) ) )
223	216, 222	mpbird 224	. . . . . . . . . 10 |- ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) -> sup ( ( U i^i ( B [,] C ) ) , RR , < ) <_ ( S - r ) )
224	1, 223	syl5eqbr 4205	. . . . . . . . 9 |- ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) -> S <_ ( S - r ) )
225	224	ex 424	. . . . . . . 8 |- ( ( ph /\ r e. RR+ ) -> ( ( ( S - r ) (,) ( S + r ) ) C_ V -> S <_ ( S - r ) ) )
226	172, 225	sylbid 207	. . . . . . 7 |- ( ( ph /\ r e. RR+ ) -> ( ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ V -> S <_ ( S - r ) ) )
227	169, 226	mtod 170	. . . . . 6 |- ( ( ph /\ r e. RR+ ) -> -. ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ V )
228	227	nrexdv 2769	. . . . 5 |- ( ph -> -. E. r e. RR+ ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ V )
229		reconnlem2.3	. . . . . 6 |- ( ph -> V e. ( topGen ` ran (,) ) )
230	155	mopni2 18476	. . . . . . . 8 |- ( ( ( ( abs o. - ) |` ( RR X. RR ) ) e. ( * Met ` RR ) /\ V e. ( topGen ` ran (,) ) /\ S e. V ) -> E. r e. RR+ ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ V )
231	104, 230	mp3an1 1266	. . . . . . 7 |- ( ( V e. ( topGen ` ran (,) ) /\ S e. V ) -> E. r e. RR+ ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ V )
232	231	ex 424	. . . . . 6 |- ( V e. ( topGen ` ran (,) ) -> ( S e. V -> E. r e. RR+ ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ V ) )
233	229, 232	syl 16	. . . . 5 |- ( ph -> ( S e. V -> E. r e. RR+ ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ V ) )
234	228, 233	mtod 170	. . . 4 |- ( ph -> -. S e. V )
235		ioran 477	. . . 4 |- ( -. ( S e. U \/ S e. V ) <-> ( -. S e. U /\ -. S e. V ) )
236	162, 234, 235	sylanbrc 646	. . 3 |- ( ph -> -. ( S e. U \/ S e. V ) )
237		elun 3448	. . 3 |- ( S e. ( U u. V ) <-> ( S e. U \/ S e. V ) )
238	236, 237	sylnibr 297	. 2 |- ( ph -> -. S e. ( U u. V ) )
239		elicc2 10931	. . . . . 6 |- ( ( B e. RR /\ C e. RR ) -> ( S e. ( B [,] C ) <-> ( S e. RR /\ B <_ S /\ S <_ C ) ) )
240	21, 23, 239	syl2anc 643	. . . . 5 |- ( ph -> ( S e. ( B [,] C ) <-> ( S e. RR /\ B <_ S /\ S <_ C ) ) )
241	45, 66, 121, 240	mpbir3and 1137	. . . 4 |- ( ph -> S e. ( B [,] C ) )
242	15, 241	sseldd 3309	. . 3 |- ( ph -> S e. A )
243		ssel 3302	. . 3 |- ( A C_ ( U u. V ) -> ( S e. A -> S e. ( U u. V ) ) )
244	242, 243	syl5com 28	. 2 |- ( ph -> ( A C_ ( U u. V ) -> S e. ( U u. V ) ) )
245	238, 244	mtod 170	1 |- ( ph -> -. A C_ ( U u. V ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 177   \/ wo 358   /\ wa 359   /\ w3a 936   = wceq 1649   e. wcel 1721   =/= wne 2567   A.wral 2666   E.wrex 2667   \ cdif 3277   u. cun 3278   i^i cin 3279   C_ wss 3280   (/)c0 3588   class class class wbr 4172   X. cxp 4835   ran crn 4838   |` cres 4839   o. ccom 4841   ` cfv 5413  (class class class)co 6040   supcsup 7403   RRcr 8945   + caddc 8949   -oocmnf 9074   RR*cxr 9075   < clt 9076   <_ cle 9077   - cmin 9247   / cdiv 9633   2c2 10005   RR+crp 10568   (,)cioo 10872   [,]cicc 10875   abscabs 11994   topGenctg 13620   * Metcxmt 16641   ballcbl 16643   MetOpencmopn 16646   Topctop 16913

This theorem is referenced by:  reconn  18812

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023  ax-pre-sup 9024

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-er 6864  df-map 6979  df-en 7069  df-dom 7070  df-sdom 7071  df-sup 7404  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-div 9634  df-nn 9957  df-2 10014  df-3 10015  df-n0 10178  df-z 10239  df-uz 10445  df-q 10531  df-rp 10569  df-xneg 10666  df-xadd 10667  df-xmul 10668  df-ioo 10876  df-icc 10879  df-seq 11279  df-exp 11338  df-cj 11859  df-re 11860  df-im 11861  df-sqr 11995  df-abs 11996  df-topgen 13622  df-psmet 16649  df-xmet 16650  df-met 16651  df-bl 16652  df-mopn 16653  df-top 16918  df-bases 16920  df-topon 16921