Metamath Proof Explorer

Theorem xlebnum

Description: Generalize lebnum to extended metrics. (Contributed by Mario Carneiro, 5-Sep-2015)

Ref Expression
Hypotheses xlebnum.j 
|- J = ( MetOpen ` D )
xlebnum.d 
|- ( ph -> D e. ( *Met ` X ) )
xlebnum.c 
|- ( ph -> J e. Comp )
xlebnum.s 
|- ( ph -> U C_ J )
xlebnum.u 
|- ( ph -> X = U. U )
Assertion xlebnum 
|- ( ph -> E. d e. RR+ A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u )

Proof

Step Hyp Ref Expression
1 xlebnum.j 
 |-  J = ( MetOpen ` D )
2 xlebnum.d 
 |-  ( ph -> D e. ( *Met ` X ) )
3 xlebnum.c 
 |-  ( ph -> J e. Comp )
4 xlebnum.s 
 |-  ( ph -> U C_ J )
5 xlebnum.u 
 |-  ( ph -> X = U. U )
6 eqid 
 |-  ( MetOpen ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) = ( MetOpen ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) )
7 1rp 
 |-  1 e. RR+
8 eqid 
 |-  ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) = ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) )
9 8 stdbdmet 
 |-  ( ( D e. ( *Met ` X ) /\ 1 e. RR+ ) -> ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) e. ( Met ` X ) )
10 2 7 9 sylancl 
 |-  ( ph -> ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) e. ( Met ` X ) )
11 rpxr 
 |-  ( 1 e. RR+ -> 1 e. RR* )
12 7 11 mp1i 
 |-  ( ph -> 1 e. RR* )
13 0lt1 
 |-  0 < 1
14 13 a1i 
 |-  ( ph -> 0 < 1 )
15 8 1 stdbdmopn 
 |-  ( ( D e. ( *Met ` X ) /\ 1 e. RR* /\ 0 < 1 ) -> J = ( MetOpen ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) )
16 2 12 14 15 syl3anc 
 |-  ( ph -> J = ( MetOpen ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) )
17 16 3 eqeltrrd 
 |-  ( ph -> ( MetOpen ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) e. Comp )
18 4 16 sseqtrd 
 |-  ( ph -> U C_ ( MetOpen ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) )
19 6 10 17 18 5 lebnum 
 |-  ( ph -> E. r e. RR+ A. x e. X E. u e. U ( x ( ball ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) r ) C_ u )
20 simpr 
 |-  ( ( ph /\ r e. RR+ ) -> r e. RR+ )
21 ifcl 
 |-  ( ( r e. RR+ /\ 1 e. RR+ ) -> if ( r <_ 1 , r , 1 ) e. RR+ )
22 20 7 21 sylancl 
 |-  ( ( ph /\ r e. RR+ ) -> if ( r <_ 1 , r , 1 ) e. RR+ )
23 2 ad2antrr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ x e. X ) -> D e. ( *Met ` X ) )
24 7 11 mp1i 
 |-  ( ( ( ph /\ r e. RR+ ) /\ x e. X ) -> 1 e. RR* )
25 13 a1i 
 |-  ( ( ( ph /\ r e. RR+ ) /\ x e. X ) -> 0 < 1 )
26 simpr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ x e. X ) -> x e. X )
27 22 adantr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ x e. X ) -> if ( r <_ 1 , r , 1 ) e. RR+ )
28 rpxr 
 |-  ( if ( r <_ 1 , r , 1 ) e. RR+ -> if ( r <_ 1 , r , 1 ) e. RR* )
29 27 28 syl 
 |-  ( ( ( ph /\ r e. RR+ ) /\ x e. X ) -> if ( r <_ 1 , r , 1 ) e. RR* )
30 rpre 
 |-  ( r e. RR+ -> r e. RR )
31 30 ad2antlr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ x e. X ) -> r e. RR )
32 1re 
 |-  1 e. RR
33 min2 
 |-  ( ( r e. RR /\ 1 e. RR ) -> if ( r <_ 1 , r , 1 ) <_ 1 )
34 31 32 33 sylancl 
 |-  ( ( ( ph /\ r e. RR+ ) /\ x e. X ) -> if ( r <_ 1 , r , 1 ) <_ 1 )
35 8 stdbdbl 
 |-  ( ( ( D e. ( *Met ` X ) /\ 1 e. RR* /\ 0 < 1 ) /\ ( x e. X /\ if ( r <_ 1 , r , 1 ) e. RR* /\ if ( r <_ 1 , r , 1 ) <_ 1 ) ) -> ( x ( ball ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) if ( r <_ 1 , r , 1 ) ) = ( x ( ball ` D ) if ( r <_ 1 , r , 1 ) ) )
36 23 24 25 26 29 34 35 syl33anc 
 |-  ( ( ( ph /\ r e. RR+ ) /\ x e. X ) -> ( x ( ball ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) if ( r <_ 1 , r , 1 ) ) = ( x ( ball ` D ) if ( r <_ 1 , r , 1 ) ) )
