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 )