MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  metrest Structured version   Unicode version

Theorem metrest 21474
Description: Two alternate formulations of a subspace topology of a metric space topology. (Contributed by Jeff Hankins, 19-Aug-2009.) (Proof shortened by Mario Carneiro, 5-Jan-2014.)
Hypotheses
Ref Expression
metrest.1  |-  D  =  ( C  |`  ( Y  X.  Y ) )
metrest.3  |-  J  =  ( MetOpen `  C )
metrest.4  |-  K  =  ( MetOpen `  D )
Assertion
Ref Expression
metrest  |-  ( ( C  e.  ( *Met `  X )  /\  Y  C_  X
)  ->  ( Jt  Y
)  =  K )

Proof of Theorem metrest
Dummy variables  u  r  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 inss1 3618 . . . . . . . . . 10  |-  ( u  i^i  Y )  C_  u
2 metrest.3 . . . . . . . . . . . . 13  |-  J  =  ( MetOpen `  C )
32elmopn2 21395 . . . . . . . . . . . 12  |-  ( C  e.  ( *Met `  X )  ->  (
u  e.  J  <->  ( u  C_  X  /\  A. y  e.  u  E. r  e.  RR+  ( y (
ball `  C )
r )  C_  u
) ) )
43simplbda 628 . . . . . . . . . . 11  |-  ( ( C  e.  ( *Met `  X )  /\  u  e.  J
)  ->  A. y  e.  u  E. r  e.  RR+  ( y (
ball `  C )
r )  C_  u
)
54adantlr 719 . . . . . . . . . 10  |-  ( ( ( C  e.  ( *Met `  X
)  /\  Y  C_  X
)  /\  u  e.  J )  ->  A. y  e.  u  E. r  e.  RR+  ( y (
ball `  C )
r )  C_  u
)
6 ssralv 3461 . . . . . . . . . 10  |-  ( ( u  i^i  Y ) 
C_  u  ->  ( A. y  e.  u  E. r  e.  RR+  (
y ( ball `  C
) r )  C_  u  ->  A. y  e.  ( u  i^i  Y ) E. r  e.  RR+  ( y ( ball `  C ) r ) 
C_  u ) )
71, 5, 6mpsyl 65 . . . . . . . . 9  |-  ( ( ( C  e.  ( *Met `  X
)  /\  Y  C_  X
)  /\  u  e.  J )  ->  A. y  e.  ( u  i^i  Y
) E. r  e.  RR+  ( y ( ball `  C ) r ) 
C_  u )
8 ssrin 3623 . . . . . . . . . . 11  |-  ( ( y ( ball `  C
) r )  C_  u  ->  ( ( y ( ball `  C
) r )  i^i 
Y )  C_  (
u  i^i  Y )
)
98reximi 2826 . . . . . . . . . 10  |-  ( E. r  e.  RR+  (
y ( ball `  C
) r )  C_  u  ->  E. r  e.  RR+  ( ( y (
ball `  C )
r )  i^i  Y
)  C_  ( u  i^i  Y ) )
109ralimi 2752 . . . . . . . . 9  |-  ( A. y  e.  ( u  i^i  Y ) E. r  e.  RR+  ( y (
ball `  C )
r )  C_  u  ->  A. y  e.  ( u  i^i  Y ) E. r  e.  RR+  ( ( y (
ball `  C )
r )  i^i  Y
)  C_  ( u  i^i  Y ) )
117, 10syl 17 . . . . . . . 8  |-  ( ( ( C  e.  ( *Met `  X
)  /\  Y  C_  X
)  /\  u  e.  J )  ->  A. y  e.  ( u  i^i  Y
) E. r  e.  RR+  ( ( y (
ball `  C )
r )  i^i  Y
)  C_  ( u  i^i  Y ) )
12 inss2 3619 . . . . . . . 8  |-  ( u  i^i  Y )  C_  Y
1311, 12jctil 539 . . . . . . 7  |-  ( ( ( C  e.  ( *Met `  X
)  /\  Y  C_  X
)  /\  u  e.  J )  ->  (
( u  i^i  Y
)  C_  Y  /\  A. y  e.  ( u  i^i  Y ) E. r  e.  RR+  (
( y ( ball `  C ) r )  i^i  Y )  C_  ( u  i^i  Y ) ) )
14 sseq1 3421 . . . . . . . 8  |-  ( x  =  ( u  i^i 
Y )  ->  (
x  C_  Y  <->  ( u  i^i  Y )  C_  Y
) )
15 sseq2 3422 . . . . . . . . . 10  |-  ( x  =  ( u  i^i 
Y )  ->  (
( ( y (
ball `  C )
r )  i^i  Y
)  C_  x  <->  ( (
y ( ball `  C
) r )  i^i 
Y )  C_  (
u  i^i  Y )
) )
1615rexbidv 2872 . . . . . . . . 9  |-  ( x  =  ( u  i^i 
Y )  ->  ( E. r  e.  RR+  (
( y ( ball `  C ) r )  i^i  Y )  C_  x 
<->  E. r  e.  RR+  ( ( y (
ball `  C )
r )  i^i  Y
)  C_  ( u  i^i  Y ) ) )
1716raleqbi1dv 2966 . . . . . . . 8  |-  ( x  =  ( u  i^i 
Y )  ->  ( A. y  e.  x  E. r  e.  RR+  (
( y ( ball `  C ) r )  i^i  Y )  C_  x 
<-> 
A. y  e.  ( u  i^i  Y ) E. r  e.  RR+  ( ( y (
ball `  C )
r )  i^i  Y
)  C_  ( u  i^i  Y ) ) )
1814, 17anbi12d 715 . . . . . . 7  |-  ( x  =  ( u  i^i 
Y )  ->  (
( x  C_  Y  /\  A. y  e.  x  E. r  e.  RR+  (
( y ( ball `  C ) r )  i^i  Y )  C_  x )  <->  ( (
u  i^i  Y )  C_  Y  /\  A. y  e.  ( u  i^i  Y
) E. r  e.  RR+  ( ( y (
ball `  C )
r )  i^i  Y
)  C_  ( u  i^i  Y ) ) ) )
1913, 18syl5ibrcom 225 . . . . . 6  |-  ( ( ( C  e.  ( *Met `  X
)  /\  Y  C_  X
)  /\  u  e.  J )  ->  (
x  =  ( u  i^i  Y )  -> 
( x  C_  Y  /\  A. y  e.  x  E. r  e.  RR+  (
( y ( ball `  C ) r )  i^i  Y )  C_  x ) ) )
2019rexlimdva 2850 . . . . 5  |-  ( ( C  e.  ( *Met `  X )  /\  Y  C_  X
)  ->  ( E. u  e.  J  x  =  ( u  i^i 
Y )  ->  (
x  C_  Y  /\  A. y  e.  x  E. r  e.  RR+  ( ( y ( ball `  C
) r )  i^i 
Y )  C_  x
) ) )
212mopntop 21390 . . . . . . . . 9  |-  ( C  e.  ( *Met `  X )  ->  J  e.  Top )
2221ad2antrr 730 . . . . . . . 8  |-  ( ( ( C  e.  ( *Met `  X
)  /\  Y  C_  X
)  /\  ( x  C_  Y  /\  A. y  e.  x  E. r  e.  RR+  ( ( y ( ball `  C
) r )  i^i 
Y )  C_  x
) )  ->  J  e.  Top )
23 ssel2 3395 . . . . . . . . . . . . . 14  |-  ( ( x  C_  Y  /\  y  e.  x )  ->  y  e.  Y )
24 ssel2 3395 . . . . . . . . . . . . . . . 16  |-  ( ( Y  C_  X  /\  y  e.  Y )  ->  y  e.  X )
25 rpxr 11253 . . . . . . . . . . . . . . . . . 18  |-  ( r  e.  RR+  ->  r  e. 
RR* )
262blopn 21450 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( C  e.  ( *Met `  X )  /\  y  e.  X  /\  r  e.  RR* )  ->  ( y ( ball `  C ) r )  e.  J )
27 eleq1a 2495 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( y ( ball `  C
) r )  e.  J  ->  ( z  =  ( y (
ball `  C )
r )  ->  z  e.  J ) )
2826, 27syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ( C  e.  ( *Met `  X )  /\  y  e.  X  /\  r  e.  RR* )  ->  ( z  =  ( y ( ball `  C
) r )  -> 
z  e.  J ) )
29283expa 1205 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( C  e.  ( *Met `  X
)  /\  y  e.  X )  /\  r  e.  RR* )  ->  (
z  =  ( y ( ball `  C
) r )  -> 
z  e.  J ) )
3025, 29sylan2 476 . . . . . . . . . . . . . . . . 17  |-  ( ( ( C  e.  ( *Met `  X
)  /\  y  e.  X )  /\  r  e.  RR+ )  ->  (
z  =  ( y ( ball `  C
) r )  -> 
z  e.  J ) )
3130rexlimdva 2850 . . . . . . . . . . . . . . . 16  |-  ( ( C  e.  ( *Met `  X )  /\  y  e.  X
)  ->  ( E. r  e.  RR+  z  =  ( y ( ball `  C ) r )  ->  z  e.  J
) )
3224, 31sylan2 476 . . . . . . . . . . . . . . 15  |-  ( ( C  e.  ( *Met `  X )  /\  ( Y  C_  X  /\  y  e.  Y
) )  ->  ( E. r  e.  RR+  z  =  ( y (
ball `  C )
r )  ->  z  e.  J ) )
3332anassrs 652 . . . . . . . . . . . . . 14  |-  ( ( ( C  e.  ( *Met `  X
)  /\  Y  C_  X
)  /\  y  e.  Y )  ->  ( E. r  e.  RR+  z  =  ( y (
ball `  C )
r )  ->  z  e.  J ) )
3423, 33sylan2 476 . . . . . . . . . . . . 13  |-  ( ( ( C  e.  ( *Met `  X
)  /\  Y  C_  X
)  /\  ( x  C_  Y  /\  y  e.  x ) )  -> 
( E. r  e.  RR+  z  =  (
y ( ball `  C
) r )  -> 
z  e.  J ) )
3534anassrs 652 . . . . . . . . . . . 12  |-  ( ( ( ( C  e.  ( *Met `  X )  /\  Y  C_  X )  /\  x  C_  Y )  /\  y  e.  x )  ->  ( E. r  e.  RR+  z  =  ( y (
ball `  C )
r )  ->  z  e.  J ) )
3635rexlimdva 2850 . . . . . . . . . . 11  |-  ( ( ( C  e.  ( *Met `  X
)  /\  Y  C_  X
)  /\  x  C_  Y
)  ->  ( E. y  e.  x  E. r  e.  RR+  z  =  ( y ( ball `  C ) r )  ->  z  e.  J
) )
3736adantrd 469 . . . . . . . . . 10  |-  ( ( ( C  e.  ( *Met `  X
)  /\  Y  C_  X
)  /\  x  C_  Y
)  ->  ( ( E. y  e.  x  E. r  e.  RR+  z  =  ( y (
ball `  C )
r )  /\  (
z  i^i  Y )  C_  x )  ->  z  e.  J ) )
3837adantrr 721 . . . . . . . . 9  |-  ( ( ( C  e.  ( *Met `  X
)  /\  Y  C_  X
)  /\  ( x  C_  Y  /\  A. y  e.  x  E. r  e.  RR+  ( ( y ( ball `  C
) r )  i^i 
Y )  C_  x
) )  ->  (
( E. y  e.  x  E. r  e.  RR+  z  =  (
y ( ball `  C
) r )  /\  ( z  i^i  Y
)  C_  x )  ->  z  e.  J ) )
3938abssdv 3471 . . . . . . . 8  |-  ( ( ( C  e.  ( *Met `  X
)  /\  Y  C_  X
)  /\  ( x  C_  Y  /\  A. y  e.  x  E. r  e.  RR+  ( ( y ( ball `  C
) r )  i^i 
Y )  C_  x
) )  ->  { z  |  ( E. y  e.  x  E. r  e.  RR+  z  =  ( y ( ball `  C
) r )  /\  ( z  i^i  Y
)  C_  x ) }  C_  J )
40 uniopn 19862 . . . . . . . 8  |-  ( ( J  e.  Top  /\  { z  |  ( E. y  e.  x  E. r  e.  RR+  z  =  ( y ( ball `  C ) r )  /\  ( z  i^i 
Y )  C_  x
) }  C_  J
)  ->  U. { z  |  ( E. y  e.  x  E. r  e.  RR+  z  =  ( y ( ball `  C
) r )  /\  ( z  i^i  Y
)  C_  x ) }  e.  J )
4122, 39, 40syl2anc 665 . . . . . . 7  |-  ( ( ( C  e.  ( *Met `  X
)  /\  Y  C_  X
)  /\  ( x  C_  Y  /\  A. y  e.  x  E. r  e.  RR+  ( ( y ( ball `  C
) r )  i^i 
Y )  C_  x
) )  ->  U. {
z  |  ( E. y  e.  x  E. r  e.  RR+  z  =  ( y ( ball `  C ) r )  /\  ( z  i^i 
Y )  C_  x
) }  e.  J
)
42 oveq1 6249 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  u  ->  (
y ( ball `  C
) r )  =  ( u ( ball `  C ) r ) )
4342ineq1d 3599 . . . . . . . . . . . . . . . . 17  |-  ( y  =  u  ->  (
( y ( ball `  C ) r )  i^i  Y )  =  ( ( u (
ball `  C )
r )  i^i  Y
) )
4443sseq1d 3427 . . . . . . . . . . . . . . . 16  |-  ( y  =  u  ->  (
( ( y (
ball `  C )
r )  i^i  Y
)  C_  x  <->  ( (
u ( ball `  C
) r )  i^i 
Y )  C_  x
) )
4544rexbidv 2872 . . . . . . . . . . . . . . 15  |-  ( y  =  u  ->  ( E. r  e.  RR+  (
( y ( ball `  C ) r )  i^i  Y )  C_  x 
<->  E. r  e.  RR+  ( ( u (
ball `  C )
r )  i^i  Y
)  C_  x )
)
4645rspccv 3115 . . . . . . . . . . . . . 14  |-  ( A. y  e.  x  E. r  e.  RR+  ( ( y ( ball `  C
) r )  i^i 
Y )  C_  x  ->  ( u  e.  x  ->  E. r  e.  RR+  ( ( u (
ball `  C )
r )  i^i  Y
)  C_  x )
)
4746ad2antll 733 . . . . . . . . . . . . 13  |-  ( ( ( C  e.  ( *Met `  X
)  /\  Y  C_  X
)  /\  ( x  C_  Y  /\  A. y  e.  x  E. r  e.  RR+  ( ( y ( ball `  C
) r )  i^i 
Y )  C_  x
) )  ->  (
u  e.  x  ->  E. r  e.  RR+  (
( u ( ball `  C ) r )  i^i  Y )  C_  x ) )
48 ssel 3394 . . . . . . . . . . . . . . 15  |-  ( x 
C_  Y  ->  (
u  e.  x  ->  u  e.  Y )
)
49 ssel 3394 . . . . . . . . . . . . . . . 16  |-  ( Y 
C_  X  ->  (
u  e.  Y  ->  u  e.  X )
)
50 blcntr 21363 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( C  e.  ( *Met `  X )  /\  u  e.  X  /\  r  e.  RR+ )  ->  u  e.  ( u ( ball `  C
) r ) )
5150a1d 26 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( C  e.  ( *Met `  X )  /\  u  e.  X  /\  r  e.  RR+ )  ->  ( ( ( u ( ball `  C
) r )  i^i 
Y )  C_  x  ->  u  e.  ( u ( ball `  C
) r ) ) )
5251ancld 555 . . . . . . . . . . . . . . . . . . 19  |-  ( ( C  e.  ( *Met `  X )  /\  u  e.  X  /\  r  e.  RR+ )  ->  ( ( ( u ( ball `  C
) r )  i^i 
Y )  C_  x  ->  ( ( ( u ( ball `  C
) r )  i^i 
Y )  C_  x  /\  u  e.  (
u ( ball `  C
) r ) ) ) )
53523expa 1205 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( C  e.  ( *Met `  X
)  /\  u  e.  X )  /\  r  e.  RR+ )  ->  (
( ( u (
ball `  C )
r )  i^i  Y
)  C_  x  ->  ( ( ( u (
ball `  C )
r )  i^i  Y
)  C_  x  /\  u  e.  ( u
( ball `  C )
r ) ) ) )
5453reximdva 2833 . . . . . . . . . . . . . . . . 17  |-  ( ( C  e.  ( *Met `  X )  /\  u  e.  X
)  ->  ( E. r  e.  RR+  ( ( u ( ball `  C
) r )  i^i 
Y )  C_  x  ->  E. r  e.  RR+  ( ( ( u ( ball `  C
) r )  i^i 
Y )  C_  x  /\  u  e.  (
u ( ball `  C
) r ) ) ) )
5554ex 435 . . . . . . . . . . . . . . . 16  |-  ( C  e.  ( *Met `  X )  ->  (
u  e.  X  -> 
( E. r  e.  RR+  ( ( u (
ball `  C )
r )  i^i  Y
)  C_  x  ->  E. r  e.  RR+  (
( ( u (
ball `  C )
r )  i^i  Y
)  C_  x  /\  u  e.  ( u
( ball `  C )
r ) ) ) ) )
5649, 55sylan9r 662 . . . . . . . . . . . . . . 15  |-  ( ( C  e.  ( *Met `  X )  /\  Y  C_  X
)  ->  ( u  e.  Y  ->  ( E. r  e.  RR+  (
( u ( ball `  C ) r )  i^i  Y )  C_  x  ->  E. r  e.  RR+  ( ( ( u ( ball `  C
) r )  i^i 
Y )  C_  x  /\  u  e.  (
u ( ball `  C
) r ) ) ) ) )
5748, 56sylan9r 662 . . . . . . . . . . . . . 14  |-  ( ( ( C  e.  ( *Met `  X
)  /\  Y  C_  X
)  /\  x  C_  Y
)  ->  ( u  e.  x  ->  ( E. r  e.  RR+  (
( u ( ball `  C ) r )  i^i  Y )  C_  x  ->  E. r  e.  RR+  ( ( ( u ( ball `  C
) r )  i^i 
Y )  C_  x  /\  u  e.  (
u ( ball `  C
) r ) ) ) ) )
5857adantrr 721 . . . . . . . . . . . . 13  |-  ( ( ( C  e.  ( *Met `  X
)  /\  Y  C_  X
)  /\  ( x  C_  Y  /\  A. y  e.  x  E. r  e.  RR+  ( ( y ( ball `  C
) r )  i^i 
Y )  C_  x
) )  ->  (
u  e.  x  -> 
( E. r  e.  RR+  ( ( u (
ball `  C )
r )  i^i  Y
)  C_  x  ->  E. r  e.  RR+  (
( ( u (
ball `  C )
r )  i^i  Y
)  C_  x  /\  u  e.  ( u
( ball `  C )
r ) ) ) ) )
5947, 58mpdd 41 . . . . . . . . . . . 12  |-  ( ( ( C  e.  ( *Met `  X
)  /\  Y  C_  X
)  /\  ( x  C_  Y  /\  A. y  e.  x  E. r  e.  RR+  ( ( y ( ball `  C
) r )  i^i 
Y )  C_  x
) )  ->  (
u  e.  x  ->  E. r  e.  RR+  (
( ( u (
ball `  C )
r )  i^i  Y
)  C_  x  /\  u  e.  ( u
( ball `  C )
r ) ) ) )
6042eleq2d 2485 . . . . . . . . . . . . . . . 16  |-  ( y  =  u  ->  (
u  e.  ( y ( ball `  C
) r )  <->  u  e.  ( u ( ball `  C ) r ) ) )
6144, 60anbi12d 715 . . . . . . . . . . . . . . 15  |-  ( y  =  u  ->  (
( ( ( y ( ball `  C
) r )  i^i 
Y )  C_  x  /\  u  e.  (
y ( ball `  C
) r ) )  <-> 
( ( ( u ( ball `  C
) r )  i^i 
Y )  C_  x  /\  u  e.  (
u ( ball `  C
) r ) ) ) )
6261rexbidv 2872 . . . . . . . . . . . . . 14  |-  ( y  =  u  ->  ( E. r  e.  RR+  (
( ( y (
ball `  C )
r )  i^i  Y
)  C_  x  /\  u  e.  ( y
( ball `  C )
r ) )  <->  E. r  e.  RR+  ( ( ( u ( ball `  C
) r )  i^i 
Y )  C_  x  /\  u  e.  (
u ( ball `  C
) r ) ) ) )
6362rspcev 3118 . . . . . . . . . . . . 13  |-  ( ( u  e.  x  /\  E. r  e.  RR+  (
( ( u (
ball `  C )
r )  i^i  Y
)  C_  x  /\  u  e.  ( u
( ball `  C )
r ) ) )  ->  E. y  e.  x  E. r  e.  RR+  (
( ( y (
ball `  C )
r )  i^i  Y
)  C_  x  /\  u  e.  ( y
( ball `  C )
r ) ) )
6463ex 435 . . . . . . . . . . . 12  |-  ( u  e.  x  ->  ( E. r  e.  RR+  (
( ( u (
ball `  C )
r )  i^i  Y
)  C_  x  /\  u  e.  ( u
( ball `  C )
r ) )  ->  E. y  e.  x  E. r  e.  RR+  (
( ( y (
ball `  C )
r )  i^i  Y
)  C_  x  /\  u  e.  ( y
( ball `  C )
r ) ) ) )
6559, 64sylcom 30 . . . . . . . . . . 11  |-  ( ( ( C  e.  ( *Met `  X
)  /\  Y  C_  X
)  /\  ( x  C_  Y  /\  A. y  e.  x  E. r  e.  RR+  ( ( y ( ball `  C
) r )  i^i 
Y )  C_  x
) )  ->  (
u  e.  x  ->  E. y  e.  x  E. r  e.  RR+  (
( ( y (
ball `  C )
r )  i^i  Y
)  C_  x  /\  u  e.  ( y
( ball `  C )
r ) ) ) )
66 simprl 762 . . . . . . . . . . . 12  |-  ( ( ( C  e.  ( *Met `  X
)  /\  Y  C_  X
)  /\  ( x  C_  Y  /\  A. y  e.  x  E. r  e.  RR+  ( ( y ( ball `  C
) r )  i^i 
Y )  C_  x
) )  ->  x  C_  Y )
6766sseld 3399 . . . . . . . . . . 11  |-  ( ( ( C  e.  ( *Met `  X
)  /\  Y  C_  X
)  /\  ( x  C_  Y  /\  A. y  e.  x  E. r  e.  RR+  ( ( y ( ball `  C
) r )  i^i 
Y )  C_  x
) )  ->  (
u  e.  x  ->  u  e.  Y )
)
6865, 67jcad 535 . . . . . . . . . 10  |-  ( ( ( C  e.  ( *Met `  X
)  /\  Y  C_  X
)  /\  ( x  C_  Y  /\  A. y  e.  x  E. r  e.  RR+  ( ( y ( ball `  C
) r )  i^i 
Y )  C_  x
) )  ->  (
u  e.  x  -> 
( E. y  e.  x  E. r  e.  RR+  ( ( ( y ( ball `  C
) r )  i^i 
Y )  C_  x  /\  u  e.  (
y ( ball `  C
) r ) )  /\  u  e.  Y
) ) )
69 elin 3585 . . . . . . . . . . . . . . 15  |-  ( u  e.  ( ( y ( ball `  C
) r )  i^i 
Y )  <->  ( u  e.  ( y ( ball `  C ) r )  /\  u  e.  Y
) )
70 ssel2 3395 . . . . . . . . . . . . . . 15  |-  ( ( ( ( y (
ball `  C )
r )  i^i  Y
)  C_  x  /\  u  e.  ( (
y ( ball `  C
) r )  i^i 
Y ) )  ->  u  e.  x )
7169, 70sylan2br 478 . . . . . . . . . . . . . 14  |-  ( ( ( ( y (
ball `  C )
r )  i^i  Y
)  C_  x  /\  ( u  e.  (
y ( ball `  C
) r )  /\  u  e.  Y )
)  ->  u  e.  x )
7271expr 618 . . . . . . . . . . . . 13  |-  ( ( ( ( y (
ball `  C )
r )  i^i  Y
)  C_  x  /\  u  e.  ( y
( ball `  C )
r ) )  -> 
( u  e.  Y  ->  u  e.  x ) )
7372rexlimivw 2847 . . . . . . . . . . . 12  |-  ( E. r  e.  RR+  (
( ( y (
ball `  C )
r )  i^i  Y
)  C_  x  /\  u  e.  ( y
( ball `  C )
r ) )  -> 
( u  e.  Y  ->  u  e.  x ) )
7473rexlimivw 2847 . . . . . . . . . . 11  |-  ( E. y  e.  x  E. r  e.  RR+  ( ( ( y ( ball `  C ) r )  i^i  Y )  C_  x  /\  u  e.  ( y ( ball `  C
) r ) )  ->  ( u  e.  Y  ->  u  e.  x ) )
7574imp 430 . . . . . . . . . 10  |-  ( ( E. y  e.  x  E. r  e.  RR+  (
( ( y (
ball `  C )
r )  i^i  Y
)  C_  x  /\  u  e.  ( y
( ball `  C )
r ) )  /\  u  e.  Y )  ->  u  e.  x )
7668, 75impbid1 206 . . . . . . . . 9  |-  ( ( ( C  e.  ( *Met `  X
)  /\  Y  C_  X
)  /\  ( x  C_  Y  /\  A. y  e.  x  E. r  e.  RR+  ( ( y ( ball `  C
) r )  i^i 
Y )  C_  x
) )  ->  (
u  e.  x  <->  ( E. y  e.  x  E. r  e.  RR+  ( ( ( y ( ball `  C ) r )  i^i  Y )  C_  x  /\  u  e.  ( y ( ball `  C
) r ) )  /\  u  e.  Y
) ) )
77 elin 3585 . . . . . . . . . 10  |-  ( u  e.  ( U. {
z  |  ( E. y  e.  x  E. r  e.  RR+  z  =  ( y ( ball `  C ) r )  /\  ( z  i^i 
Y )  C_  x
) }  i^i  Y
)  <->  ( u  e. 
U. { z  |  ( E. y  e.  x  E. r  e.  RR+  z  =  (
y ( ball `  C
) r )  /\  ( z  i^i  Y
)  C_  x ) }  /\  u  e.  Y
) )
78 eluniab 4166 . . . . . . . . . . . 12  |-  ( u  e.  U. { z  |  ( E. y  e.  x  E. r  e.  RR+  z  =  ( y ( ball `  C
) r )  /\  ( z  i^i  Y
)  C_  x ) } 
<->  E. z ( u  e.  z  /\  ( E. y  e.  x  E. r  e.  RR+  z  =  ( y (
ball `  C )
r )  /\  (
z  i^i  Y )  C_  x ) ) )
79 ancom 451 . . . . . . . . . . . . . 14  |-  ( ( u  e.  z  /\  ( E. y  e.  x  E. r  e.  RR+  z  =  ( y (
ball `  C )
r )  /\  (
z  i^i  Y )  C_  x ) )  <->  ( ( E. y  e.  x  E. r  e.  RR+  z  =  ( y (
ball `  C )
r )  /\  (
z  i^i  Y )  C_  x )  /\  u  e.  z ) )
80 anass 653 . . . . . . . . . . . . . 14  |-  ( ( ( E. y  e.  x  E. r  e.  RR+  z  =  (
y ( ball `  C
) r )  /\  ( z  i^i  Y
)  C_  x )  /\  u  e.  z
)  <->  ( E. y  e.  x  E. r  e.  RR+  z  =  ( y ( ball `  C
) r )  /\  ( ( z  i^i 
Y )  C_  x  /\  u  e.  z
) ) )
81 r19.41v 2913 . . . . . . . . . . . . . . . 16  |-  ( E. r  e.  RR+  (
z  =  ( y ( ball `  C
) r )  /\  ( ( z  i^i 
Y )  C_  x  /\  u  e.  z
) )  <->  ( E. r  e.  RR+  z  =  ( y ( ball `  C ) r )  /\  ( ( z  i^i  Y )  C_  x  /\  u  e.  z ) ) )
8281rexbii 2860 . . . . . . . . . . . . . . 15  |-  ( E. y  e.  x  E. r  e.  RR+  ( z  =  ( y (
ball `  C )
r )  /\  (
( z  i^i  Y
)  C_  x  /\  u  e.  z )
)  <->  E. y  e.  x  ( E. r  e.  RR+  z  =  ( y
( ball `  C )
r )  /\  (
( z  i^i  Y
)  C_  x  /\  u  e.  z )
) )
83 r19.41v 2913 . . . . . . . . . . . . . . 15  |-  ( E. y  e.  x  ( E. r  e.  RR+  z  =  ( y
( ball `  C )
r )  /\  (
( z  i^i  Y
)  C_  x  /\  u  e.  z )
)  <->  ( E. y  e.  x  E. r  e.  RR+  z  =  ( y ( ball `  C
) r )  /\  ( ( z  i^i 
Y )  C_  x  /\  u  e.  z
) ) )
8482, 83bitr2i 253 . . . . . . . . . . . . . 14  |-  ( ( E. y  e.  x  E. r  e.  RR+  z  =  ( y (
ball `  C )
r )  /\  (
( z  i^i  Y
)  C_  x  /\  u  e.  z )
)  <->  E. y  e.  x  E. r  e.  RR+  (
z  =  ( y ( ball `  C
) r )  /\  ( ( z  i^i 
Y )  C_  x  /\  u  e.  z
) ) )
8579, 80, 843bitri 274 . . . . . . . . . . . . 13  |-  ( ( u  e.  z  /\  ( E. y  e.  x  E. r  e.  RR+  z  =  ( y (
ball `  C )
r )  /\  (
z  i^i  Y )  C_  x ) )  <->  E. y  e.  x  E. r  e.  RR+  ( z  =  ( y ( ball `  C ) r )  /\  ( ( z  i^i  Y )  C_  x  /\  u  e.  z ) ) )
8685exbii 1712 . . . . . . . . . . . 12  |-  ( E. z ( u  e.  z  /\  ( E. y  e.  x  E. r  e.  RR+  z  =  ( y ( ball `  C ) r )  /\  ( z  i^i 
Y )  C_  x
) )  <->  E. z E. y  e.  x  E. r  e.  RR+  (
z  =  ( y ( ball `  C
) r )  /\  ( ( z  i^i 
Y )  C_  x  /\  u  e.  z
) ) )
87 ovex 6270 . . . . . . . . . . . . . . . . 17  |-  ( y ( ball `  C
) r )  e. 
_V
88 ineq1 3593 . . . . . . . . . . . . . . . . . . 19  |-  ( z  =  ( y (
ball `  C )
r )  ->  (
z  i^i  Y )  =  ( ( y ( ball `  C
) r )  i^i 
Y ) )
8988sseq1d 3427 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  ( y (
ball `  C )
r )  ->  (
( z  i^i  Y
)  C_  x  <->  ( (
y ( ball `  C
) r )  i^i 
Y )  C_  x
) )
90 eleq2 2489 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  ( y (
ball `  C )
r )  ->  (
u  e.  z  <->  u  e.  ( y ( ball `  C ) r ) ) )
9189, 90anbi12d 715 . . . . . . . . . . . . . . . . 17  |-  ( z  =  ( y (
ball `  C )
r )  ->  (
( ( z  i^i 
Y )  C_  x  /\  u  e.  z
)  <->  ( ( ( y ( ball `  C
) r )  i^i 
Y )  C_  x  /\  u  e.  (
y ( ball `  C
) r ) ) ) )
9287, 91ceqsexv 3054 . . . . . . . . . . . . . . . 16  |-  ( E. z ( z  =  ( y ( ball `  C ) r )  /\  ( ( z  i^i  Y )  C_  x  /\  u  e.  z ) )  <->  ( (
( y ( ball `  C ) r )  i^i  Y )  C_  x  /\  u  e.  ( y ( ball `  C
) r ) ) )
9392rexbii 2860 . . . . . . . . . . . . . . 15  |-  ( E. r  e.  RR+  E. z
( z  =  ( y ( ball `  C
) r )  /\  ( ( z  i^i 
Y )  C_  x  /\  u  e.  z
) )  <->  E. r  e.  RR+  ( ( ( y ( ball `  C
) r )  i^i 
Y )  C_  x  /\  u  e.  (
y ( ball `  C
) r ) ) )
94 rexcom4 3037 . . . . . . . . . . . . . . 15  |-  ( E. r  e.  RR+  E. z
( z  =  ( y ( ball `  C
) r )  /\  ( ( z  i^i 
Y )  C_  x  /\  u  e.  z
) )  <->  E. z E. r  e.  RR+  (
z  =  ( y ( ball `  C
) r )  /\  ( ( z  i^i 
Y )  C_  x  /\  u  e.  z
) ) )
9593, 94bitr3i 254 . . . . . . . . . . . . . 14  |-  ( E. r  e.  RR+  (
( ( y (
ball `  C )
r )  i^i  Y
)  C_  x  /\  u  e.  ( y
( ball `  C )
r ) )  <->  E. z E. r  e.  RR+  (
z  =  ( y ( ball `  C
) r )  /\  ( ( z  i^i 
Y )  C_  x  /\  u  e.  z
) ) )
9695rexbii 2860 . . . . . . . . . . . . 13  |-  ( E. y  e.  x  E. r  e.  RR+  ( ( ( y ( ball `  C ) r )  i^i  Y )  C_  x  /\  u  e.  ( y ( ball `  C
) r ) )  <->  E. y  e.  x  E. z E. r  e.  RR+  ( z  =  ( y ( ball `  C
) r )  /\  ( ( z  i^i 
Y )  C_  x  /\  u  e.  z
) ) )
97 rexcom4 3037 . . . . . . . . . . . . 13  |-  ( E. y  e.  x  E. z E. r  e.  RR+  ( z  =  ( y ( ball `  C
) r )  /\  ( ( z  i^i 
Y )  C_  x  /\  u  e.  z
) )  <->  E. z E. y  e.  x  E. r  e.  RR+  (
z  =  ( y ( ball `  C
) r )  /\  ( ( z  i^i 
Y )  C_  x  /\  u  e.  z
) ) )
9896, 97bitr2i 253 . . . . . . . . . . . 12  |-  ( E. z E. y  e.  x  E. r  e.  RR+  ( z  =  ( y ( ball `  C
) r )  /\  ( ( z  i^i 
Y )  C_  x  /\  u  e.  z
) )  <->  E. y  e.  x  E. r  e.  RR+  ( ( ( y ( ball `  C
) r )  i^i 
Y )  C_  x  /\  u  e.  (
y ( ball `  C
) r ) ) )
9978, 86, 983bitri 274 . . . . . . . . . . 11  |-  ( u  e.  U. { z  |  ( E. y  e.  x  E. r  e.  RR+  z  =  ( y ( ball `  C
) r )  /\  ( z  i^i  Y
)  C_  x ) } 
<->  E. y  e.  x  E. r  e.  RR+  (
( ( y (
ball `  C )
r )  i^i  Y
)  C_  x  /\  u  e.  ( y
( ball `  C )
r ) ) )
10099anbi1i 699 . . . . . . . . . 10  |-  ( ( u  e.  U. {
z  |  ( E. y  e.  x  E. r  e.  RR+  z  =  ( y ( ball `  C ) r )  /\  ( z  i^i 
Y )  C_  x
) }  /\  u  e.  Y )  <->  ( E. y  e.  x  E. r  e.  RR+  ( ( ( y ( ball `  C ) r )  i^i  Y )  C_  x  /\  u  e.  ( y ( ball `  C
) r ) )  /\  u  e.  Y
) )
10177, 100bitr2i 253 . . . . . . . . 9  |-  ( ( E. y  e.  x  E. r  e.  RR+  (
( ( y (
ball `  C )
r )  i^i  Y
)  C_  x  /\  u  e.  ( y
( ball `  C )
r ) )  /\  u  e.  Y )  <->  u  e.  ( U. {
z  |  ( E. y  e.  x  E. r  e.  RR+  z  =  ( y ( ball `  C ) r )  /\  ( z  i^i 
Y )  C_  x
) }  i^i  Y
) )
10276, 101syl6bb 264 . . . . . . . 8  |-  ( ( ( C  e.  ( *Met `  X
)  /\  Y  C_  X
)  /\  ( x  C_  Y  /\  A. y  e.  x  E. r  e.  RR+  ( ( y ( ball `  C
) r )  i^i 
Y )  C_  x
) )  ->  (
u  e.  x  <->  u  e.  ( U. { z  |  ( E. y  e.  x  E. r  e.  RR+  z  =  (
y ( ball `  C
) r )  /\  ( z  i^i  Y
)  C_  x ) }  i^i  Y ) ) )
103102eqrdv 2420 . . . . . . 7  |-  ( ( ( C  e.  ( *Met `  X
)  /\  Y  C_  X
)  /\  ( x  C_  Y  /\  A. y  e.  x  E. r  e.  RR+  ( ( y ( ball `  C
) r )  i^i 
Y )  C_  x
) )  ->  x  =  ( U. {
z  |  ( E. y  e.  x  E. r  e.  RR+  z  =  ( y ( ball `  C ) r )  /\  ( z  i^i 
Y )  C_  x
) }  i^i  Y
) )
104 ineq1 3593 . . . . . . . . 9  |-  ( u  =  U. { z  |  ( E. y  e.  x  E. r  e.  RR+  z  =  ( y ( ball `  C
) r )  /\  ( z  i^i  Y
)  C_  x ) }  ->  ( u  i^i 
Y )  =  ( U. { z  |  ( E. y  e.  x  E. r  e.  RR+  z  =  (
y ( ball `  C
) r )  /\  ( z  i^i  Y
)  C_  x ) }  i^i  Y ) )
105104eqeq2d 2432 . . . . . . . 8  |-  ( u  =  U. { z  |  ( E. y  e.  x  E. r  e.  RR+  z  =  ( y ( ball `  C
) r )  /\  ( z  i^i  Y
)  C_  x ) }  ->  ( x  =  ( u  i^i  Y
)  <->  x  =  ( U. { z  |  ( E. y  e.  x  E. r  e.  RR+  z  =  ( y (
ball `  C )
r )  /\  (
z  i^i  Y )  C_  x ) }  i^i  Y ) ) )
106105rspcev 3118 . . . . . . 7  |-  ( ( U. { z  |  ( E. y  e.  x  E. r  e.  RR+  z  =  (
y ( ball `  C
) r )  /\  ( z  i^i  Y
)  C_  x ) }  e.  J  /\  x  =  ( U. { z  |  ( E. y  e.  x  E. r  e.  RR+  z  =  ( y (
ball `  C )
r )  /\  (
z  i^i  Y )  C_  x ) }  i^i  Y ) )  ->  E. u  e.  J  x  =  ( u  i^i  Y ) )
10741, 103, 106syl2anc 665 . . . . . 6  |-  ( ( ( C  e.  ( *Met `  X
)  /\  Y  C_  X
)  /\  ( x  C_  Y  /\  A. y  e.  x  E. r  e.  RR+  ( ( y ( ball `  C
) r )  i^i 
Y )  C_  x
) )  ->  E. u  e.  J  x  =  ( u  i^i  Y ) )
108107ex 435 . . . . 5  |-  ( ( C  e.  ( *Met `  X )  /\  Y  C_  X
)  ->  ( (
x  C_  Y  /\  A. y  e.  x  E. r  e.  RR+  ( ( y ( ball `  C
) r )  i^i 
Y )  C_  x
)  ->  E. u  e.  J  x  =  ( u  i^i  Y ) ) )
10920, 108impbid 193 . . . 4  |-  ( ( C  e.  ( *Met `  X )  /\  Y  C_  X
)  ->  ( E. u  e.  J  x  =  ( u  i^i 
Y )  <->  ( x  C_  Y  /\  A. y  e.  x  E. r  e.  RR+  ( ( y ( ball `  C
) r )  i^i 
Y )  C_  x
) ) )
110 simpr 462 . . . . . . . . . . 11  |-  ( ( Y  C_  X  /\  y  e.  Y )  ->  y  e.  Y )
11124, 110elind 3586 . . . . . . . . . 10  |-  ( ( Y  C_  X  /\  y  e.  Y )  ->  y  e.  ( X  i^i  Y ) )
112 metrest.1 . . . . . . . . . . . . . . 15  |-  D  =  ( C  |`  ( Y  X.  Y ) )
113112blres 21381 . . . . . . . . . . . . . 14  |-  ( ( C  e.  ( *Met `  X )  /\  y  e.  ( X  i^i  Y )  /\  r  e.  RR* )  ->  ( y (
ball `  D )
r )  =  ( ( y ( ball `  C ) r )  i^i  Y ) )
114113sseq1d 3427 . . . . . . . . . . . . 13  |-  ( ( C  e.  ( *Met `  X )  /\  y  e.  ( X  i^i  Y )  /\  r  e.  RR* )  ->  ( ( y ( ball `  D
) r )  C_  x 
<->  ( ( y (
ball `  C )
r )  i^i  Y
)  C_  x )
)
1151143expa 1205 . . . . . . . . . . . 12  |-  ( ( ( C  e.  ( *Met `  X
)  /\  y  e.  ( X  i^i  Y ) )  /\  r  e. 
RR* )  ->  (
( y ( ball `  D ) r ) 
C_  x  <->  ( (
y ( ball `  C
) r )  i^i 
Y )  C_  x
) )
11625, 115sylan2 476 . . . . . . . . . . 11  |-  ( ( ( C  e.  ( *Met `  X
)  /\  y  e.  ( X  i^i  Y ) )  /\  r  e.  RR+ )  ->  ( ( y ( ball `  D
) r )  C_  x 
<->  ( ( y (
ball `  C )
r )  i^i  Y
)  C_  x )
)
117116rexbidva 2869 . . . . . . . . . 10  |-  ( ( C  e.  ( *Met `  X )  /\  y  e.  ( X  i^i  Y ) )  ->  ( E. r  e.  RR+  ( y ( ball `  D
) r )  C_  x 
<->  E. r  e.  RR+  ( ( y (
ball `  C )
r )  i^i  Y
)  C_  x )
)
118111, 117sylan2 476 . . . . . . . . 9  |-  ( ( C  e.  ( *Met `  X )  /\  ( Y  C_  X  /\  y  e.  Y
) )  ->  ( E. r  e.  RR+  (
y ( ball `  D
) r )  C_  x 
<->  E. r  e.  RR+  ( ( y (
ball `  C )
r )  i^i  Y
)  C_  x )
)
119118anassrs 652 . . . . . . . 8  |-  ( ( ( C  e.  ( *Met `  X
)  /\  Y  C_  X
)  /\  y  e.  Y )  ->  ( E. r  e.  RR+  (
y ( ball `  D
) r )  C_  x 
<->  E. r  e.  RR+  ( ( y (
ball `  C )
r )  i^i  Y
)  C_  x )
)
12023, 119sylan2 476 . . . . . . 7  |-  ( ( ( C  e.  ( *Met `  X
)  /\  Y  C_  X
)  /\  ( x  C_  Y  /\  y  e.  x ) )  -> 
( E. r  e.  RR+  ( y ( ball `  D ) r ) 
C_  x  <->  E. r  e.  RR+  ( ( y ( ball `  C
) r )  i^i 
Y )  C_  x
) )
121120anassrs 652 . . . . . 6  |-  ( ( ( ( C  e.  ( *Met `  X )  /\  Y  C_  X )  /\  x  C_  Y )  /\  y  e.  x )  ->  ( E. r  e.  RR+  (
y ( ball `  D
) r )  C_  x 
<->  E. r  e.  RR+  ( ( y (
ball `  C )
r )  i^i  Y
)  C_  x )
)
122121ralbidva 2795 . . . . 5  |-  ( ( ( C  e.  ( *Met `  X
)  /\  Y  C_  X
)  /\  x  C_  Y
)  ->  ( A. y  e.  x  E. r  e.  RR+  ( y ( ball `  D
) r )  C_  x 
<-> 
A. y  e.  x  E. r  e.  RR+  (
( y ( ball `  C ) r )  i^i  Y )  C_  x ) )
123122pm5.32da 645 . . . 4  |-  ( ( C  e.  ( *Met `  X )  /\  Y  C_  X
)  ->  ( (
x  C_  Y  /\  A. y  e.  x  E. r  e.  RR+  ( y ( ball `  D
) r )  C_  x )  <->  ( x  C_  Y  /\  A. y  e.  x  E. r  e.  RR+  ( ( y ( ball `  C
) r )  i^i 
Y )  C_  x
) ) )
124109, 123bitr4d 259 . . 3  |-  ( ( C  e.  ( *Met `  X )  /\  Y  C_  X
)  ->  ( E. u  e.  J  x  =  ( u  i^i 
Y )  <->  ( x  C_  Y  /\  A. y  e.  x  E. r  e.  RR+  ( y (
ball `  D )
r )  C_  x
) ) )
12521adantr 466 . . . 4  |-  ( ( C  e.  ( *Met `  X )  /\  Y  C_  X
)  ->  J  e.  Top )
126 id 22 . . . . 5  |-  ( Y 
C_  X  ->  Y  C_  X )
1272mopnm 21394 . . . . 5  |-  ( C  e.  ( *Met `  X )  ->  X  e.  J )
128 ssexg 4506 . . . . 5  |-  ( ( Y  C_  X  /\  X  e.  J )  ->  Y  e.  _V )
129126, 127, 128syl2anr 480 . . . 4  |-  ( ( C  e.  ( *Met `  X )  /\  Y  C_  X
)  ->  Y  e.  _V )
130 elrest 15262 . . . 4  |-  ( ( J  e.  Top  /\  Y  e.  _V )  ->  ( x  e.  ( Jt  Y )  <->  E. u  e.  J  x  =  ( u  i^i  Y ) ) )
131125, 129, 130syl2anc 665 . . 3  |-  ( ( C  e.  ( *Met `  X )  /\  Y  C_  X
)  ->  ( x  e.  ( Jt  Y )  <->  E. u  e.  J  x  =  ( u  i^i  Y ) ) )
132 xmetres2 21311 . . . . 5  |-  ( ( C  e.  ( *Met `  X )  /\  Y  C_  X
)  ->  ( C  |`  ( Y  X.  Y
) )  e.  ( *Met `  Y
) )
133112, 132syl5eqel 2504 . . . 4  |-  ( ( C  e.  ( *Met `  X )  /\  Y  C_  X
)  ->  D  e.  ( *Met `  Y
) )
134 metrest.4 . . . . 5  |-  K  =  ( MetOpen `  D )
135134elmopn2 21395 . . . 4  |-  ( D  e.  ( *Met `  Y )  ->  (
x  e.  K  <->  ( x  C_  Y  /\  A. y  e.  x  E. r  e.  RR+  ( y (
ball `  D )
r )  C_  x
) ) )
136133, 135syl 17 . . 3  |-  ( ( C  e.  ( *Met `  X )  /\  Y  C_  X
)  ->  ( x  e.  K  <->  ( x  C_  Y  /\  A. y  e.  x  E. r  e.  RR+  ( y ( ball `  D ) r ) 
C_  x ) ) )
137124, 131, 1363bitr4d 288 . 2  |-  ( ( C  e.  ( *Met `  X )  /\  Y  C_  X
)  ->  ( x  e.  ( Jt  Y )  <->  x  e.  K ) )
138137eqrdv 2420 1  |-  ( ( C  e.  ( *Met `  X )  /\  Y  C_  X
)  ->  ( Jt  Y
)  =  K )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    /\ w3a 982    = wceq 1437   E.wex 1657    e. wcel 1872   {cab 2408   A.wral 2708   E.wrex 2709   _Vcvv 3016    i^i cin 3371    C_ wss 3372   U.cuni 4155    X. cxp 4787    |` cres 4791   ` cfv 5537  (class class class)co 6242   RR*cxr 9618   RR+crp 11246   ↾t crest 15255   *Metcxmt 18891   ballcbl 18893   MetOpencmopn 18896   Topctop 19852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2402  ax-rep 4472  ax-sep 4482  ax-nul 4491  ax-pow 4538  ax-pr 4596  ax-un 6534  ax-cnex 9539  ax-resscn 9540  ax-1cn 9541  ax-icn 9542  ax-addcl 9543  ax-addrcl 9544  ax-mulcl 9545  ax-mulrcl 9546  ax-mulcom 9547  ax-addass 9548  ax-mulass 9549  ax-distr 9550  ax-i2m1 9551  ax-1ne0 9552  ax-1rid 9553  ax-rnegex 9554  ax-rrecex 9555  ax-cnre 9556  ax-pre-lttri 9557  ax-pre-lttrn 9558  ax-pre-ltadd 9559  ax-pre-mulgt0 9560  ax-pre-sup 9561
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2274  df-mo 2275  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2552  df-ne 2595  df-nel 2596  df-ral 2713  df-rex 2714  df-reu 2715  df-rmo 2716  df-rab 2717  df-v 3018  df-sbc 3236  df-csb 3332  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-pss 3388  df-nul 3698  df-if 3848  df-pw 3919  df-sn 3935  df-pr 3937  df-tp 3939  df-op 3941  df-uni 4156  df-iun 4237  df-br 4360  df-opab 4419  df-mpt 4420  df-tr 4455  df-eprel 4700  df-id 4704  df-po 4710  df-so 4711  df-fr 4748  df-we 4750  df-xp 4795  df-rel 4796  df-cnv 4797  df-co 4798  df-dm 4799  df-rn 4800  df-res 4801  df-ima 4802  df-pred 5335  df-ord 5381  df-on 5382  df-lim 5383  df-suc 5384  df-iota 5501  df-fun 5539  df-fn 5540  df-f 5541  df-f1 5542  df-fo 5543  df-f1o 5544  df-fv 5545  df-riota 6204  df-ov 6245  df-oprab 6246  df-mpt2 6247  df-om 6644  df-1st 6744  df-2nd 6745  df-wrecs 6976  df-recs 7038  df-rdg 7076  df-er 7311  df-map 7422  df-en 7518  df-dom 7519  df-sdom 7520  df-sup 7902  df-inf 7903  df-pnf 9621  df-mnf 9622  df-xr 9623  df-ltxr 9624  df-le 9625  df-sub 9806  df-neg 9807  df-div 10214  df-nn 10554  df-2 10612  df-n0 10814  df-z 10882  df-uz 11104  df-q 11209  df-rp 11247  df-xneg 11353  df-xadd 11354  df-xmul 11355  df-rest 15257  df-topgen 15278  df-psmet 18898  df-xmet 18899  df-bl 18901  df-mopn 18902  df-top 19856  df-bases 19857  df-topon 19858
This theorem is referenced by:  ressxms  21475  nrginvrcn  21629  resubmet  21755  tgioo2  21756  metdscn2  21809  metdscn2OLD  21824  divcn  21835  dfii3  21850  cncfcn  21876  cmetss  22219  minveclem4a  22307  minveclem4aOLD  22319  ftc1lem6  22928  ulmdvlem3  23292  abelth  23331  cxpcn3  23623  rlimcnp  23826  minvecolem4b  26455  minvecolem4  26457  minvecolem4bOLD  26465  minvecolem4OLD  26467  hhsscms  26865  ftc1cnnc  31917
  Copyright terms: Public domain W3C validator