Theorem reconnlem2 22630

Description: Lemma for reconn 22631. (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 3834	. . . . . . . . . . . . 13 |- ( U i^i ( B [,] C ) ) C_ ( B [,] C )
3		inss2 3834	. . . . . . . . . . . . . . . 16 |- ( U i^i A ) C_ A
4		reconnlem2.5	. . . . . . . . . . . . . . . 16 |- ( ph -> B e. ( U i^i A ) )
5	3, 4	sseldi 3601	. . . . . . . . . . . . . . 15 |- ( ph -> B e. A )
6		inss2 3834	. . . . . . . . . . . . . . . 16 |- ( V i^i A ) C_ A
7		reconnlem2.6	. . . . . . . . . . . . . . . 16 |- ( ph -> C e. ( V i^i A ) )
8	6, 7	sseldi 3601	. . . . . . . . . . . . . . 15 |- ( ph -> C e. A )
9		reconnlem2.4	. . . . . . . . . . . . . . 15 |- ( ph -> A. x e. A A. y e. A ( x [,] y ) C_ A )
10		oveq1 6657	. . . . . . . . . . . . . . . . 17 |- ( x = B -> ( x [,] y ) = ( B [,] y ) )
11	10	sseq1d 3632	. . . . . . . . . . . . . . . 16 |- ( x = B -> ( ( x [,] y ) C_ A <-> ( B [,] y ) C_ A ) )
12		oveq2 6658	. . . . . . . . . . . . . . . . 17 |- ( y = C -> ( B [,] y ) = ( B [,] C ) )
13	12	sseq1d 3632	. . . . . . . . . . . . . . . 16 |- ( y = C -> ( ( B [,] y ) C_ A <-> ( B [,] C ) C_ A ) )
14	11, 13	rspc2va 3323	. . . . . . . . . . . . . . 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 1325	. . . . . . . . . . . . . 14 |- ( ph -> ( B [,] C ) C_ A )
16		reconnlem2.1	. . . . . . . . . . . . . 14 |- ( ph -> A C_ RR )
17	15, 16	sstrd 3613	. . . . . . . . . . . . 13 |- ( ph -> ( B [,] C ) C_ RR )
18	2, 17	syl5ss 3614	. . . . . . . . . . . 12 |- ( ph -> ( U i^i ( B [,] C ) ) C_ RR )
19		inss1 3833	. . . . . . . . . . . . . . 15 |- ( U i^i A ) C_ U
20	19, 4	sseldi 3601	. . . . . . . . . . . . . 14 |- ( ph -> B e. U )
21	16, 5	sseldd 3604	. . . . . . . . . . . . . . . 16 |- ( ph -> B e. RR )
22	21	rexrd 10089	. . . . . . . . . . . . . . 15 |- ( ph -> B e. RR* )
23	16, 8	sseldd 3604	. . . . . . . . . . . . . . . 16 |- ( ph -> C e. RR )
24	23	rexrd 10089	. . . . . . . . . . . . . . 15 |- ( ph -> C e. RR* )
25		reconnlem2.8	. . . . . . . . . . . . . . 15 |- ( ph -> B <_ C )
26		lbicc2 12288	. . . . . . . . . . . . . . 15 |- ( ( B e. RR* /\ C e. RR* /\ B <_ C ) -> B e. ( B [,] C ) )
27	22, 24, 25, 26	syl3anc 1326	. . . . . . . . . . . . . 14 |- ( ph -> B e. ( B [,] C ) )
28	20, 27	elind 3798	. . . . . . . . . . . . 13 |- ( ph -> B e. ( U i^i ( B [,] C ) ) )
29		ne0i 3921	. . . . . . . . . . . . 13 |- ( B e. ( U i^i ( B [,] C ) ) -> ( U i^i ( B [,] C ) ) =/= (/) )
30	28, 29	syl 17	. . . . . . . . . . . 12 |- ( ph -> ( U i^i ( B [,] C ) ) =/= (/) )
31	2	sseli 3599	. . . . . . . . . . . . . . 15 |- ( w e. ( U i^i ( B [,] C ) ) -> w e. ( B [,] C ) )
32		elicc2 12238	. . . . . . . . . . . . . . . . 17 |- ( ( B e. RR /\ C e. RR ) -> ( w e. ( B [,] C ) <-> ( w e. RR /\ B <_ w /\ w <_ C ) ) )
33	21, 23, 32	syl2anc 693	. . . . . . . . . . . . . . . 16 |- ( ph -> ( w e. ( B [,] C ) <-> ( w e. RR /\ B <_ w /\ w <_ C ) ) )
34		simp3 1063	. . . . . . . . . . . . . . . 16 |- ( ( w e. RR /\ B <_ w /\ w <_ C ) -> w <_ C )
35	33, 34	syl6bi 243	. . . . . . . . . . . . . . 15 |- ( ph -> ( w e. ( B [,] C ) -> w <_ C ) )
36	31, 35	syl5 34	. . . . . . . . . . . . . 14 |- ( ph -> ( w e. ( U i^i ( B [,] C ) ) -> w <_ C ) )
37	36	ralrimiv 2965	. . . . . . . . . . . . 13 |- ( ph -> A. w e. ( U i^i ( B [,] C ) ) w <_ C )
38		breq2 4657	. . . . . . . . . . . . . . 15 |- ( z = C -> ( w <_ z <-> w <_ C ) )
39	38	ralbidv 2986	. . . . . . . . . . . . . 14 |- ( z = C -> ( A. w e. ( U i^i ( B [,] C ) ) w <_ z <-> A. w e. ( U i^i ( B [,] C ) ) w <_ C ) )
40	39	rspcev 3309	. . . . . . . . . . . . 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 )
41	23, 37, 40	syl2anc 693	. . . . . . . . . . . 12 |- ( ph -> E. z e. RR A. w e. ( U i^i ( B [,] C ) ) w <_ z )
42		suprcl 10983	. . . . . . . . . . . 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 )
43	18, 30, 41, 42	syl3anc 1326	. . . . . . . . . . 11 |- ( ph -> sup ( ( U i^i ( B [,] C ) ) , RR , < ) e. RR )
44	1, 43	syl5eqel 2705	. . . . . . . . . 10 |- ( ph -> S e. RR )
45		rphalfcl 11858	. . . . . . . . . 10 |- ( r e. RR+ -> ( r / 2 ) e. RR+ )
46		ltaddrp 11867	. . . . . . . . . 10 |- ( ( S e. RR /\ ( r / 2 ) e. RR+ ) -> S < ( S + ( r / 2 ) ) )
47	44, 45, 46	syl2an 494	. . . . . . . . 9 |- ( ( ph /\ r e. RR+ ) -> S < ( S + ( r / 2 ) ) )
48	44	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ r e. RR+ ) -> S e. RR )
49	45	rpred 11872	. . . . . . . . . . 11 |- ( r e. RR+ -> ( r / 2 ) e. RR )
50		readdcl 10019	. . . . . . . . . . 11 |- ( ( S e. RR /\ ( r / 2 ) e. RR ) -> ( S + ( r / 2 ) ) e. RR )
51	44, 49, 50	syl2an 494	. . . . . . . . . 10 |- ( ( ph /\ r e. RR+ ) -> ( S + ( r / 2 ) ) e. RR )
52	48, 51	ltnled 10184	. . . . . . . . 9 |- ( ( ph /\ r e. RR+ ) -> ( S < ( S + ( r / 2 ) ) <-> -. ( S + ( r / 2 ) ) <_ S ) )
53	47, 52	mpbid 222	. . . . . . . 8 |- ( ( ph /\ r e. RR+ ) -> -. ( S + ( r / 2 ) ) <_ S )
54	18	ad2antrr 762	. . . . . . . . . 10 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> ( U i^i ( B [,] C ) ) C_ RR )
55	30	ad2antrr 762	. . . . . . . . . 10 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> ( U i^i ( B [,] C ) ) =/= (/) )
56	41	ad2antrr 762	. . . . . . . . . 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 )
57		inss1 3833	. . . . . . . . . . . 12 |- ( U i^i ( -oo (,) C ) ) C_ U
58		simpr 477	. . . . . . . . . . . 12 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) )
59	57, 58	sseldi 3601	. . . . . . . . . . 11 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> ( S + ( r / 2 ) ) e. U )
60	51	adantr 481	. . . . . . . . . . . 12 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> ( S + ( r / 2 ) ) e. RR )
61	21	ad2antrr 762	. . . . . . . . . . . . 13 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> B e. RR )
62	44	ad2antrr 762	. . . . . . . . . . . . 13 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> S e. RR )
63		suprub 10984	. . . . . . . . . . . . . . . 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 , < ) )
64	18, 30, 41, 28, 63	syl31anc 1329	. . . . . . . . . . . . . . 15 |- ( ph -> B <_ sup ( ( U i^i ( B [,] C ) ) , RR , < ) )
65	64, 1	syl6breqr 4695	. . . . . . . . . . . . . 14 |- ( ph -> B <_ S )
66	65	ad2antrr 762	. . . . . . . . . . . . 13 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> B <_ S )
67	47	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> S < ( S + ( r / 2 ) ) )
68	62, 60, 67	ltled 10185	. . . . . . . . . . . . 13 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> S <_ ( S + ( r / 2 ) ) )
69	61, 62, 60, 66, 68	letrd 10194	. . . . . . . . . . . 12 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> B <_ ( S + ( r / 2 ) ) )
70	23	ad2antrr 762	. . . . . . . . . . . . 13 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> C e. RR )
71		inss2 3834	. . . . . . . . . . . . . . 15 |- ( U i^i ( -oo (,) C ) ) C_ ( -oo (,) C )
72	71, 58	sseldi 3601	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> ( S + ( r / 2 ) ) e. ( -oo (,) C ) )
73		eliooord 12233	. . . . . . . . . . . . . . 15 |- ( ( S + ( r / 2 ) ) e. ( -oo (,) C ) -> ( -oo < ( S + ( r / 2 ) ) /\ ( S + ( r / 2 ) ) < C ) )
74	73	simprd 479	. . . . . . . . . . . . . 14 |- ( ( S + ( r / 2 ) ) e. ( -oo (,) C ) -> ( S + ( r / 2 ) ) < C )
75	72, 74	syl 17	. . . . . . . . . . . . 13 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> ( S + ( r / 2 ) ) < C )
76	60, 70, 75	ltled 10185	. . . . . . . . . . . 12 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> ( S + ( r / 2 ) ) <_ C )
77		elicc2 12238	. . . . . . . . . . . . 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 ) ) )
78	61, 70, 77	syl2anc 693	. . . . . . . . . . . 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 ) ) )
79	60, 69, 76, 78	mpbir3and 1245	. . . . . . . . . . 11 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> ( S + ( r / 2 ) ) e. ( B [,] C ) )
80	59, 79	elind 3798	. . . . . . . . . 10 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> ( S + ( r / 2 ) ) e. ( U i^i ( B [,] C ) ) )
81		suprub 10984	. . . . . . . . . 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 , < ) )
82	54, 55, 56, 80, 81	syl31anc 1329	. . . . . . . . 9 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> ( S + ( r / 2 ) ) <_ sup ( ( U i^i ( B [,] C ) ) , RR , < ) )
83	82, 1	syl6breqr 4695	. . . . . . . 8 |- ( ( ( ph /\ r e. RR+ ) /\ ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) ) -> ( S + ( r / 2 ) ) <_ S )
84	53, 83	mtand 691	. . . . . . 7 |- ( ( ph /\ r e. RR+ ) -> -. ( S + ( r / 2 ) ) e. ( U i^i ( -oo (,) C ) ) )
85		eqid 2622	. . . . . . . . . . . . 13 |- ( ( abs o. - ) |` ( RR X. RR ) ) = ( ( abs o. - ) |` ( RR X. RR ) )
86	85	remetdval 22592	. . . . . . . . . . . 12 |- ( ( ( S + ( r / 2 ) ) e. RR /\ S e. RR ) -> ( ( S + ( r / 2 ) ) ( ( abs o. - ) |` ( RR X. RR ) ) S ) = ( abs ` ( ( S + ( r / 2 ) ) - S ) ) )
87	51, 48, 86	syl2anc 693	. . . . . . . . . . 11 |- ( ( ph /\ r e. RR+ ) -> ( ( S + ( r / 2 ) ) ( ( abs o. - ) |` ( RR X. RR ) ) S ) = ( abs ` ( ( S + ( r / 2 ) ) - S ) ) )
88	48	recnd 10068	. . . . . . . . . . . . 13 |- ( ( ph /\ r e. RR+ ) -> S e. CC )
89	49	adantl 482	. . . . . . . . . . . . . 14 |- ( ( ph /\ r e. RR+ ) -> ( r / 2 ) e. RR )
90	89	recnd 10068	. . . . . . . . . . . . 13 |- ( ( ph /\ r e. RR+ ) -> ( r / 2 ) e. CC )
91	88, 90	pncan2d 10394	. . . . . . . . . . . 12 |- ( ( ph /\ r e. RR+ ) -> ( ( S + ( r / 2 ) ) - S ) = ( r / 2 ) )
92	91	fveq2d 6195	. . . . . . . . . . 11 |- ( ( ph /\ r e. RR+ ) -> ( abs ` ( ( S + ( r / 2 ) ) - S ) ) = ( abs ` ( r / 2 ) ) )
93	45	adantl 482	. . . . . . . . . . . 12 |- ( ( ph /\ r e. RR+ ) -> ( r / 2 ) e. RR+ )
94		rpre 11839	. . . . . . . . . . . . 13 |- ( ( r / 2 ) e. RR+ -> ( r / 2 ) e. RR )
95		rpge0 11845	. . . . . . . . . . . . 13 |- ( ( r / 2 ) e. RR+ -> 0 <_ ( r / 2 ) )
96	94, 95	absidd 14161	. . . . . . . . . . . 12 |- ( ( r / 2 ) e. RR+ -> ( abs ` ( r / 2 ) ) = ( r / 2 ) )
97	93, 96	syl 17	. . . . . . . . . . 11 |- ( ( ph /\ r e. RR+ ) -> ( abs ` ( r / 2 ) ) = ( r / 2 ) )
98	87, 92, 97	3eqtrd 2660	. . . . . . . . . 10 |- ( ( ph /\ r e. RR+ ) -> ( ( S + ( r / 2 ) ) ( ( abs o. - ) |` ( RR X. RR ) ) S ) = ( r / 2 ) )
99		rphalflt 11860	. . . . . . . . . . 11 |- ( r e. RR+ -> ( r / 2 ) < r )
100	99	adantl 482	. . . . . . . . . 10 |- ( ( ph /\ r e. RR+ ) -> ( r / 2 ) < r )
101	98, 100	eqbrtrd 4675	. . . . . . . . 9 |- ( ( ph /\ r e. RR+ ) -> ( ( S + ( r / 2 ) ) ( ( abs o. - ) |` ( RR X. RR ) ) S ) < r )
102	85	rexmet 22594	. . . . . . . . . . 11 |- ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR )
103	102	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ r e. RR+ ) -> ( ( abs o. - ) |` ( RR X. RR ) ) e. ( *Met ` RR ) )
104		rpxr 11840	. . . . . . . . . . 11 |- ( r e. RR+ -> r e. RR* )
105	104	adantl 482	. . . . . . . . . 10 |- ( ( ph /\ r e. RR+ ) -> r e. RR* )
106		elbl3 22197	. . . . . . . . . 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 ) )
107	103, 105, 48, 51, 106	syl22anc 1327	. . . . . . . . 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 ) )
108	101, 107	mpbird 247	. . . . . . . 8 |- ( ( ph /\ r e. RR+ ) -> ( S + ( r / 2 ) ) e. ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) )
109		ssel 3597	. . . . . . . 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 ) ) ) )
110	108, 109	syl5com 31	. . . . . . 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 ) ) ) )
111	84, 110	mtod 189	. . . . . 6 |- ( ( ph /\ r e. RR+ ) -> -. ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ ( U i^i ( -oo (,) C ) ) )
112	111	nrexdv 3001	. . . . 5 |- ( ph -> -. E. r e. RR+ ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ ( U i^i ( -oo (,) C ) ) )
113	44	adantr 481	. . . . . . . . 9 |- ( ( ph /\ S e. U ) -> S e. RR )
114		mnflt 11957	. . . . . . . . . 10 |- ( S e. RR -> -oo < S )
115	113, 114	syl 17	. . . . . . . . 9 |- ( ( ph /\ S e. U ) -> -oo < S )
116		suprleub 10989	. . . . . . . . . . . . . . . . 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 ) )
117	18, 30, 41, 23, 116	syl31anc 1329	. . . . . . . . . . . . . . . 16 |- ( ph -> ( sup ( ( U i^i ( B [,] C ) ) , RR , < ) <_ C <-> A. w e. ( U i^i ( B [,] C ) ) w <_ C ) )
118	37, 117	mpbird 247	. . . . . . . . . . . . . . 15 |- ( ph -> sup ( ( U i^i ( B [,] C ) ) , RR , < ) <_ C )
119	1, 118	syl5eqbr 4688	. . . . . . . . . . . . . 14 |- ( ph -> S <_ C )
120	44, 23	leloed 10180	. . . . . . . . . . . . . 14 |- ( ph -> ( S <_ C <-> ( S < C \/ S = C ) ) )
121	119, 120	mpbid 222	. . . . . . . . . . . . 13 |- ( ph -> ( S < C \/ S = C ) )
122	121	ord 392	. . . . . . . . . . . 12 |- ( ph -> ( -. S < C -> S = C ) )
123		elndif 3734	. . . . . . . . . . . . . . 15 |- ( C e. A -> -. C e. ( RR \ A ) )
124	8, 123	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> -. C e. ( RR \ A ) )
125		inss1 3833	. . . . . . . . . . . . . . . 16 |- ( V i^i A ) C_ V
126	125, 7	sseldi 3601	. . . . . . . . . . . . . . 15 |- ( ph -> C e. V )
127		elin 3796	. . . . . . . . . . . . . . . 16 |- ( C e. ( U i^i V ) <-> ( C e. U /\ C e. V ) )
128		reconnlem2.7	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( U i^i V ) C_ ( RR \ A ) )
129	128	sseld 3602	. . . . . . . . . . . . . . . 16 |- ( ph -> ( C e. ( U i^i V ) -> C e. ( RR \ A ) ) )
130	127, 129	syl5bir 233	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( C e. U /\ C e. V ) -> C e. ( RR \ A ) ) )
131	126, 130	mpan2d 710	. . . . . . . . . . . . . 14 |- ( ph -> ( C e. U -> C e. ( RR \ A ) ) )
132	124, 131	mtod 189	. . . . . . . . . . . . 13 |- ( ph -> -. C e. U )
133		eleq1 2689	. . . . . . . . . . . . . 14 |- ( S = C -> ( S e. U <-> C e. U ) )
134	133	notbid 308	. . . . . . . . . . . . 13 |- ( S = C -> ( -. S e. U <-> -. C e. U ) )
135	132, 134	syl5ibrcom 237	. . . . . . . . . . . 12 |- ( ph -> ( S = C -> -. S e. U ) )
136	122, 135	syld 47	. . . . . . . . . . 11 |- ( ph -> ( -. S < C -> -. S e. U ) )
137	136	con4d 114	. . . . . . . . . 10 |- ( ph -> ( S e. U -> S < C ) )
138	137	imp 445	. . . . . . . . 9 |- ( ( ph /\ S e. U ) -> S < C )
139		mnfxr 10096	. . . . . . . . . . 11 |- -oo e. RR*
140		elioo2 12216	. . . . . . . . . . 11 |- ( ( -oo e. RR* /\ C e. RR* ) -> ( S e. ( -oo (,) C ) <-> ( S e. RR /\ -oo < S /\ S < C ) ) )
141	139, 24, 140	sylancr 695	. . . . . . . . . 10 |- ( ph -> ( S e. ( -oo (,) C ) <-> ( S e. RR /\ -oo < S /\ S < C ) ) )
142	141	adantr 481	. . . . . . . . 9 |- ( ( ph /\ S e. U ) -> ( S e. ( -oo (,) C ) <-> ( S e. RR /\ -oo < S /\ S < C ) ) )
143	113, 115, 138, 142	mpbir3and 1245	. . . . . . . 8 |- ( ( ph /\ S e. U ) -> S e. ( -oo (,) C ) )
144	143	ex 450	. . . . . . 7 |- ( ph -> ( S e. U -> S e. ( -oo (,) C ) ) )
145	144	ancld 576	. . . . . 6 |- ( ph -> ( S e. U -> ( S e. U /\ S e. ( -oo (,) C ) ) ) )
146		elin 3796	. . . . . . 7 |- ( S e. ( U i^i ( -oo (,) C ) ) <-> ( S e. U /\ S e. ( -oo (,) C ) ) )
147		reconnlem2.2	. . . . . . . 8 |- ( ph -> U e. ( topGen ` ran (,) ) )
148		retop 22565	. . . . . . . . 9 |- ( topGen ` ran (,) ) e. Top
149		iooretop 22569	. . . . . . . . 9 |- ( -oo (,) C ) e. ( topGen ` ran (,) )
150		inopn 20704	. . . . . . . . 9 |- ( ( ( topGen ` ran (,) ) e. Top /\ U e. ( topGen ` ran (,) ) /\ ( -oo (,) C ) e. ( topGen ` ran (,) ) ) -> ( U i^i ( -oo (,) C ) ) e. ( topGen ` ran (,) ) )
151	148, 149, 150	mp3an13 1415	. . . . . . . 8 |- ( U e. ( topGen ` ran (,) ) -> ( U i^i ( -oo (,) C ) ) e. ( topGen ` ran (,) ) )
152		eqid 2622	. . . . . . . . . . . 12 |- ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
153	85, 152	tgioo 22599	. . . . . . . . . . 11 |- ( topGen ` ran (,) ) = ( MetOpen ` ( ( abs o. - ) |` ( RR X. RR ) ) )
154	153	mopni2 22298	. . . . . . . . . 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 ) ) )
155	102, 154	mp3an1 1411	. . . . . . . . 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 ) ) )
156	155	ex 450	. . . . . . . 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 ) ) ) )
157	147, 151, 156	3syl 18	. . . . . . 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 ) ) ) )
158	146, 157	syl5bir 233	. . . . . 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 ) ) ) )
159	145, 158	syld 47	. . . . 5 |- ( ph -> ( S e. U -> E. r e. RR+ ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ ( U i^i ( -oo (,) C ) ) ) )
160	112, 159	mtod 189	. . . 4 |- ( ph -> -. S e. U )
161		ltsubrp 11866	. . . . . . . . 9 |- ( ( S e. RR /\ r e. RR+ ) -> ( S - r ) < S )
162	44, 161	sylan 488	. . . . . . . 8 |- ( ( ph /\ r e. RR+ ) -> ( S - r ) < S )
163		rpre 11839	. . . . . . . . . 10 |- ( r e. RR+ -> r e. RR )
164		resubcl 10345	. . . . . . . . . 10 |- ( ( S e. RR /\ r e. RR ) -> ( S - r ) e. RR )
165	44, 163, 164	syl2an 494	. . . . . . . . 9 |- ( ( ph /\ r e. RR+ ) -> ( S - r ) e. RR )
166	165, 48	ltnled 10184	. . . . . . . 8 |- ( ( ph /\ r e. RR+ ) -> ( ( S - r ) < S <-> -. S <_ ( S - r ) ) )
167	162, 166	mpbid 222	. . . . . . 7 |- ( ( ph /\ r e. RR+ ) -> -. S <_ ( S - r ) )
168	85	bl2ioo 22595	. . . . . . . . . 10 |- ( ( S e. RR /\ r e. RR ) -> ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) = ( ( S - r ) (,) ( S + r ) ) )
169	44, 163, 168	syl2an 494	. . . . . . . . 9 |- ( ( ph /\ r e. RR+ ) -> ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) = ( ( S - r ) (,) ( S + r ) ) )
170	169	sseq1d 3632	. . . . . . . 8 |- ( ( ph /\ r e. RR+ ) -> ( ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ V <-> ( ( S - r ) (,) ( S + r ) ) C_ V ) )
171	15	ad2antrr 762	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) -> ( B [,] C ) C_ A )
172	2, 171	syl5ss 3614	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) -> ( U i^i ( B [,] C ) ) C_ A )
173	172	sselda 3603	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ w e. ( U i^i ( B [,] C ) ) ) -> w e. A )
174		elndif 3734	. . . . . . . . . . . . . . 15 |- ( w e. A -> -. w e. ( RR \ A ) )
175	173, 174	syl 17	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ w e. ( U i^i ( B [,] C ) ) ) -> -. w e. ( RR \ A ) )
176	128	ad3antrrr 766	. . . . . . . . . . . . . . . 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 ) )
177		inss1 3833	. . . . . . . . . . . . . . . . . 18 |- ( U i^i ( B [,] C ) ) C_ U
178		simprl 794	. . . . . . . . . . . . . . . . . 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 ) ) )
179	177, 178	sseldi 3601	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> w e. U )
180		simplr 792	. . . . . . . . . . . . . . . . . 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 )
181	18	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . 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 )
182		simpr 477	. . . . . . . . . . . . . . . . . . . . 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 ) ) )
183	181, 182	sseldd 3604	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ w e. ( U i^i ( B [,] C ) ) ) -> w e. RR )
184	183	adantrr 753	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> w e. RR )
185		simprr 796	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> ( S - r ) < w )
186	48	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> S e. RR )
187		simpllr 799	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> r e. RR+ )
188	187	rpred 11872	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> r e. RR )
189	186, 188	readdcld 10069	. . . . . . . . . . . . . . . . . . . 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 )
190	181	adantrr 753	. . . . . . . . . . . . . . . . . . . . . 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 )
191	30	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . 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 ) ) =/= (/) )
192	41	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . 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 )
193		suprub 10984	. . . . . . . . . . . . . . . . . . . . . 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 , < ) )
194	190, 191, 192, 178, 193	syl31anc 1329	. . . . . . . . . . . . . . . . . . . . 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 , < ) )
195	194, 1	syl6breqr 4695	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> w <_ S )
196	186, 187	ltaddrpd 11905	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> S < ( S + r ) )
197	184, 186, 189, 195, 196	lelttrd 10195	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> w < ( S + r ) )
198	165	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 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 )
199		rexr 10085	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( S - r ) e. RR -> ( S - r ) e. RR* )
200		rexr 10085	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( S + r ) e. RR -> ( S + r ) e. RR* )
201		elioo2 12216	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( S - r ) e. RR* /\ ( S + r ) e. RR* ) -> ( w e. ( ( S - r ) (,) ( S + r ) ) <-> ( w e. RR /\ ( S - r ) < w /\ w < ( S + r ) ) ) )
202	199, 200, 201	syl2an 494	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( S - r ) e. RR /\ ( S + r ) e. RR ) -> ( w e. ( ( S - r ) (,) ( S + r ) ) <-> ( w e. RR /\ ( S - r ) < w /\ w < ( S + r ) ) ) )
203	198, 189, 202	syl2anc 693	. . . . . . . . . . . . . . . . . . 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 ) ) ) )
204	184, 185, 197, 203	mpbir3and 1245	. . . . . . . . . . . . . . . . . 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 ) ) )
205	180, 204	sseldd 3604	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ ( w e. ( U i^i ( B [,] C ) ) /\ ( S - r ) < w ) ) -> w e. V )
206	179, 205	elind 3798	. . . . . . . . . . . . . . . 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 ) )
207	176, 206	sseldd 3604	. . . . . . . . . . . . . . 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 ) )
208	207	expr 643	. . . . . . . . . . . . . 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 ) ) )
209	175, 208	mtod 189	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ w e. ( U i^i ( B [,] C ) ) ) -> -. ( S - r ) < w )
210	165	ad2antrr 762	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ w e. ( U i^i ( B [,] C ) ) ) -> ( S - r ) e. RR )
211	183, 210	lenltd 10183	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ w e. ( U i^i ( B [,] C ) ) ) -> ( w <_ ( S - r ) <-> -. ( S - r ) < w ) )
212	209, 211	mpbird 247	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) /\ w e. ( U i^i ( B [,] C ) ) ) -> w <_ ( S - r ) )
213	212	ralrimiva 2966	. . . . . . . . . . 11 |- ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) -> A. w e. ( U i^i ( B [,] C ) ) w <_ ( S - r ) )
214	18	ad2antrr 762	. . . . . . . . . . . 12 |- ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) -> ( U i^i ( B [,] C ) ) C_ RR )
215	30	ad2antrr 762	. . . . . . . . . . . 12 |- ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) -> ( U i^i ( B [,] C ) ) =/= (/) )
216	41	ad2antrr 762	. . . . . . . . . . . 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 )
217	165	adantr 481	. . . . . . . . . . . 12 |- ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) -> ( S - r ) e. RR )
218		suprleub 10989	. . . . . . . . . . . 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 ) ) )
219	214, 215, 216, 217, 218	syl31anc 1329	. . . . . . . . . . 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 ) ) )
220	213, 219	mpbird 247	. . . . . . . . . 10 |- ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) -> sup ( ( U i^i ( B [,] C ) ) , RR , < ) <_ ( S - r ) )
221	1, 220	syl5eqbr 4688	. . . . . . . . 9 |- ( ( ( ph /\ r e. RR+ ) /\ ( ( S - r ) (,) ( S + r ) ) C_ V ) -> S <_ ( S - r ) )
222	221	ex 450	. . . . . . . 8 |- ( ( ph /\ r e. RR+ ) -> ( ( ( S - r ) (,) ( S + r ) ) C_ V -> S <_ ( S - r ) ) )
223	170, 222	sylbid 230	. . . . . . 7 |- ( ( ph /\ r e. RR+ ) -> ( ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ V -> S <_ ( S - r ) ) )
224	167, 223	mtod 189	. . . . . 6 |- ( ( ph /\ r e. RR+ ) -> -. ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ V )
225	224	nrexdv 3001	. . . . 5 |- ( ph -> -. E. r e. RR+ ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ V )
226		reconnlem2.3	. . . . . 6 |- ( ph -> V e. ( topGen ` ran (,) ) )
227	153	mopni2 22298	. . . . . . . 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 )
228	102, 227	mp3an1 1411	. . . . . . 7 |- ( ( V e. ( topGen ` ran (,) ) /\ S e. V ) -> E. r e. RR+ ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ V )
229	228	ex 450	. . . . . 6 |- ( V e. ( topGen ` ran (,) ) -> ( S e. V -> E. r e. RR+ ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ V ) )
230	226, 229	syl 17	. . . . 5 |- ( ph -> ( S e. V -> E. r e. RR+ ( S ( ball ` ( ( abs o. - ) |` ( RR X. RR ) ) ) r ) C_ V ) )
231	225, 230	mtod 189	. . . 4 |- ( ph -> -. S e. V )
232		ioran 511	. . . 4 |- ( -. ( S e. U \/ S e. V ) <-> ( -. S e. U /\ -. S e. V ) )
233	160, 231, 232	sylanbrc 698	. . 3 |- ( ph -> -. ( S e. U \/ S e. V ) )
234		elun 3753	. . 3 |- ( S e. ( U u. V ) <-> ( S e. U \/ S e. V ) )
235	233, 234	sylnibr 319	. 2 |- ( ph -> -. S e. ( U u. V ) )
236		elicc2 12238	. . . . . 6 |- ( ( B e. RR /\ C e. RR ) -> ( S e. ( B [,] C ) <-> ( S e. RR /\ B <_ S /\ S <_ C ) ) )
237	21, 23, 236	syl2anc 693	. . . . 5 |- ( ph -> ( S e. ( B [,] C ) <-> ( S e. RR /\ B <_ S /\ S <_ C ) ) )
238	44, 65, 119, 237	mpbir3and 1245	. . . 4 |- ( ph -> S e. ( B [,] C ) )
239	15, 238	sseldd 3604	. . 3 |- ( ph -> S e. A )
240		ssel 3597	. . 3 |- ( A C_ ( U u. V ) -> ( S e. A -> S e. ( U u. V ) ) )
241	239, 240	syl5com 31	. 2 |- ( ph -> ( A C_ ( U u. V ) -> S e. ( U u. V ) ) )
242	235, 241	mtod 189	1 |- ( ph -> -. A C_ ( U u. V ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   \ cdif 3571   u. cun 3572   i^i cin 3573   C_ wss 3574   (/)c0 3915   class class class wbr 4653   X. cxp 5112   ran crn 5115   |` cres 5116   o. ccom 5118   ` cfv 5888  (class class class)co 6650   supcsup 8346   RRcr 9935   + caddc 9939   -oocmnf 10072   RR*cxr 10073   < clt 10074   <_ cle 10075   - cmin 10266   / cdiv 10684   2c2 11070   RR+crp 11832   (,)cioo 12175   [,]cicc 12178   abscabs 13974   topGenctg 16098   *Metcxmt 19731   ballcbl 19733   MetOpencmopn 19736   Topctop 20698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-sup 8348  df-inf 8349  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-n0 11293  df-z 11378  df-uz 11688  df-q 11789  df-rp 11833  df-xneg 11946  df-xadd 11947  df-xmul 11948  df-ioo 12179  df-icc 12182  df-seq 12802  df-exp 12861  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-topgen 16104  df-psmet 19738  df-xmet 19739  df-met 19740  df-bl 19741  df-mopn 19742  df-top 20699  df-topon 20716  df-bases 20750

This theorem is referenced by:  reconn  22631