Metamath Proof Explorer

Theorem metss

Description: Two ways of saying that metric D generates a finer topology than metric C . (Contributed by Mario Carneiro, 12-Nov-2013) (Revised by Mario Carneiro, 24-Aug-2015)

Ref Expression
Hypotheses metequiv.3 
|- J = ( MetOpen ` C )
metequiv.4 
|- K = ( MetOpen ` D )
Assertion metss 
|- ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) -> ( J C_ K <-> A. x e. X A. r e. RR+ E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) ) )

Proof

Step Hyp Ref Expression
1 metequiv.3 
 |-  J = ( MetOpen ` C )
2 metequiv.4 
 |-  K = ( MetOpen ` D )
3 1 mopnval 
 |-  ( C e. ( *Met ` X ) -> J = ( topGen ` ran ( ball ` C ) ) )
4 3 adantr 
 |-  ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) -> J = ( topGen ` ran ( ball ` C ) ) )
5 2 mopnval 
 |-  ( D e. ( *Met ` X ) -> K = ( topGen ` ran ( ball ` D ) ) )
6 5 adantl 
 |-  ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) -> K = ( topGen ` ran ( ball ` D ) ) )
7 4 6 sseq12d 
 |-  ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) -> ( J C_ K <-> ( topGen ` ran ( ball ` C ) ) C_ ( topGen ` ran ( ball ` D ) ) ) )
8 blbas 
 |-  ( C e. ( *Met ` X ) -> ran ( ball ` C ) e. TopBases )
9 unirnbl 
 |-  ( C e. ( *Met ` X ) -> U. ran ( ball ` C ) = X )
10 9 adantr 
 |-  ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) -> U. ran ( ball ` C ) = X )
11 unirnbl 
 |-  ( D e. ( *Met ` X ) -> U. ran ( ball ` D ) = X )
12 11 adantl 
 |-  ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) -> U. ran ( ball ` D ) = X )
13 10 12 eqtr4d 
 |-  ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) -> U. ran ( ball ` C ) = U. ran ( ball ` D ) )
14 tgss2 
 |-  ( ( ran ( ball ` C ) e. TopBases /\ U. ran ( ball ` C ) = U. ran ( ball ` D ) ) -> ( ( topGen ` ran ( ball ` C ) ) C_ ( topGen ` ran ( ball ` D ) ) <-> A. x e. U. ran ( ball ` C ) A. y e. ran ( ball ` C ) ( x e. y -> E. z e. ran ( ball ` D ) ( x e. z /\ z C_ y ) ) ) )
15 8 13 14 syl2an2r 
 |-  ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) -> ( ( topGen ` ran ( ball ` C ) ) C_ ( topGen ` ran ( ball ` D ) ) <-> A. x e. U. ran ( ball ` C ) A. y e. ran ( ball ` C ) ( x e. y -> E. z e. ran ( ball ` D ) ( x e. z /\ z C_ y ) ) ) )
16 10 raleqdv 
 |-  ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) -> ( A. x e. U. ran ( ball ` C ) A. y e. ran ( ball ` C ) ( x e. y -> E. z e. ran ( ball ` D ) ( x e. z /\ z C_ y ) ) <-> A. x e. X A. y e. ran ( ball ` C ) ( x e. y -> E. z e. ran ( ball ` D ) ( x e. z /\ z C_ y ) ) ) )
