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

Theorem ucncn 18268
Description: Uniform continuity implies continuity. Deduction form. Proposition 1 of [BourbakiTop1] p. II.6. (Contributed by Thierry Arnoux, 30-Nov-2017.)
Hypotheses
Ref Expression
ucncn.j  |-  J  =  ( TopOpen `  R )
ucncn.k  |-  K  =  ( TopOpen `  S )
ucncn.1  |-  ( ph  ->  R  e. UnifSp )
ucncn.2  |-  ( ph  ->  S  e. UnifSp )
ucncn.3  |-  ( ph  ->  R  e.  TopSp )
ucncn.4  |-  ( ph  ->  S  e.  TopSp )
ucncn.5  |-  ( ph  ->  F  e.  ( (UnifSt `  R ) Cnu (UnifSt `  S
) ) )
Assertion
Ref Expression
ucncn  |-  ( ph  ->  F  e.  ( J  Cn  K ) )

Proof of Theorem ucncn
Dummy variables  r 
a  s  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ucncn.5 . . . 4  |-  ( ph  ->  F  e.  ( (UnifSt `  R ) Cnu (UnifSt `  S
) ) )
2 ucncn.1 . . . . . 6  |-  ( ph  ->  R  e. UnifSp )
3 eqid 2404 . . . . . . . 8  |-  ( Base `  R )  =  (
Base `  R )
4 eqid 2404 . . . . . . . 8  |-  (UnifSt `  R )  =  (UnifSt `  R )
5 ucncn.j . . . . . . . 8  |-  J  =  ( TopOpen `  R )
63, 4, 5isusp 18244 . . . . . . 7  |-  ( R  e. UnifSp 
<->  ( (UnifSt `  R
)  e.  (UnifOn `  ( Base `  R )
)  /\  J  =  (unifTop `  (UnifSt `  R
) ) ) )
76simplbi 447 . . . . . 6  |-  ( R  e. UnifSp  ->  (UnifSt `  R )  e.  (UnifOn `  ( Base `  R ) ) )
82, 7syl 16 . . . . 5  |-  ( ph  ->  (UnifSt `  R )  e.  (UnifOn `  ( Base `  R ) ) )
9 ucncn.2 . . . . . 6  |-  ( ph  ->  S  e. UnifSp )
10 eqid 2404 . . . . . . . 8  |-  ( Base `  S )  =  (
Base `  S )
11 eqid 2404 . . . . . . . 8  |-  (UnifSt `  S )  =  (UnifSt `  S )
12 ucncn.k . . . . . . . 8  |-  K  =  ( TopOpen `  S )
1310, 11, 12isusp 18244 . . . . . . 7  |-  ( S  e. UnifSp 
<->  ( (UnifSt `  S
)  e.  (UnifOn `  ( Base `  S )
)  /\  K  =  (unifTop `  (UnifSt `  S
) ) ) )
1413simplbi 447 . . . . . 6  |-  ( S  e. UnifSp  ->  (UnifSt `  S )  e.  (UnifOn `  ( Base `  S ) ) )
159, 14syl 16 . . . . 5  |-  ( ph  ->  (UnifSt `  S )  e.  (UnifOn `  ( Base `  S ) ) )
16 isucn 18261 . . . . 5  |-  ( ( (UnifSt `  R )  e.  (UnifOn `  ( Base `  R ) )  /\  (UnifSt `  S )  e.  (UnifOn `  ( Base `  S ) ) )  ->  ( F  e.  ( (UnifSt `  R
) Cnu (UnifSt `  S )
)  <->  ( F :
( Base `  R ) --> ( Base `  S )  /\  A. s  e.  (UnifSt `  S ) E. r  e.  (UnifSt `  R ) A. x  e.  ( Base `  R ) A. z  e.  ( Base `  R ) ( x r z  ->  ( F `  x )
s ( F `  z ) ) ) ) )
178, 15, 16syl2anc 643 . . . 4  |-  ( ph  ->  ( F  e.  ( (UnifSt `  R ) Cnu (UnifSt `  S ) )  <->  ( F : ( Base `  R
) --> ( Base `  S
)  /\  A. s  e.  (UnifSt `  S ) E. r  e.  (UnifSt `  R ) A. x  e.  ( Base `  R
) A. z  e.  ( Base `  R
) ( x r z  ->  ( F `  x ) s ( F `  z ) ) ) ) )
181, 17mpbid 202 . . 3  |-  ( ph  ->  ( F : (
Base `  R ) --> ( Base `  S )  /\  A. s  e.  (UnifSt `  S ) E. r  e.  (UnifSt `  R ) A. x  e.  ( Base `  R ) A. z  e.  ( Base `  R ) ( x r z  ->  ( F `  x )
s ( F `  z ) ) ) )
1918simpld 446 . 2  |-  ( ph  ->  F : ( Base `  R ) --> ( Base `  S ) )
20 cnvimass 5183 . . . . 5  |-  ( `' F " a ) 
C_  dom  F
21 fdm 5554 . . . . . . 7  |-  ( F : ( Base `  R
) --> ( Base `  S
)  ->  dom  F  =  ( Base `  R
) )
2219, 21syl 16 . . . . . 6  |-  ( ph  ->  dom  F  =  (
Base `  R )
)
2322adantr 452 . . . . 5  |-  ( (
ph  /\  a  e.  K )  ->  dom  F  =  ( Base `  R
) )
2420, 23syl5sseq 3356 . . . 4  |-  ( (
ph  /\  a  e.  K )  ->  ( `' F " a ) 
C_  ( Base `  R
) )
25 simplll 735 . . . . . . . . 9  |-  ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F " a ) )  /\  s  e.  (UnifSt `  S )
)  ->  ph )
26 simpr 448 . . . . . . . . 9  |-  ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F " a ) )  /\  s  e.  (UnifSt `  S )
)  ->  s  e.  (UnifSt `  S ) )
2724ad2antrr 707 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F " a ) )  /\  s  e.  (UnifSt `  S )
)  ->  ( `' F " a )  C_  ( Base `  R )
)
28 simplr 732 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F " a ) )  /\  s  e.  (UnifSt `  S )
)  ->  x  e.  ( `' F " a ) )
2927, 28sseldd 3309 . . . . . . . . 9  |-  ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F " a ) )  /\  s  e.  (UnifSt `  S )
)  ->  x  e.  ( Base `  R )
)
3018simprd 450 . . . . . . . . . . . 12  |-  ( ph  ->  A. s  e.  (UnifSt `  S ) E. r  e.  (UnifSt `  R ) A. x  e.  ( Base `  R ) A. z  e.  ( Base `  R ) ( x r z  ->  ( F `  x )
s ( F `  z ) ) )
3130r19.21bi 2764 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  (UnifSt `  S ) )  ->  E. r  e.  (UnifSt `  R ) A. x  e.  ( Base `  R
) A. z  e.  ( Base `  R
) ( x r z  ->  ( F `  x ) s ( F `  z ) ) )
32 r19.12 2779 . . . . . . . . . . 11  |-  ( E. r  e.  (UnifSt `  R ) A. x  e.  ( Base `  R
) A. z  e.  ( Base `  R
) ( x r z  ->  ( F `  x ) s ( F `  z ) )  ->  A. x  e.  ( Base `  R
) E. r  e.  (UnifSt `  R ) A. z  e.  ( Base `  R ) ( x r z  -> 
( F `  x
) s ( F `
 z ) ) )
3331, 32syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  (UnifSt `  S ) )  ->  A. x  e.  (
Base `  R ) E. r  e.  (UnifSt `  R ) A. z  e.  ( Base `  R
) ( x r z  ->  ( F `  x ) s ( F `  z ) ) )
3433r19.21bi 2764 . . . . . . . . 9  |-  ( ( ( ph  /\  s  e.  (UnifSt `  S )
)  /\  x  e.  ( Base `  R )
)  ->  E. r  e.  (UnifSt `  R ) A. z  e.  ( Base `  R ) ( x r z  -> 
( F `  x
) s ( F `
 z ) ) )
3525, 26, 29, 34syl21anc 1183 . . . . . . . 8  |-  ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F " a ) )  /\  s  e.  (UnifSt `  S )
)  ->  E. r  e.  (UnifSt `  R ) A. z  e.  ( Base `  R ) ( x r z  -> 
( F `  x
) s ( F `
 z ) ) )
