Metamath Proof Explorer

Theorem icccmplem3

Description: Lemma for icccmp . (Contributed by Mario Carneiro, 13-Jun-2014)

Ref Expression
Hypotheses icccmp.1 
|- J = ( topGen ` ran (,) )
icccmp.2 
|- T = ( J |`t ( A [,] B ) )
icccmp.3 
|- D = ( ( abs o. - ) |` ( RR X. RR ) )
icccmp.4 
|- S = { x e. ( A [,] B ) | E. z e. ( ~P U i^i Fin ) ( A [,] x ) C_ U. z }
icccmp.5 
|- ( ph -> A e. RR )
icccmp.6 
|- ( ph -> B e. RR )
icccmp.7 
|- ( ph -> A <_ B )
icccmp.8 
|- ( ph -> U C_ J )
icccmp.9 
|- ( ph -> ( A [,] B ) C_ U. U )
Assertion icccmplem3 
|- ( ph -> B e. S )

Proof

Step Hyp Ref Expression
1 icccmp.1 
 |-  J = ( topGen ` ran (,) )
2 icccmp.2 
 |-  T = ( J |`t ( A [,] B ) )
3 icccmp.3 
 |-  D = ( ( abs o. - ) |` ( RR X. RR ) )
4 icccmp.4 
 |-  S = { x e. ( A [,] B ) | E. z e. ( ~P U i^i Fin ) ( A [,] x ) C_ U. z }
5 icccmp.5 
 |-  ( ph -> A e. RR )
6 icccmp.6 
 |-  ( ph -> B e. RR )
7 icccmp.7 
 |-  ( ph -> A <_ B )
8 icccmp.8 
 |-  ( ph -> U C_ J )
9 icccmp.9 
 |-  ( ph -> ( A [,] B ) C_ U. U )
10 4 ssrab3 
 |-  S C_ ( A [,] B )
11 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
12 5 6 11 syl2anc 
 |-  ( ph -> ( A [,] B ) C_ RR )
13 10 12 sstrid 
 |-  ( ph -> S C_ RR )
14 1 2 3 4 5 6 7 8 9 icccmplem1 
 |-  ( ph -> ( A e. S /\ A. y e. S y <_ B ) )
15 14 simpld 
 |-  ( ph -> A e. S )
16 15 ne0d 
 |-  ( ph -> S =/= (/) )
17 14 simprd 
 |-  ( ph -> A. y e. S y <_ B )
18 brralrspcev 
 |-  ( ( B e. RR /\ A. y e. S y <_ B ) -> E. v e. RR A. y e. S y <_ v )
19 6 17 18 syl2anc 
 |-  ( ph -> E. v e. RR A. y e. S y <_ v )
20 13 16 19 suprcld 
 |-  ( ph -> sup ( S , RR , < ) e. RR )
21 13 16 19 15 suprubd 
 |-  ( ph -> A <_ sup ( S , RR , < ) )
22 suprleub 
 |-  ( ( ( S C_ RR /\ S =/= (/) /\ E. v e. RR A. y e. S y <_ v ) /\ B e. RR ) -> ( sup ( S , RR , < ) <_ B <-> A. y e. S y <_ B ) )
23 13 16 19 6 22 syl31anc 
 |-  ( ph -> ( sup ( S , RR , < ) <_ B <-> A. y e. S y <_ B ) )
24 17 23 mpbird 
 |-  ( ph -> sup ( S , RR , < ) <_ B )
25 elicc2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( sup ( S , RR , < ) e. ( A [,] B ) <-> ( sup ( S , RR , < ) e. RR /\ A <_ sup ( S , RR , < ) /\ sup ( S , RR , < ) <_ B ) ) )
26 5 6 25 syl2anc 
 |-  ( ph -> ( sup ( S , RR , < ) e. ( A [,] B ) <-> ( sup ( S , RR , < ) e. RR /\ A <_ sup ( S , RR , < ) /\ sup ( S , RR , < ) <_ B ) ) )
27 20 21 24 26 mpbir3and 
 |-  ( ph -> sup ( S , RR , < ) e. ( A [,] B ) )
28 9 27 sseldd 
 |-  ( ph -> sup ( S , RR , < ) e. U. U )
29 eluni2 
 |-  ( sup ( S , RR , < ) e. U. U <-> E. u e. U sup ( S , RR , < ) e. u )
30 28 29 sylib 
 |-  ( ph -> E. u e. U sup ( S , RR , < ) e. u )