17 blssex 
 |-  ( ( D e. ( *Met ` X ) /\ x e. X ) -> ( E. z e. ran ( ball ` D ) ( x e. z /\ z C_ y ) <-> E. s e. RR+ ( x ( ball ` D ) s ) C_ y ) )
18 17 adantll 
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) /\ x e. X ) -> ( E. z e. ran ( ball ` D ) ( x e. z /\ z C_ y ) <-> E. s e. RR+ ( x ( ball ` D ) s ) C_ y ) )
19 18 imbi2d 
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) /\ x e. X ) -> ( ( x e. y -> E. z e. ran ( ball ` D ) ( x e. z /\ z C_ y ) ) <-> ( x e. y -> E. s e. RR+ ( x ( ball ` D ) s ) C_ y ) ) )
20 19 ralbidv 
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) /\ x e. X ) -> ( A. y e. ran ( ball ` C ) ( x e. y -> E. z e. ran ( ball ` D ) ( x e. z /\ z C_ y ) ) <-> A. y e. ran ( ball ` C ) ( x e. y -> E. s e. RR+ ( x ( ball ` D ) s ) C_ y ) ) )
21 rpxr 
 |-  ( r e. RR+ -> r e. RR* )
22 blelrn 
 |-  ( ( C e. ( *Met ` X ) /\ x e. X /\ r e. RR* ) -> ( x ( ball ` C ) r ) e. ran ( ball ` C ) )
23 21 22 syl3an3 
 |-  ( ( C e. ( *Met ` X ) /\ x e. X /\ r e. RR+ ) -> ( x ( ball ` C ) r ) e. ran ( ball ` C ) )
24 blcntr 
 |-  ( ( C e. ( *Met ` X ) /\ x e. X /\ r e. RR+ ) -> x e. ( x ( ball ` C ) r ) )
25 eleq2 
 |-  ( y = ( x ( ball ` C ) r ) -> ( x e. y <-> x e. ( x ( ball ` C ) r ) ) )
26 sseq2 
 |-  ( y = ( x ( ball ` C ) r ) -> ( ( x ( ball ` D ) s ) C_ y <-> ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) ) )
27 26 rexbidv 
 |-  ( y = ( x ( ball ` C ) r ) -> ( E. s e. RR+ ( x ( ball ` D ) s ) C_ y <-> E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) ) )
28 25 27 imbi12d 
 |-  ( y = ( x ( ball ` C ) r ) -> ( ( x e. y -> E. s e. RR+ ( x ( ball ` D ) s ) C_ y ) <-> ( x e. ( x ( ball ` C ) r ) -> E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) ) ) )
29 28 rspcv 
 |-  ( ( x ( ball ` C ) r ) e. ran ( ball ` C ) -> ( A. y e. ran ( ball ` C ) ( x e. y -> E. s e. RR+ ( x ( ball ` D ) s ) C_ y ) -> ( x e. ( x ( ball ` C ) r ) -> E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) ) ) )
30 29 com23 
 |-  ( ( x ( ball ` C ) r ) e. ran ( ball ` C ) -> ( x e. ( x ( ball ` C ) r ) -> ( A. y e. ran ( ball ` C ) ( x e. y -> E. s e. RR+ ( x ( ball ` D ) s ) C_ y ) -> E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) ) ) )
31 23 24 30 sylc 
 |-  ( ( C e. ( *Met ` X ) /\ x e. X /\ r e. RR+ ) -> ( A. y e. ran ( ball ` C ) ( x e. y -> E. s e. RR+ ( x ( ball ` D ) s ) C_ y ) -> E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) ) )
32 31 ad4ant134 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) /\ x e. X ) /\ r e. RR+ ) -> ( A. y e. ran ( ball ` C ) ( x e. y -> E. s e. RR+ ( x ( ball ` D ) s ) C_ y ) -> E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) ) )
33 32 ralrimdva 
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) /\ x e. X ) -> ( A. y e. ran ( ball ` C ) ( x e. y -> E. s e. RR+ ( x ( ball ` D ) s ) C_ y ) -> A. r e. RR+ E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) ) )
34 blss 
 |-  ( ( C e. ( *Met ` X ) /\ y e. ran ( ball ` C ) /\ x e. y ) -> E. r e. RR+ ( x ( ball ` C ) r ) C_ y )
35 34 3expb 
 |-  ( ( C e. ( *Met ` X ) /\ ( y e. ran ( ball ` C ) /\ x e. y ) ) -> E. r e. RR+ ( x ( ball ` C ) r ) C_ y )
36 35 ad4ant14 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) /\ x e. X ) /\ ( y e. ran ( ball ` C ) /\ x e. y ) ) -> E. r e. RR+ ( x ( ball ` C ) r ) C_ y )
37 r19.29 
 |-  ( ( A. r e. RR+ E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) /\ E. r e. RR+ ( x ( ball ` C ) r ) C_ y ) -> E. r e. RR+ ( E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) /\ ( x ( ball ` C ) r ) C_ y ) )
38 sstr 
 |-  ( ( ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) /\ ( x ( ball ` C ) r ) C_ y ) -> ( x ( ball ` D ) s ) C_ y )
39 38 expcom 
 |-  ( ( x ( ball ` C ) r ) C_ y -> ( ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) -> ( x ( ball ` D ) s ) C_ y ) )
40 39 reximdv 
 |-  ( ( x ( ball ` C ) r ) C_ y -> ( E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) -> E. s e. RR+ ( x ( ball ` D ) s ) C_ y ) )
41 40 impcom 
 |-  ( ( E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) /\ ( x ( ball ` C ) r ) C_ y ) -> E. s e. RR+ ( x ( ball ` D ) s ) C_ y )
42 41 rexlimivw 
 |-  ( E. r e. RR+ ( E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) /\ ( x ( ball ` C ) r ) C_ y ) -> E. s e. RR+ ( x ( ball ` D ) s ) C_ y )
43 37 42 syl 
 |-  ( ( A. r e. RR+ E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) /\ E. r e. RR+ ( x ( ball ` C ) r ) C_ y ) -> E. s e. RR+ ( x ( ball ` D ) s ) C_ y )
44 43 ex 
 |-  ( A. r e. RR+ E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) -> ( E. r e. RR+ ( x ( ball ` C ) r ) C_ y -> E. s e. RR+ ( x ( ball ` D ) s ) C_ y ) )
45 36 44 syl5com 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) /\ x e. X ) /\ ( y e. ran ( ball ` C ) /\ x e. y ) ) -> ( A. r e. RR+ E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) -> E. s e. RR+ ( x ( ball ` D ) s ) C_ y ) )
46 45 expr 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) /\ x e. X ) /\ y e. ran ( ball ` C ) ) -> ( x e. y -> ( A. r e. RR+ E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) -> E. s e. RR+ ( x ( ball ` D ) s ) C_ y ) ) )
47 46 com23 
 |-  ( ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) /\ x e. X ) /\ y e. ran ( ball ` C ) ) -> ( A. r e. RR+ E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) -> ( x e. y -> E. s e. RR+ ( x ( ball ` D ) s ) C_ y ) ) )
48 47 ralrimdva 
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) /\ x e. X ) -> ( A. r e. RR+ E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) -> A. y e. ran ( ball ` C ) ( x e. y -> E. s e. RR+ ( x ( ball ` D ) s ) C_ y ) ) )
49 33 48 impbid 
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) /\ x e. X ) -> ( A. y e. ran ( ball ` C ) ( x e. y -> E. s e. RR+ ( x ( ball ` D ) s ) C_ y ) <-> A. r e. RR+ E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) ) )
50 20 49 bitrd 
 |-  ( ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) /\ x e. X ) -> ( A. y e. ran ( ball ` C ) ( x e. y -> E. z e. ran ( ball ` D ) ( x e. z /\ z C_ y ) ) <-> A. r e. RR+ E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) ) )
51 50 ralbidva 
 |-  ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) -> ( A. x e. X A. y e. ran ( ball ` C ) ( x e. y -> E. z e. ran ( ball ` D ) ( x e. z /\ z C_ y ) ) <-> A. x e. X A. r e. RR+ E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) ) )
52 16 51 bitrd 
 |-  ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) -> ( A. x e. U. ran ( ball ` C ) A. y e. ran ( ball ` C ) ( x e. y -> E. z e. ran ( ball ` D ) ( x e. z /\ z C_ y ) ) <-> A. x e. X A. r e. RR+ E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) ) )
53 7 15 52 3bitrd 
 |-  ( ( C e. ( *Met ` X ) /\ D e. ( *Met ` X ) ) -> ( J C_ K <-> A. x e. X A. r e. RR+ E. s e. RR+ ( x ( ball ` D ) s ) C_ ( x ( ball ` C ) r ) ) )