37 10 ad2antrr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ x e. X ) -> ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) e. ( Met ` X ) )
38 metxmet 
 |-  ( ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) e. ( Met ` X ) -> ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) e. ( *Met ` X ) )
39 37 38 syl 
 |-  ( ( ( ph /\ r e. RR+ ) /\ x e. X ) -> ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) e. ( *Met ` X ) )
40 rpxr 
 |-  ( r e. RR+ -> r e. RR* )
41 40 ad2antlr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ x e. X ) -> r e. RR* )
42 min1 
 |-  ( ( r e. RR /\ 1 e. RR ) -> if ( r <_ 1 , r , 1 ) <_ r )
43 31 32 42 sylancl 
 |-  ( ( ( ph /\ r e. RR+ ) /\ x e. X ) -> if ( r <_ 1 , r , 1 ) <_ r )
44 ssbl 
 |-  ( ( ( ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) e. ( *Met ` X ) /\ x e. X ) /\ ( if ( r <_ 1 , r , 1 ) e. RR* /\ r e. RR* ) /\ if ( r <_ 1 , r , 1 ) <_ r ) -> ( x ( ball ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) if ( r <_ 1 , r , 1 ) ) C_ ( x ( ball ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) r ) )
45 39 26 29 41 43 44 syl221anc 
 |-  ( ( ( ph /\ r e. RR+ ) /\ x e. X ) -> ( x ( ball ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) if ( r <_ 1 , r , 1 ) ) C_ ( x ( ball ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) r ) )
46 36 45 eqsstrrd 
 |-  ( ( ( ph /\ r e. RR+ ) /\ x e. X ) -> ( x ( ball ` D ) if ( r <_ 1 , r , 1 ) ) C_ ( x ( ball ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) r ) )
47 sstr2 
 |-  ( ( x ( ball ` D ) if ( r <_ 1 , r , 1 ) ) C_ ( x ( ball ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) r ) -> ( ( x ( ball ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) r ) C_ u -> ( x ( ball ` D ) if ( r <_ 1 , r , 1 ) ) C_ u ) )
48 46 47 syl 
 |-  ( ( ( ph /\ r e. RR+ ) /\ x e. X ) -> ( ( x ( ball ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) r ) C_ u -> ( x ( ball ` D ) if ( r <_ 1 , r , 1 ) ) C_ u ) )
49 48 reximdv 
 |-  ( ( ( ph /\ r e. RR+ ) /\ x e. X ) -> ( E. u e. U ( x ( ball ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) r ) C_ u -> E. u e. U ( x ( ball ` D ) if ( r <_ 1 , r , 1 ) ) C_ u ) )
50 49 ralimdva 
 |-  ( ( ph /\ r e. RR+ ) -> ( A. x e. X E. u e. U ( x ( ball ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) r ) C_ u -> A. x e. X E. u e. U ( x ( ball ` D ) if ( r <_ 1 , r , 1 ) ) C_ u ) )
51 oveq2 
 |-  ( d = if ( r <_ 1 , r , 1 ) -> ( x ( ball ` D ) d ) = ( x ( ball ` D ) if ( r <_ 1 , r , 1 ) ) )
52 51 sseq1d 
 |-  ( d = if ( r <_ 1 , r , 1 ) -> ( ( x ( ball ` D ) d ) C_ u <-> ( x ( ball ` D ) if ( r <_ 1 , r , 1 ) ) C_ u ) )
53 52 rexbidv 
 |-  ( d = if ( r <_ 1 , r , 1 ) -> ( E. u e. U ( x ( ball ` D ) d ) C_ u <-> E. u e. U ( x ( ball ` D ) if ( r <_ 1 , r , 1 ) ) C_ u ) )
54 53 ralbidv 
 |-  ( d = if ( r <_ 1 , r , 1 ) -> ( A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u <-> A. x e. X E. u e. U ( x ( ball ` D ) if ( r <_ 1 , r , 1 ) ) C_ u ) )
55 54 rspcev 
 |-  ( ( if ( r <_ 1 , r , 1 ) e. RR+ /\ A. x e. X E. u e. U ( x ( ball ` D ) if ( r <_ 1 , r , 1 ) ) C_ u ) -> E. d e. RR+ A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u )
56 22 50 55 syl6an 
 |-  ( ( ph /\ r e. RR+ ) -> ( A. x e. X E. u e. U ( x ( ball ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) r ) C_ u -> E. d e. RR+ A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u ) )
57 56 rexlimdva 
 |-  ( ph -> ( E. r e. RR+ A. x e. X E. u e. U ( x ( ball ` ( y e. X , z e. X |-> if ( ( y D z ) <_ 1 , ( y D z ) , 1 ) ) ) r ) C_ u -> E. d e. RR+ A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u ) )
58 19 57 mpd 
 |-  ( ph -> E. d e. RR+ A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u )