31 8 sselda 
 |-  ( ( ph /\ u e. U ) -> u e. J )
32 3 rexmet 
 |-  D e. ( *Met ` RR )
33 eqid 
 |-  ( MetOpen ` D ) = ( MetOpen ` D )
34 3 33 tgioo 
 |-  ( topGen ` ran (,) ) = ( MetOpen ` D )
35 1 34 eqtri 
 |-  J = ( MetOpen ` D )
36 35 mopni2 
 |-  ( ( D e. ( *Met ` RR ) /\ u e. J /\ sup ( S , RR , < ) e. u ) -> E. w e. RR+ ( sup ( S , RR , < ) ( ball ` D ) w ) C_ u )
37 32 36 mp3an1 
 |-  ( ( u e. J /\ sup ( S , RR , < ) e. u ) -> E. w e. RR+ ( sup ( S , RR , < ) ( ball ` D ) w ) C_ u )
38 37 ex 
 |-  ( u e. J -> ( sup ( S , RR , < ) e. u -> E. w e. RR+ ( sup ( S , RR , < ) ( ball ` D ) w ) C_ u ) )
39 31 38 syl 
 |-  ( ( ph /\ u e. U ) -> ( sup ( S , RR , < ) e. u -> E. w e. RR+ ( sup ( S , RR , < ) ( ball ` D ) w ) C_ u ) )
40 5 ad2antrr 
 |-  ( ( ( ph /\ u e. U ) /\ ( w e. RR+ /\ ( sup ( S , RR , < ) ( ball ` D ) w ) C_ u ) ) -> A e. RR )
41 6 ad2antrr 
 |-  ( ( ( ph /\ u e. U ) /\ ( w e. RR+ /\ ( sup ( S , RR , < ) ( ball ` D ) w ) C_ u ) ) -> B e. RR )
42 7 ad2antrr 
 |-  ( ( ( ph /\ u e. U ) /\ ( w e. RR+ /\ ( sup ( S , RR , < ) ( ball ` D ) w ) C_ u ) ) -> A <_ B )
43 8 ad2antrr 
 |-  ( ( ( ph /\ u e. U ) /\ ( w e. RR+ /\ ( sup ( S , RR , < ) ( ball ` D ) w ) C_ u ) ) -> U C_ J )
44 9 ad2antrr 
 |-  ( ( ( ph /\ u e. U ) /\ ( w e. RR+ /\ ( sup ( S , RR , < ) ( ball ` D ) w ) C_ u ) ) -> ( A [,] B ) C_ U. U )
45 simplr 
 |-  ( ( ( ph /\ u e. U ) /\ ( w e. RR+ /\ ( sup ( S , RR , < ) ( ball ` D ) w ) C_ u ) ) -> u e. U )
46 simprl 
 |-  ( ( ( ph /\ u e. U ) /\ ( w e. RR+ /\ ( sup ( S , RR , < ) ( ball ` D ) w ) C_ u ) ) -> w e. RR+ )
47 simprr 
 |-  ( ( ( ph /\ u e. U ) /\ ( w e. RR+ /\ ( sup ( S , RR , < ) ( ball ` D ) w ) C_ u ) ) -> ( sup ( S , RR , < ) ( ball ` D ) w ) C_ u )
48 eqid 
 |-  sup ( S , RR , < ) = sup ( S , RR , < )
49 eqid 
 |-  if ( ( sup ( S , RR , < ) + ( w / 2 ) ) <_ B , ( sup ( S , RR , < ) + ( w / 2 ) ) , B ) = if ( ( sup ( S , RR , < ) + ( w / 2 ) ) <_ B , ( sup ( S , RR , < ) + ( w / 2 ) ) , B )
50 1 2 3 4 40 41 42 43 44 45 46 47 48 49 icccmplem2 
 |-  ( ( ( ph /\ u e. U ) /\ ( w e. RR+ /\ ( sup ( S , RR , < ) ( ball ` D ) w ) C_ u ) ) -> B e. S )
51 50 rexlimdvaa 
 |-  ( ( ph /\ u e. U ) -> ( E. w e. RR+ ( sup ( S , RR , < ) ( ball ` D ) w ) C_ u -> B e. S ) )
52 39 51 syld 
 |-  ( ( ph /\ u e. U ) -> ( sup ( S , RR , < ) e. u -> B e. S ) )
53 52 rexlimdva 
 |-  ( ph -> ( E. u e. U sup ( S , RR , < ) e. u -> B e. S ) )
54 30 53 mpd 
 |-  ( ph -> B e. S )