3635adantr 452 . . . . . . 7  |-  ( ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F " a ) )  /\  s  e.  (UnifSt `  S )
)  /\  ( s " { ( F `  x ) } ) 
C_  a )  ->  E. r  e.  (UnifSt `  R ) A. z  e.  ( Base `  R
) ( x r z  ->  ( F `  x ) s ( F `  z ) ) )
3725ad3antrrr 711 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  /\  s  e.  (UnifSt `  S
) )  /\  (
s " { ( F `  x ) } )  C_  a
)  /\  r  e.  (UnifSt `  R ) )  /\  A. z  e.  ( Base `  R
) ( x r z  ->  ( F `  x ) s ( F `  z ) ) )  ->  ph )
388ad5antr 715 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  /\  s  e.  (UnifSt `  S
) )  /\  (
s " { ( F `  x ) } )  C_  a
)  /\  r  e.  (UnifSt `  R ) )  ->  (UnifSt `  R )  e.  (UnifOn `  ( Base `  R ) ) )
39 simpr 448 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  /\  s  e.  (UnifSt `  S
) )  /\  (
s " { ( F `  x ) } )  C_  a
)  /\  r  e.  (UnifSt `  R ) )  ->  r  e.  (UnifSt `  R ) )
40 ustrel 18194 . . . . . . . . . . . 12  |-  ( ( (UnifSt `  R )  e.  (UnifOn `  ( Base `  R ) )  /\  r  e.  (UnifSt `  R
) )  ->  Rel  r )
4138, 39, 40syl2anc 643 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  /\  s  e.  (UnifSt `  S
) )  /\  (
s " { ( F `  x ) } )  C_  a
)  /\  r  e.  (UnifSt `  R ) )  ->  Rel  r )
4241adantr 452 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  /\  s  e.  (UnifSt `  S
) )  /\  (
s " { ( F `  x ) } )  C_  a
)  /\  r  e.  (UnifSt `  R ) )  /\  A. z  e.  ( Base `  R
) ( x r z  ->  ( F `  x ) s ( F `  z ) ) )  ->  Rel  r )
4337, 8syl 16 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  /\  s  e.  (UnifSt `  S
) )  /\  (
s " { ( F `  x ) } )  C_  a
)  /\  r  e.  (UnifSt `  R ) )  /\  A. z  e.  ( Base `  R
) ( x r z  ->  ( F `  x ) s ( F `  z ) ) )  ->  (UnifSt `  R )  e.  (UnifOn `  ( Base `  R
) ) )
44 simplr 732 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  /\  s  e.  (UnifSt `  S
) )  /\  (
s " { ( F `  x ) } )  C_  a
)  /\  r  e.  (UnifSt `  R ) )  /\  A. z  e.  ( Base `  R
) ( x r z  ->  ( F `  x ) s ( F `  z ) ) )  ->  r  e.  (UnifSt `  R )
)
4529ad3antrrr 711 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  /\  s  e.  (UnifSt `  S
) )  /\  (
s " { ( F `  x ) } )  C_  a
)  /\  r  e.  (UnifSt `  R ) )  /\  A. z  e.  ( Base `  R
) ( x r z  ->  ( F `  x ) s ( F `  z ) ) )  ->  x  e.  ( Base `  R
) )
46 ustimasn 18211 . . . . . . . . . . 11  |-  ( ( (UnifSt `  R )  e.  (UnifOn `  ( Base `  R ) )  /\  r  e.  (UnifSt `  R
)  /\  x  e.  ( Base `  R )
)  ->  ( r " { x } ) 
C_  ( Base `  R
) )
4743, 44, 45, 46syl3anc 1184 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  /\  s  e.  (UnifSt `  S
) )  /\  (
s " { ( F `  x ) } )  C_  a
)  /\  r  e.  (UnifSt `  R ) )  /\  A. z  e.  ( Base `  R
) ( x r z  ->  ( F `  x ) s ( F `  z ) ) )  ->  (
r " { x } )  C_  ( Base `  R ) )
48 simpr 448 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  /\  s  e.  (UnifSt `  S
) )  /\  (
s " { ( F `  x ) } )  C_  a
)  /\  r  e.  (UnifSt `  R ) )  /\  A. z  e.  ( Base `  R
) ( x r z  ->  ( F `  x ) s ( F `  z ) ) )  ->  A. z  e.  ( Base `  R
) ( x r z  ->  ( F `  x ) s ( F `  z ) ) )
49 simplr 732 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F " a ) )  /\  s  e.  (UnifSt `  S )
)  /\  ( s " { ( F `  x ) } ) 
C_  a )  /\  r  e.  (UnifSt `  R
) )  /\  z  e.  ( Base `  R
) )  /\  ( F `  x )
s ( F `  z ) )  -> 
z  e.  ( Base `  R ) )
50 simpllr 736 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  /\  s  e.  (UnifSt `  S
) )  /\  (
s " { ( F `  x ) } )  C_  a
)  /\  r  e.  (UnifSt `  R ) )  /\  ( F `  x ) s ( F `  z ) )  ->  ( s " { ( F `  x ) } ) 
C_  a )
5115ad5antr 715 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( (
ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  /\  s  e.  (UnifSt `  S
) )  /\  (
s " { ( F `  x ) } )  C_  a
)  /\  r  e.  (UnifSt `  R ) )  ->  (UnifSt `  S )  e.  (UnifOn `  ( Base `  S ) ) )
52 simpllr 736 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( (
ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  /\  s  e.  (UnifSt `  S
) )  /\  (
s " { ( F `  x ) } )  C_  a
)  /\  r  e.  (UnifSt `  R ) )  ->  s  e.  (UnifSt `  S ) )
53 ustrel 18194 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( (UnifSt `  S )  e.  (UnifOn `  ( Base `  S ) )  /\  s  e.  (UnifSt `  S
) )  ->  Rel  s )
5451, 52, 53syl2anc 643 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( (
ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  /\  s  e.  (UnifSt `  S
) )  /\  (
s " { ( F `  x ) } )  C_  a
)  /\  r  e.  (UnifSt `  R ) )  ->  Rel  s )
55 elrelimasn 5187 . . . . . . . . . . . . . . . . . . 19  |-  ( Rel  s  ->  ( ( F `  z )  e.  ( s " {
( F `  x
) } )  <->  ( F `  x ) s ( F `  z ) ) )
5654, 55syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( (
ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  /\  s  e.  (UnifSt `  S
) )  /\  (
s " { ( F `  x ) } )  C_  a
)  /\  r  e.  (UnifSt `  R ) )  ->  ( ( F `
 z )  e.  ( s " {
( F `  x
) } )  <->  ( F `  x ) s ( F `  z ) ) )
5756biimpar 472 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  /\  s  e.  (UnifSt `  S
) )  /\  (
s " { ( F `  x ) } )  C_  a
)  /\  r  e.  (UnifSt `  R ) )  /\  ( F `  x ) s ( F `  z ) )  ->  ( F `  z )  e.  ( s " { ( F `  x ) } ) )
5850, 57sseldd 3309 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  /\  s  e.  (UnifSt `  S
) )  /\  (
s " { ( F `  x ) } )  C_  a
)  /\  r  e.  (UnifSt `  R ) )  /\  ( F `  x ) s ( F `  z ) )  ->  ( F `  z )  e.  a )
5958adantlr 696 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F " a ) )  /\  s  e.  (UnifSt `  S )
)  /\  ( s " { ( F `  x ) } ) 
C_  a )  /\  r  e.  (UnifSt `  R
) )  /\  z  e.  ( Base `  R
) )  /\  ( F `  x )
s ( F `  z ) )  -> 
( F `  z
)  e.  a )
60 ffn 5550 . . . . . . . . . . . . . . . . 17  |-  ( F : ( Base `  R
) --> ( Base `  S
)  ->  F  Fn  ( Base `  R )
)
61 elpreima 5809 . . . . . . . . . . . . . . . . 17  |-  ( F  Fn  ( Base `  R
)  ->  ( z  e.  ( `' F "
a )  <->  ( z  e.  ( Base `  R
)  /\  ( F `  z )  e.  a ) ) )
6219, 60, 613syl 19 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( z  e.  ( `' F " a )  <-> 
( z  e.  (
Base `  R )  /\  ( F `  z
)  e.  a ) ) )
6362ad7antr 719 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F " a ) )  /\  s  e.  (UnifSt `  S )
)  /\  ( s " { ( F `  x ) } ) 
C_  a )  /\  r  e.  (UnifSt `  R
) )  /\  z  e.  ( Base `  R
) )  /\  ( F `  x )
s ( F `  z ) )  -> 
( z  e.  ( `' F " a )  <-> 
( z  e.  (
Base `  R )  /\  ( F `  z
)  e.  a ) ) )
6449, 59, 63mpbir2and 889 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F " a ) )  /\  s  e.  (UnifSt `  S )
)  /\  ( s " { ( F `  x ) } ) 
C_  a )  /\  r  e.  (UnifSt `  R
) )  /\  z  e.  ( Base `  R
) )  /\  ( F `  x )
s ( F `  z ) )  -> 
z  e.  ( `' F " a ) )
6564ex 424 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  /\  s  e.  (UnifSt `  S
) )  /\  (
s " { ( F `  x ) } )  C_  a
)  /\  r  e.  (UnifSt `  R ) )  /\  z  e.  (
Base `  R )
)  ->  ( ( F `  x )
s ( F `  z )  ->  z  e.  ( `' F "
a ) ) )
6665ralrimiva 2749 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  /\  s  e.  (UnifSt `  S
) )  /\  (
s " { ( F `  x ) } )  C_  a
)  /\  r  e.  (UnifSt `  R ) )  ->  A. z  e.  (
Base `  R )
( ( F `  x ) s ( F `  z )  ->  z  e.  ( `' F " a ) ) )
6766adantr 452 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  /\  s  e.  (UnifSt `  S
) )  /\  (
s " { ( F `  x ) } )  C_  a
)  /\  r  e.  (UnifSt `  R ) )  /\  A. z  e.  ( Base `  R
) ( x r z  ->  ( F `  x ) s ( F `  z ) ) )  ->  A. z  e.  ( Base `  R
) ( ( F `
 x ) s ( F `  z
)  ->  z  e.  ( `' F " a ) ) )
68 r19.26 2798 . . . . . . . . . . . 12  |-  ( A. z  e.  ( Base `  R ) ( ( x r z  -> 
( F `  x
) s ( F `
 z ) )  /\  ( ( F `
 x ) s ( F `  z
)  ->  z  e.  ( `' F " a ) ) )  <->  ( A. z  e.  ( Base `  R ) ( x r z  ->  ( F `  x )
s ( F `  z ) )  /\  A. z  e.  ( Base `  R ) ( ( F `  x ) s ( F `  z )  ->  z  e.  ( `' F "
a ) ) ) )
69 pm3.33 569 . . . . . . . . . . . . 13  |-  ( ( ( x r z  ->  ( F `  x ) s ( F `  z ) )  /\  ( ( F `  x ) s ( F `  z )  ->  z  e.  ( `' F "
a ) ) )  ->  ( x r z  ->  z  e.  ( `' F " a ) ) )
7069ralimi 2741 . . . . . . . . . . . 12  |-  ( A. z  e.  ( Base `  R ) ( ( x r z  -> 
( F `  x
) s ( F `
 z ) )  /\  ( ( F `
 x ) s ( F `  z
)  ->  z  e.  ( `' F " a ) ) )  ->  A. z  e.  ( Base `  R
) ( x r z  ->  z  e.  ( `' F " a ) ) )
7168, 70sylbir 205 . . . . . . . . . . 11  |-  ( ( A. z  e.  (
Base `  R )
( x r z  ->  ( F `  x ) s ( F `  z ) )  /\  A. z  e.  ( Base `  R
) ( ( F `
 x ) s ( F `  z
)  ->  z  e.  ( `' F " a ) ) )  ->  A. z  e.  ( Base `  R
) ( x r z  ->  z  e.  ( `' F " a ) ) )
7248, 67, 71syl2anc 643 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  /\  s  e.  (UnifSt `  S
) )  /\  (
s " { ( F `  x ) } )  C_  a
)  /\  r  e.  (UnifSt `  R ) )  /\  A. z  e.  ( Base `  R
) ( x r z  ->  ( F `  x ) s ( F `  z ) ) )  ->  A. z  e.  ( Base `  R
) ( x r z  ->  z  e.  ( `' F " a ) ) )
73 simpl2l 1010 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ( Rel  r  /\  (
r " { x } )  C_  ( Base `  R ) )  /\  A. z  e.  ( Base `  R
) ( x r z  ->  z  e.  ( `' F " a ) ) )  /\  y  e.  ( r " {
x } ) )  ->  Rel  r )
74 simpr 448 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ( Rel  r  /\  (
r " { x } )  C_  ( Base `  R ) )  /\  A. z  e.  ( Base `  R
) ( x r z  ->  z  e.  ( `' F " a ) ) )  /\  y  e.  ( r " {
x } ) )  ->  y  e.  ( r " { x } ) )
75 elrelimasn 5187 . . . . . . . . . . . . . . 15  |-  ( Rel  r  ->  ( y  e.  ( r " {
x } )  <->  x r
y ) )
7675biimpa 471 . . . . . . . . . . . . . 14  |-  ( ( Rel  r  /\  y  e.  ( r " {
x } ) )  ->  x r y )
7773, 74, 76syl2anc 643 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( Rel  r  /\  (
r " { x } )  C_  ( Base `  R ) )  /\  A. z  e.  ( Base `  R
) ( x r z  ->  z  e.  ( `' F " a ) ) )  /\  y  e.  ( r " {
x } ) )  ->  x r y )
78 simpl2r 1011 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  ( Rel  r  /\  (
r " { x } )  C_  ( Base `  R ) )  /\  A. z  e.  ( Base `  R
) ( x r z  ->  z  e.  ( `' F " a ) ) )  /\  y  e.  ( r " {
x } ) )  ->  ( r " { x } ) 
C_  ( Base `  R
) )
7978, 74sseldd 3309 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ( Rel  r  /\  (
r " { x } )  C_  ( Base `  R ) )  /\  A. z  e.  ( Base `  R
) ( x r z  ->  z  e.  ( `' F " a ) ) )  /\  y  e.  ( r " {
x } ) )  ->  y  e.  (
Base `  R )
)
80 simpl3 962 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ( Rel  r  /\  (
r " { x } )  C_  ( Base `  R ) )  /\  A. z  e.  ( Base `  R
) ( x r z  ->  z  e.  ( `' F " a ) ) )  /\  y  e.  ( r " {
x } ) )  ->  A. z  e.  (
Base `  R )
( x r z  ->  z  e.  ( `' F " a ) ) )
81 breq2 4176 . . . . . . . . . . . . . . . 16  |-  ( z  =  y  ->  (
x r z  <->  x r
y ) )
82 eleq1 2464 . . . . . . . . . . . . . . . 16  |-  ( z  =  y  ->  (
z  e.  ( `' F " a )  <-> 
y  e.  ( `' F " a ) ) )
8381, 82imbi12d 312 . . . . . . . . . . . . . . 15  |-  ( z  =  y  ->  (
( x r z  ->  z  e.  ( `' F " a ) )  <->  ( x r y  ->  y  e.  ( `' F " a ) ) ) )
8483rspcv 3008 . . . . . . . . . . . . . 14  |-  ( y  e.  ( Base `  R
)  ->  ( A. z  e.  ( Base `  R ) ( x r z  ->  z  e.  ( `' F "
a ) )  -> 
( x r y  ->  y  e.  ( `' F " a ) ) ) )
8579, 80, 84sylc 58 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( Rel  r  /\  (
r " { x } )  C_  ( Base `  R ) )  /\  A. z  e.  ( Base `  R
) ( x r z  ->  z  e.  ( `' F " a ) ) )  /\  y  e.  ( r " {
x } ) )  ->  ( x r y  ->  y  e.  ( `' F " a ) ) )
8677, 85mpd 15 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ( Rel  r  /\  (
r " { x } )  C_  ( Base `  R ) )  /\  A. z  e.  ( Base `  R
) ( x r z  ->  z  e.  ( `' F " a ) ) )  /\  y  e.  ( r " {
x } ) )  ->  y  e.  ( `' F " a ) )
8786ex 424 . . . . . . . . . . 11  |-  ( (
ph  /\  ( Rel  r  /\  ( r " { x } ) 
C_  ( Base `  R
) )  /\  A. z  e.  ( Base `  R ) ( x r z  ->  z  e.  ( `' F "
a ) ) )  ->  ( y  e.  ( r " {
x } )  -> 
y  e.  ( `' F " a ) ) )
8887ssrdv 3314 . . . . . . . . . 10  |-  ( (
ph  /\  ( Rel  r  /\  ( r " { x } ) 
C_  ( Base `  R
) )  /\  A. z  e.  ( Base `  R ) ( x r z  ->  z  e.  ( `' F "
a ) ) )  ->  ( r " { x } ) 
C_  ( `' F " a ) )
8937, 42, 47, 72, 88syl121anc 1189 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  /\  s  e.  (UnifSt `  S
) )  /\  (
s " { ( F `  x ) } )  C_  a
)  /\  r  e.  (UnifSt `  R ) )  /\  A. z  e.  ( Base `  R
) ( x r z  ->  ( F `  x ) s ( F `  z ) ) )  ->  (
r " { x } )  C_  ( `' F " a ) )
9089ex 424 . . . . . . . 8  |-  ( ( ( ( ( (
ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  /\  s  e.  (UnifSt `  S
) )  /\  (
s " { ( F `  x ) } )  C_  a
)  /\  r  e.  (UnifSt `  R ) )  ->  ( A. z  e.  ( Base `  R
) ( x r z  ->  ( F `  x ) s ( F `  z ) )  ->  ( r " { x } ) 
C_  ( `' F " a ) ) )
9190reximdva 2778 . . . . . . 7  |-  ( ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F " a ) )  /\  s  e.  (UnifSt `  S )
)  /\  ( s " { ( F `  x ) } ) 
C_  a )  -> 
( E. r  e.  (UnifSt `  R ) A. z  e.  ( Base `  R ) ( x r z  -> 
( F `  x
) s ( F `
 z ) )  ->  E. r  e.  (UnifSt `  R ) ( r
" { x }
)  C_  ( `' F " a ) ) )
9236, 91mpd 15 . . . . . 6  |-  ( ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F " a ) )  /\  s  e.  (UnifSt `  S )
)  /\  ( s " { ( F `  x ) } ) 
C_  a )  ->  E. r  e.  (UnifSt `  R ) ( r
" { x }
)  C_  ( `' F " a ) )
93 elpreima 5809 . . . . . . . . . . 11  |-  ( F  Fn  ( Base `  R
)  ->  ( x  e.  ( `' F "
a )  <->  ( x  e.  ( Base `  R
)  /\  ( F `  x )  e.  a ) ) )
9419, 60, 933syl 19 . . . . . . . . . 10  |-  ( ph  ->  ( x  e.  ( `' F " a )  <-> 
( x  e.  (
Base `  R )  /\  ( F `  x
)  e.  a ) ) )
9594adantr 452 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  K )  ->  (
x  e.  ( `' F " a )  <-> 
( x  e.  (
Base `  R )  /\  ( F `  x
)  e.  a ) ) )
9695biimpa 471 . . . . . . . 8  |-  ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  -> 
( x  e.  (
Base `  R )  /\  ( F `  x
)  e.  a ) )
9796simprd 450 . . . . . . 7  |-  ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  -> 
( F `  x
)  e.  a )
98 simpr 448 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  K )  ->  a  e.  K )
9913simprbi 451 . . . . . . . . . . . . 13  |-  ( S  e. UnifSp  ->  K  =  (unifTop `  (UnifSt `  S )
) )
1009, 99syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  K  =  (unifTop `  (UnifSt `  S ) ) )
101100adantr 452 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  K )  ->  K  =  (unifTop `  (UnifSt `  S
) ) )
10298, 101eleqtrd 2480 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  K )  ->  a  e.  (unifTop `  (UnifSt `  S
) ) )
103 elutop 18216 . . . . . . . . . . . 12  |-  ( (UnifSt `  S )  e.  (UnifOn `  ( Base `  S
) )  ->  (
a  e.  (unifTop `  (UnifSt `  S ) )  <->  ( a  C_  ( Base `  S
)  /\  A. y  e.  a  E. s  e.  (UnifSt `  S )
( s " {
y } )  C_  a ) ) )
10415, 103syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( a  e.  (unifTop `  (UnifSt `  S )
)  <->  ( a  C_  ( Base `  S )  /\  A. y  e.  a  E. s  e.  (UnifSt `  S ) ( s
" { y } )  C_  a )
) )
105104adantr 452 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  K )  ->  (
a  e.  (unifTop `  (UnifSt `  S ) )  <->  ( a  C_  ( Base `  S
)  /\  A. y  e.  a  E. s  e.  (UnifSt `  S )
( s " {
y } )  C_  a ) ) )
106102, 105mpbid 202 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  K )  ->  (
a  C_  ( Base `  S )  /\  A. y  e.  a  E. s  e.  (UnifSt `  S
) ( s " { y } ) 
C_  a ) )
107106simprd 450 . . . . . . . 8  |-  ( (
ph  /\  a  e.  K )  ->  A. y  e.  a  E. s  e.  (UnifSt `  S )
( s " {
y } )  C_  a )
108107adantr 452 . . . . . . 7  |-  ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  ->  A. y  e.  a  E. s  e.  (UnifSt `  S ) ( s
" { y } )  C_  a )
109 sneq 3785 . . . . . . . . . . 11  |-  ( y  =  ( F `  x )  ->  { y }  =  { ( F `  x ) } )
110109imaeq2d 5162 . . . . . . . . . 10  |-  ( y  =  ( F `  x )  ->  (
s " { y } )  =  ( s " { ( F `  x ) } ) )
111110sseq1d 3335 . . . . . . . . 9  |-  ( y  =  ( F `  x )  ->  (
( s " {
y } )  C_  a 
<->  ( s " {
( F `  x
) } )  C_  a ) )
112111rexbidv 2687 . . . . . . . 8  |-  ( y  =  ( F `  x )  ->  ( E. s  e.  (UnifSt `  S ) ( s
" { y } )  C_  a  <->  E. s  e.  (UnifSt `  S )
( s " {
( F `  x
) } )  C_  a ) )
113112rspcv 3008 . . . . . . 7  |-  ( ( F `  x )  e.  a  ->  ( A. y  e.  a  E. s  e.  (UnifSt `  S ) ( s
" { y } )  C_  a  ->  E. s  e.  (UnifSt `  S ) ( s
" { ( F `
 x ) } )  C_  a )
)
11497, 108, 113sylc 58 . . . . . 6  |-  ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  ->  E. s  e.  (UnifSt `  S ) ( s
" { ( F `
 x ) } )  C_  a )
11592, 114r19.29a 2810 . . . . 5  |-  ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  ->  E. r  e.  (UnifSt `  R ) ( r
" { x }
)  C_  ( `' F " a ) )
116115ralrimiva 2749 . . . 4  |-  ( (
ph  /\  a  e.  K )  ->  A. x  e.  ( `' F "
a ) E. r  e.  (UnifSt `  R )
( r " {
x } )  C_  ( `' F " a ) )
1176simprbi 451 . . . . . . . 8  |-  ( R  e. UnifSp  ->  J  =  (unifTop `  (UnifSt `  R )
) )
1182, 117syl 16 . . . . . . 7  |-  ( ph  ->  J  =  (unifTop `  (UnifSt `  R ) ) )
119118adantr 452 . . . . . 6  |-  ( (
ph  /\  a  e.  K )  ->  J  =  (unifTop `  (UnifSt `  R
) ) )
120119eleq2d 2471 . . . . 5  |-  ( (
ph  /\  a  e.  K )  ->  (
( `' F "
a )  e.  J  <->  ( `' F " a )  e.  (unifTop `  (UnifSt `  R ) ) ) )
121 elutop 18216 . . . . . . 7  |-  ( (UnifSt `  R )  e.  (UnifOn `  ( Base `  R
) )  ->  (
( `' F "
a )  e.  (unifTop `  (UnifSt `  R )
)  <->  ( ( `' F " a ) 
C_  ( Base `  R
)  /\  A. x  e.  ( `' F "
a ) E. r  e.  (UnifSt `  R )
( r " {
x } )  C_  ( `' F " a ) ) ) )
1228, 121syl 16 . . . . . 6  |-  ( ph  ->  ( ( `' F " a )  e.  (unifTop `  (UnifSt `  R )
)  <->  ( ( `' F " a ) 
C_  ( Base `  R
)  /\  A. x  e.  ( `' F "
a ) E. r  e.  (UnifSt `  R )
( r " {
x } )  C_  ( `' F " a ) ) ) )
123122adantr 452 . . . . 5  |-  ( (
ph  /\  a  e.  K )  ->  (
( `' F "
a )  e.  (unifTop `  (UnifSt `  R )
)  <->  ( ( `' F " a ) 
C_  ( Base `  R
)  /\  A. x  e.  ( `' F "
a ) E. r  e.  (UnifSt `  R )
( r " {
x } )  C_  ( `' F " a ) ) ) )
124120, 123bitrd 245 . . . 4  |-  ( (
ph  /\  a  e.  K )  ->  (
( `' F "
a )  e.  J  <->  ( ( `' F "
a )  C_  ( Base `  R )  /\  A. x  e.  ( `' F " a ) E. r  e.  (UnifSt `  R ) ( r
" { x }
)  C_  ( `' F " a ) ) ) )
12524, 116, 124mpbir2and 889 . . 3  |-  ( (
ph  /\  a  e.  K )  ->  ( `' F " a )  e.  J )
126125ralrimiva 2749 . 2  |-  ( ph  ->  A. a  e.  K  ( `' F " a )  e.  J )
127 ucncn.3 . . . 4  |-  ( ph  ->  R  e.  TopSp )
1283, 5istps 16956 . . . 4  |-  ( R  e.  TopSp 
<->  J  e.  (TopOn `  ( Base `  R )
) )
129127, 128sylib 189 . . 3  |-  ( ph  ->  J  e.  (TopOn `  ( Base `  R )
) )
130 ucncn.4 . . . 4  |-  ( ph  ->  S  e.  TopSp )
13110, 12istps 16956 . . . 4  |-  ( S  e.  TopSp 
<->  K  e.  (TopOn `  ( Base `  S )
) )
132130, 131sylib 189 . . 3  |-  ( ph  ->  K  e.  (TopOn `  ( Base `  S )
) )
133 iscn 17253 . . 3  |-  ( ( J  e.  (TopOn `  ( Base `  R )
)  /\  K  e.  (TopOn `  ( Base `  S
) ) )  -> 
( F  e.  ( J  Cn  K )  <-> 
( F : (
Base `  R ) --> ( Base `  S )  /\  A. a  e.  K  ( `' F " a )  e.  J ) ) )
134129, 132, 133syl2anc 643 . 2  |-  ( ph  ->  ( F  e.  ( J  Cn  K )  <-> 
( F : (
Base `  R ) --> ( Base `  S )  /\  A. a  e.  K  ( `' F " a )  e.  J ) ) )
13519, 126, 134mpbir2and 889 1  |-  ( ph  ->  F  e.  ( J  Cn  K ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    /\ w3a 936    = wceq 1649    e. wcel 1721   A.wral 2666   E.wrex 2667    C_ wss 3280   {csn 3774   class class class wbr 4172   `'ccnv 4836   dom cdm 4837   "cima 4840   Rel wrel 4842    Fn wfn 5408   -->wf 5409   ` cfv 5413  (class class class)co 6040   Basecbs 13424   TopOpenctopn 13604  TopOnctopon 16914   TopSpctps 16916    Cn ccn 17242  UnifOncust 18182  unifTopcutop 18213  UnifStcuss 18236  UnifSpcusp 18237   Cnucucn 18258
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-map 6979  df-top 16918  df-topon 16921  df-topsp 16922  df-cn 17245  df-ust 18183  df-utop 18214  df-usp 18240  df-ucn 18259
  Copyright terms: Public domain W3C validator