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

Theorem ucncn 19865
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 2443 . . . . . . . 8  |-  ( Base `  R )  =  (
Base `  R )
4 eqid 2443 . . . . . . . 8  |-  (UnifSt `  R )  =  (UnifSt `  R )
5 ucncn.j . . . . . . . 8  |-  J  =  ( TopOpen `  R )
63, 4, 5isusp 19841 . . . . . . 7  |-  ( R  e. UnifSp 
<->  ( (UnifSt `  R
)  e.  (UnifOn `  ( Base `  R )
)  /\  J  =  (unifTop `  (UnifSt `  R
) ) ) )
76simplbi 460 . . . . . 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 2443 . . . . . . . 8  |-  ( Base `  S )  =  (
Base `  S )
11 eqid 2443 . . . . . . . 8  |-  (UnifSt `  S )  =  (UnifSt `  S )
12 ucncn.k . . . . . . . 8  |-  K  =  ( TopOpen `  S )
1310, 11, 12isusp 19841 . . . . . . 7  |-  ( S  e. UnifSp 
<->  ( (UnifSt `  S
)  e.  (UnifOn `  ( Base `  S )
)  /\  K  =  (unifTop `  (UnifSt `  S
) ) ) )
1413simplbi 460 . . . . . 6  |-  ( S  e. UnifSp  ->  (UnifSt `  S )  e.  (UnifOn `  ( Base `  S ) ) )
159, 14syl 16 . . . . 5  |-  ( ph  ->  (UnifSt `  S )  e.  (UnifOn `  ( Base `  S ) ) )
16 isucn 19858 . . . . 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 661 . . . 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 210 . . 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 459 . 2  |-  ( ph  ->  F : ( Base `  R ) --> ( Base `  S ) )
20 cnvimass 5194 . . . . 5  |-  ( `' F " a ) 
C_  dom  F
21 fdm 5568 . . . . . . 7  |-  ( F : ( Base `  R
) --> ( Base `  S
)  ->  dom  F  =  ( Base `  R
) )
2219, 21syl 16 . . . . . 6  |-  ( ph  ->  dom  F  =  (
Base `  R )
)
2322adantr 465 . . . . 5  |-  ( (
ph  /\  a  e.  K )  ->  dom  F  =  ( Base `  R
) )
2420, 23syl5sseq 3409 . . . 4  |-  ( (
ph  /\  a  e.  K )  ->  ( `' F " a ) 
C_  ( Base `  R
) )
25 simplll 757 . . . . . . . . 9  |-  ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F " a ) )  /\  s  e.  (UnifSt `  S )
)  ->  ph )
26 simpr 461 . . . . . . . . 9  |-  ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F " a ) )  /\  s  e.  (UnifSt `  S )
)  ->  s  e.  (UnifSt `  S ) )
2724ad2antrr 725 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F " a ) )  /\  s  e.  (UnifSt `  S )
)  ->  ( `' F " a )  C_  ( Base `  R )
)
28 simplr 754 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F " a ) )  /\  s  e.  (UnifSt `  S )
)  ->  x  e.  ( `' F " a ) )
2927, 28sseldd 3362 . . . . . . . . 9  |-  ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F " a ) )  /\  s  e.  (UnifSt `  S )
)  ->  x  e.  ( Base `  R )
)
3018simprd 463 . . . . . . . . . . . 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 2819 . . . . . . . . . . 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 2835 . . . . . . . . . . 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 2819 . . . . . . . . 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 1217 . . . . . . . 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 465 . . . . . . 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 729 . . . . . . . . . 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 733 . . . . . . . . . . . 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 461 . . . . . . . . . . . 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 19791 . . . . . . . . . . . 12  |-  ( ( (UnifSt `  R )  e.  (UnifOn `  ( Base `  R ) )  /\  r  e.  (UnifSt `  R
) )  ->  Rel  r )
4138, 39, 40syl2anc 661 . . . . . . . . . . 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 465 . . . . . . . . . 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 754 . . . . . . . . . . 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 729 . . . . . . . . . . 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 19808 . . . . . . . . . . 11  |-  ( ( (UnifSt `  R )  e.  (UnifOn `  ( Base `  R ) )  /\  r  e.  (UnifSt `  R
)  /\  x  e.  ( Base `  R )
)  ->  ( r " { x } ) 
C_  ( Base `  R
) )
4743, 44, 45, 46syl3anc 1218 . . . . . . . . . 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 461 . . . . . . . . . . 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 754 . . . . . . . . . . . . . . 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 758 . . . . . . . . . . . . . . . . 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 733 . . . . . . . . . . . . . . . . . . . 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 758 . . . . . . . . . . . . . . . . . . . 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 19791 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( (UnifSt `  S )  e.  (UnifOn `  ( Base `  S ) )  /\  s  e.  (UnifSt `  S
) )  ->  Rel  s )
5451, 52, 53syl2anc 661 . . . . . . . . . . . . . . . . . . 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 5198 . . . . . . . . . . . . . . . . . . 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 485 . . . . . . . . . . . . . . . . 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 3362 . . . . . . . . . . . . . . . 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 714 . . . . . . . . . . . . . . 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 5564 . . . . . . . . . . . . . . . . 17  |-  ( F : ( Base `  R
) --> ( Base `  S
)  ->  F  Fn  ( Base `  R )
)
61 elpreima 5828 . . . . . . . . . . . . . . . . 17  |-  ( F  Fn  ( Base `  R
)  ->  ( z  e.  ( `' F "
a )  <->  ( z  e.  ( Base `  R
)  /\  ( F `  z )  e.  a ) ) )
6219, 60, 613syl 20 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( z  e.  ( `' F " a )  <-> 
( z  e.  (
Base `  R )  /\  ( F `  z
)  e.  a ) ) )
6362ad7antr 737 . . . . . . . . . . . . . . 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 913 . . . . . . . . . . . . . 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 434 . . . . . . . . . . . . 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 2804 . . . . . . . . . . . 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 465 . . . . . . . . . . 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 2854 . . . . . . . . . . . 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 585 . . . . . . . . . . . . 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 2796 . . . . . . . . . . . 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 213 . . . . . . . . . . 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 661 . . . . . . . . . 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 1041 . . . . . . . . . . . . . 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 461 . . . . . . . . . . . . . 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 5198 . . . . . . . . . . . . . . 15  |-  ( Rel  r  ->  ( y  e.  ( r " {
x } )  <->  x r
y ) )
7675biimpa 484 . . . . . . . . . . . . . 14  |-  ( ( Rel  r  /\  y  e.  ( r " {
x } ) )  ->  x r y )
7773, 74, 76syl2anc 661 . . . . . . . . . . . . 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 1042 . . . . . . . . . . . . . . 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 3362 . . . . . . . . . . . . . 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 993 . . . . . . . . . . . . . 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 4301 . . . . . . . . . . . . . . . 16  |-  ( z  =  y  ->  (
x r z  <->  x r
y ) )
82 eleq1 2503 . . . . . . . . . . . . . . . 16  |-  ( z  =  y  ->  (
z  e.  ( `' F " a )  <-> 
y  e.  ( `' F " a ) ) )
8381, 82imbi12d 320 . . . . . . . . . . . . . . 15  |-  ( z  =  y  ->  (
( x r z  ->  z  e.  ( `' F " a ) )  <->  ( x r y  ->  y  e.  ( `' F " a ) ) ) )
8483rspcv 3074 . . . . . . . . . . . . . 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 60 . . . . . . . . . . . . 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 434 . . . . . . . . . . 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 3367 . . . . . . . . . 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 1223 . . . . . . . . 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 434 . . . . . . . 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 2833 . . . . . . 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 5828 . . . . . . . . . . 11  |-  ( F  Fn  ( Base `  R
)  ->  ( x  e.  ( `' F "
a )  <->  ( x  e.  ( Base `  R
)  /\  ( F `  x )  e.  a ) ) )
9419, 60, 933syl 20 . . . . . . . . . 10  |-  ( ph  ->  ( x  e.  ( `' F " a )  <-> 
( x  e.  (
Base `  R )  /\  ( F `  x
)  e.  a ) ) )
9594adantr 465 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  K )  ->  (
x  e.  ( `' F " a )  <-> 
( x  e.  (
Base `  R )  /\  ( F `  x
)  e.  a ) ) )
9695biimpa 484 . . . . . . . 8  |-  ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  -> 
( x  e.  (
Base `  R )  /\  ( F `  x
)  e.  a ) )
9796simprd 463 . . . . . . 7  |-  ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  -> 
( F `  x
)  e.  a )
98 simpr 461 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  K )  ->  a  e.  K )
9913simprbi 464 . . . . . . . . . . . . 13  |-  ( S  e. UnifSp  ->  K  =  (unifTop `  (UnifSt `  S )
) )
1009, 99syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  K  =  (unifTop `  (UnifSt `  S ) ) )
101100adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  K )  ->  K  =  (unifTop `  (UnifSt `  S
) ) )
10298, 101eleqtrd 2519 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  K )  ->  a  e.  (unifTop `  (UnifSt `  S
) ) )
103 elutop 19813 . . . . . . . . . . . 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 465 . . . . . . . . . 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 210 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  K )  ->  (
a  C_  ( Base `  S )  /\  A. y  e.  a  E. s  e.  (UnifSt `  S
) ( s " { y } ) 
C_  a ) )
107106simprd 463 . . . . . . . 8  |-  ( (
ph  /\  a  e.  K )  ->  A. y  e.  a  E. s  e.  (UnifSt `  S )
( s " {
y } )  C_  a )
108107adantr 465 . . . . . . 7  |-  ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  ->  A. y  e.  a  E. s  e.  (UnifSt `  S ) ( s
" { y } )  C_  a )
109 sneq 3892 . . . . . . . . . . 11  |-  ( y  =  ( F `  x )  ->  { y }  =  { ( F `  x ) } )
110109imaeq2d 5174 . . . . . . . . . 10  |-  ( y  =  ( F `  x )  ->  (
s " { y } )  =  ( s " { ( F `  x ) } ) )
111110sseq1d 3388 . . . . . . . . 9  |-  ( y  =  ( F `  x )  ->  (
( s " {
y } )  C_  a 
<->  ( s " {
( F `  x
) } )  C_  a ) )
112111rexbidv 2741 . . . . . . . 8  |-  ( y  =  ( F `  x )  ->  ( E. s  e.  (UnifSt `  S ) ( s
" { y } )  C_  a  <->  E. s  e.  (UnifSt `  S )
( s " {
( F `  x
) } )  C_  a ) )
113112rspcv 3074 . . . . . . 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 60 . . . . . 6  |-  ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  ->  E. s  e.  (UnifSt `  S ) ( s
" { ( F `
 x ) } )  C_  a )
11592, 114r19.29a 2867 . . . . 5  |-  ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  ->  E. r  e.  (UnifSt `  R ) ( r
" { x }
)  C_  ( `' F " a ) )
116115ralrimiva 2804 . . . 4  |-  ( (
ph  /\  a  e.  K )  ->  A. x  e.  ( `' F "
a ) E. r  e.  (UnifSt `  R )
( r " {
x } )  C_  ( `' F " a ) )
1176simprbi 464 . . . . . . . 8  |-  ( R  e. UnifSp  ->  J  =  (unifTop `  (UnifSt `  R )
) )
1182, 117syl 16 . . . . . . 7  |-  ( ph  ->  J  =  (unifTop `  (UnifSt `  R ) ) )
119118adantr 465 . . . . . 6  |-  ( (
ph  /\  a  e.  K )  ->  J  =  (unifTop `  (UnifSt `  R
) ) )
120119eleq2d 2510 . . . . 5  |-  ( (
ph  /\  a  e.  K )  ->  (
( `' F "
a )  e.  J  <->  ( `' F " a )  e.  (unifTop `  (UnifSt `  R ) ) ) )
121 elutop 19813 . . . . . . 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 465 . . . . 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 253 . . . 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 913 . . 3  |-  ( (
ph  /\  a  e.  K )  ->  ( `' F " a )  e.  J )
126125ralrimiva 2804 . 2  |-  ( ph  ->  A. a  e.  K  ( `' F " a )  e.  J )
127 ucncn.3 . . . 4  |-  ( ph  ->  R  e.  TopSp )
1283, 5istps 18546 . . . 4  |-  ( R  e.  TopSp 
<->  J  e.  (TopOn `  ( Base `  R )
) )
129127, 128sylib 196 . . 3  |-  ( ph  ->  J  e.  (TopOn `  ( Base `  R )
) )
130 ucncn.4 . . . 4  |-  ( ph  ->  S  e.  TopSp )
13110, 12istps 18546 . . . 4  |-  ( S  e.  TopSp 
<->  K  e.  (TopOn `  ( Base `  S )
) )
132130, 131sylib 196 . . 3  |-  ( ph  ->  K  e.  (TopOn `  ( Base `  S )
) )
133 iscn 18844 . . 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 661 . 2  |-  ( ph  ->  ( F  e.  ( J  Cn  K )  <-> 
( F : (
Base `  R ) --> ( Base `  S )  /\  A. a  e.  K  ( `' F " a )  e.  J ) ) )
13519, 126, 134mpbir2and 913 1  |-  ( ph  ->  F  e.  ( J  Cn  K ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 965    = wceq 1369    e. wcel 1756   A.wral 2720   E.wrex 2721    C_ wss 3333   {csn 3882   class class class wbr 4297   `'ccnv 4844   dom cdm 4845   "cima 4848   Rel wrel 4850    Fn wfn 5418   -->wf 5419   ` cfv 5423  (class class class)co 6096   Basecbs 14179   TopOpenctopn 14365  TopOnctopon 18504   TopSpctps 18506    Cn ccn 18833  UnifOncust 19779  unifTopcutop 19810  UnifStcuss 19833  UnifSpcusp 19834   Cnucucn 19855
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4418  ax-nul 4426  ax-pow 4475  ax-pr 4536  ax-un 6377
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ne 2613  df-ral 2725  df-rex 2726  df-rab 2729  df-v 2979  df-sbc 3192  df-csb 3294  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-nul 3643  df-if 3797  df-pw 3867  df-sn 3883  df-pr 3885  df-op 3889  df-uni 4097  df-br 4298  df-opab 4356  df-mpt 4357  df-id 4641  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5386  df-fun 5425  df-fn 5426  df-f 5427  df-fv 5431  df-ov 6099  df-oprab 6100  df-mpt2 6101  df-map 7221  df-top 18508  df-topon 18511  df-topsp 18512  df-cn 18836  df-ust 19780  df-utop 19811  df-usp 19837  df-ucn 19856
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator