Metamath Proof Explorer

Theorem metnrmlem2

Description: Lemma for metnrm . (Contributed by Mario Carneiro, 14-Jan-2014) (Revised by Mario Carneiro, 5-Sep-2015)

Ref Expression
Hypotheses metdscn.f 
|- F = ( x e. X |-> inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) )
metdscn.j 
|- J = ( MetOpen ` D )
metnrmlem.1 
|- ( ph -> D e. ( *Met ` X ) )
metnrmlem.2 
|- ( ph -> S e. ( Clsd ` J ) )
metnrmlem.3 
|- ( ph -> T e. ( Clsd ` J ) )
metnrmlem.4 
|- ( ph -> ( S i^i T ) = (/) )
metnrmlem.u 
|- U = U_ t e. T ( t ( ball ` D ) ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) )
Assertion metnrmlem2 
|- ( ph -> ( U e. J /\ T C_ U ) )

Proof

Step Hyp Ref Expression
1 metdscn.f 
 |-  F = ( x e. X |-> inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) )
2 metdscn.j 
 |-  J = ( MetOpen ` D )
3 metnrmlem.1 
 |-  ( ph -> D e. ( *Met ` X ) )
4 metnrmlem.2 
 |-  ( ph -> S e. ( Clsd ` J ) )
5 metnrmlem.3 
 |-  ( ph -> T e. ( Clsd ` J ) )
6 metnrmlem.4 
 |-  ( ph -> ( S i^i T ) = (/) )
7 metnrmlem.u 
 |-  U = U_ t e. T ( t ( ball ` D ) ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) )
8 2 mopntop 
 |-  ( D e. ( *Met ` X ) -> J e. Top )
9 3 8 syl 
 |-  ( ph -> J e. Top )
10 3 adantr 
 |-  ( ( ph /\ t e. T ) -> D e. ( *Met ` X ) )
11 eqid 
 |-  U. J = U. J
12 11 cldss 
 |-  ( T e. ( Clsd ` J ) -> T C_ U. J )
13 5 12 syl 
 |-  ( ph -> T C_ U. J )
14 2 mopnuni 
 |-  ( D e. ( *Met ` X ) -> X = U. J )
15 3 14 syl 
 |-  ( ph -> X = U. J )
16 13 15 sseqtrrd 
 |-  ( ph -> T C_ X )
17 16 sselda 
 |-  ( ( ph /\ t e. T ) -> t e. X )
18 1 2 3 4 5 6 metnrmlem1a 
 |-  ( ( ph /\ t e. T ) -> ( 0 < ( F ` t ) /\ if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) e. RR+ ) )
19 18 simprd 
 |-  ( ( ph /\ t e. T ) -> if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) e. RR+ )
20 19 rphalfcld 
 |-  ( ( ph /\ t e. T ) -> ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) e. RR+ )
21 20 rpxrd 
 |-  ( ( ph /\ t e. T ) -> ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) e. RR* )
22 2 blopn 
 |-  ( ( D e. ( *Met ` X ) /\ t e. X /\ ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) e. RR* ) -> ( t ( ball ` D ) ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) ) e. J )
23 10 17 21 22 syl3anc 
 |-  ( ( ph /\ t e. T ) -> ( t ( ball ` D ) ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) ) e. J )
24 23 ralrimiva 
 |-  ( ph -> A. t e. T ( t ( ball ` D ) ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) ) e. J )
25 iunopn 
 |-  ( ( J e. Top /\ A. t e. T ( t ( ball ` D ) ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) ) e. J ) -> U_ t e. T ( t ( ball ` D ) ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) ) e. J )
26 9 24 25 syl2anc 
 |-  ( ph -> U_ t e. T ( t ( ball ` D ) ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) ) e. J )
27 7 26 eqeltrid 
 |-  ( ph -> U e. J )
28 blcntr 
 |-  ( ( D e. ( *Met ` X ) /\ t e. X /\ ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) e. RR+ ) -> t e. ( t ( ball ` D ) ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) ) )
29 10 17 20 28 syl3anc 
 |-  ( ( ph /\ t e. T ) -> t e. ( t ( ball ` D ) ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) ) )
30 29 snssd 
 |-  ( ( ph /\ t e. T ) -> { t } C_ ( t ( ball ` D ) ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) ) )
31 30 ralrimiva 
 |-  ( ph -> A. t e. T { t } C_ ( t ( ball ` D ) ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) ) )
32 ss2iun 
 |-  ( A. t e. T { t } C_ ( t ( ball ` D ) ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) ) -> U_ t e. T { t } C_ U_ t e. T ( t ( ball ` D ) ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) ) )
33 31 32 syl 
 |-  ( ph -> U_ t e. T { t } C_ U_ t e. T ( t ( ball ` D ) ( if ( 1 <_ ( F ` t ) , 1 , ( F ` t ) ) / 2 ) ) )
34 iunid 
 |-  U_ t e. T { t } = T
35 34 eqcomi 
 |-  T = U_ t e. T { t }
36 33 35 7 3sstr4g 
 |-  ( ph -> T C_ U )
37 27 36 jca 
 |-  ( ph -> ( U e. J /\ T C_ U ) )