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

Theorem ucncn 21349
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 2462 . . . . . . . 8  |-  ( Base `  R )  =  (
Base `  R )
4 eqid 2462 . . . . . . . 8  |-  (UnifSt `  R )  =  (UnifSt `  R )
5 ucncn.j . . . . . . . 8  |-  J  =  ( TopOpen `  R )
63, 4, 5isusp 21325 . . . . . . 7  |-  ( R  e. UnifSp 
<->  ( (UnifSt `  R
)  e.  (UnifOn `  ( Base `  R )
)  /\  J  =  (unifTop `  (UnifSt `  R
) ) ) )
76simplbi 466 . . . . . 6  |-  ( R  e. UnifSp  ->  (UnifSt `  R )  e.  (UnifOn `  ( Base `  R ) ) )
82, 7syl 17 . . . . 5  |-  ( ph  ->  (UnifSt `  R )  e.  (UnifOn `  ( Base `  R ) ) )
9 ucncn.2 . . . . . 6  |-  ( ph  ->  S  e. UnifSp )
10 eqid 2462 . . . . . . . 8  |-  ( Base `  S )  =  (
Base `  S )
11 eqid 2462 . . . . . . . 8  |-  (UnifSt `  S )  =  (UnifSt `  S )
12 ucncn.k . . . . . . . 8  |-  K  =  ( TopOpen `  S )
1310, 11, 12isusp 21325 . . . . . . 7  |-  ( S  e. UnifSp 
<->  ( (UnifSt `  S
)  e.  (UnifOn `  ( Base `  S )
)  /\  K  =  (unifTop `  (UnifSt `  S
) ) ) )
1413simplbi 466 . . . . . 6  |-  ( S  e. UnifSp  ->  (UnifSt `  S )  e.  (UnifOn `  ( Base `  S ) ) )
159, 14syl 17 . . . . 5  |-  ( ph  ->  (UnifSt `  S )  e.  (UnifOn `  ( Base `  S ) ) )
16 isucn 21342 . . . . 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 671 . . . 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 215 . . 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 465 . 2  |-  ( ph  ->  F : ( Base `  R ) --> ( Base `  S ) )
20 cnvimass 5207 . . . . 5  |-  ( `' F " a ) 
C_  dom  F
21 fdm 5756 . . . . . . 7  |-  ( F : ( Base `  R
) --> ( Base `  S
)  ->  dom  F  =  ( Base `  R
) )
2219, 21syl 17 . . . . . 6  |-  ( ph  ->  dom  F  =  (
Base `  R )
)
2322adantr 471 . . . . 5  |-  ( (
ph  /\  a  e.  K )  ->  dom  F  =  ( Base `  R
) )
2420, 23syl5sseq 3492 . . . 4  |-  ( (
ph  /\  a  e.  K )  ->  ( `' F " a ) 
C_  ( Base `  R
) )
25 simplll 773 . . . . . . . . 9  |-  ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F " a ) )  /\  s  e.  (UnifSt `  S )
)  ->  ph )
26 simpr 467 . . . . . . . . 9  |-  ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F " a ) )  /\  s  e.  (UnifSt `  S )
)  ->  s  e.  (UnifSt `  S ) )
2724ad2antrr 737 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F " a ) )  /\  s  e.  (UnifSt `  S )
)  ->  ( `' F " a )  C_  ( Base `  R )
)
28 simplr 767 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F " a ) )  /\  s  e.  (UnifSt `  S )
)  ->  x  e.  ( `' F " a ) )
2927, 28sseldd 3445 . . . . . . . . 9  |-  ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F " a ) )  /\  s  e.  (UnifSt `  S )
)  ->  x  e.  ( Base `  R )
)
3018simprd 469 . . . . . . . . . . . 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 2769 . . . . . . . . . . 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 2928 . . . . . . . . . . 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 17 . . . . . . . . . 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 2769 . . . . . . . . 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 1275 . . . . . . . 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 471 . . . . . . 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 741 . . . . . . . . . 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 745 . . . . . . . . . . . 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 467 . . . . . . . . . . . 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 21275 . . . . . . . . . . . 12  |-  ( ( (UnifSt `  R )  e.  (UnifOn `  ( Base `  R ) )  /\  r  e.  (UnifSt `  R
) )  ->  Rel  r )
4138, 39, 40syl2anc 671 . . . . . . . . . . 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 471 . . . . . . . . . 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 17 . . . . . . . . . . 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 767 . . . . . . . . . . 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 741 . . . . . . . . . . 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 21292 . . . . . . . . . . 11  |-  ( ( (UnifSt `  R )  e.  (UnifOn `  ( Base `  R ) )  /\  r  e.  (UnifSt `  R
)  /\  x  e.  ( Base `  R )
)  ->  ( r " { x } ) 
C_  ( Base `  R
) )
4743, 44, 45, 46syl3anc 1276 . . . . . . . . . 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 467 . . . . . . . . . . 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 767 . . . . . . . . . . . . . . 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 774 . . . . . . . . . . . . . . . . 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 745 . . . . . . . . . . . . . . . . . . . 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 774 . . . . . . . . . . . . . . . . . . . 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 21275 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( (UnifSt `  S )  e.  (UnifOn `  ( Base `  S ) )  /\  s  e.  (UnifSt `  S
) )  ->  Rel  s )
5451, 52, 53syl2anc 671 . . . . . . . . . . . . . . . . . . 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 5211 . . . . . . . . . . . . . . . . . . 19  |-  ( Rel  s  ->  ( ( F `  z )  e.  ( s " {
( F `  x
) } )  <->  ( F `  x ) s ( F `  z ) ) )
5654, 55syl 17 . . . . . . . . . . . . . . . . . 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 492 . . . . . . . . . . . . . . . . 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 3445 . . . . . . . . . . . . . . . 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 726 . . . . . . . . . . . . . . 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 5751 . . . . . . . . . . . . . . . . 17  |-  ( F : ( Base `  R
) --> ( Base `  S
)  ->  F  Fn  ( Base `  R )
)
61 elpreima 6025 . . . . . . . . . . . . . . . . 17  |-  ( F  Fn  ( Base `  R
)  ->  ( z  e.  ( `' F "
a )  <->  ( z  e.  ( Base `  R
)  /\  ( F `  z )  e.  a ) ) )
6219, 60, 613syl 18 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( z  e.  ( `' F " a )  <-> 
( z  e.  (
Base `  R )  /\  ( F `  z
)  e.  a ) ) )
6362ad7antr 749 . . . . . . . . . . . . . . 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 938 . . . . . . . . . . . . . 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 440 . . . . . . . . . . . . 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 2814 . . . . . . . . . . . 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 471 . . . . . . . . . . 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 2929 . . . . . . . . . . . 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 593 . . . . . . . . . . . . 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 2793 . . . . . . . . . . . 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 218 . . . . . . . . . . 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 671 . . . . . . . . . 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 1067 . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . 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 5211 . . . . . . . . . . . . . . 15  |-  ( Rel  r  ->  ( y  e.  ( r " {
x } )  <->  x r
y ) )
7675biimpa 491 . . . . . . . . . . . . . 14  |-  ( ( Rel  r  /\  y  e.  ( r " {
x } ) )  ->  x r y )
7773, 74, 76syl2anc 671 . . . . . . . . . . . . 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 1068 . . . . . . . . . . . . . . 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 3445 . . . . . . . . . . . . . 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 1019 . . . . . . . . . . . . . 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 4420 . . . . . . . . . . . . . . . 16  |-  ( z  =  y  ->  (
x r z  <->  x r
y ) )
82 eleq1 2528 . . . . . . . . . . . . . . . 16  |-  ( z  =  y  ->  (
z  e.  ( `' F " a )  <-> 
y  e.  ( `' F " a ) ) )
8381, 82imbi12d 326 . . . . . . . . . . . . . . 15  |-  ( z  =  y  ->  (
( x r z  ->  z  e.  ( `' F " a ) )  <->  ( x r y  ->  y  e.  ( `' F " a ) ) ) )
8483rspcv 3158 . . . . . . . . . . . . . 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 62 . . . . . . . . . . . . 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 440 . . . . . . . . . . 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 3450 . . . . . . . . . 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 1281 . . . . . . . . 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 440 . . . . . . . 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 2874 . . . . . . 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 6025 . . . . . . . . . . 11  |-  ( F  Fn  ( Base `  R
)  ->  ( x  e.  ( `' F "
a )  <->  ( x  e.  ( Base `  R
)  /\  ( F `  x )  e.  a ) ) )
9419, 60, 933syl 18 . . . . . . . . . 10  |-  ( ph  ->  ( x  e.  ( `' F " a )  <-> 
( x  e.  (
Base `  R )  /\  ( F `  x
)  e.  a ) ) )
9594adantr 471 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  K )  ->  (
x  e.  ( `' F " a )  <-> 
( x  e.  (
Base `  R )  /\  ( F `  x
)  e.  a ) ) )
9695biimpa 491 . . . . . . . 8  |-  ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  -> 
( x  e.  (
Base `  R )  /\  ( F `  x
)  e.  a ) )
9796simprd 469 . . . . . . 7  |-  ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  -> 
( F `  x
)  e.  a )
98 simpr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  K )  ->  a  e.  K )
9913simprbi 470 . . . . . . . . . . . . 13  |-  ( S  e. UnifSp  ->  K  =  (unifTop `  (UnifSt `  S )
) )
1009, 99syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  K  =  (unifTop `  (UnifSt `  S ) ) )
101100adantr 471 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  K )  ->  K  =  (unifTop `  (UnifSt `  S
) ) )
10298, 101eleqtrd 2542 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  K )  ->  a  e.  (unifTop `  (UnifSt `  S
) ) )
103 elutop 21297 . . . . . . . . . . . 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 17 . . . . . . . . . . 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 471 . . . . . . . . . 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 215 . . . . . . . . 9  |-  ( (
ph  /\  a  e.  K )  ->  (
a  C_  ( Base `  S )  /\  A. y  e.  a  E. s  e.  (UnifSt `  S
) ( s " { y } ) 
C_  a ) )
107106simprd 469 . . . . . . . 8  |-  ( (
ph  /\  a  e.  K )  ->  A. y  e.  a  E. s  e.  (UnifSt `  S )
( s " {
y } )  C_  a )
108107adantr 471 . . . . . . 7  |-  ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  ->  A. y  e.  a  E. s  e.  (UnifSt `  S ) ( s
" { y } )  C_  a )
109 sneq 3990 . . . . . . . . . . 11  |-  ( y  =  ( F `  x )  ->  { y }  =  { ( F `  x ) } )
110109imaeq2d 5187 . . . . . . . . . 10  |-  ( y  =  ( F `  x )  ->  (
s " { y } )  =  ( s " { ( F `  x ) } ) )
111110sseq1d 3471 . . . . . . . . 9  |-  ( y  =  ( F `  x )  ->  (
( s " {
y } )  C_  a 
<->  ( s " {
( F `  x
) } )  C_  a ) )
112111rexbidv 2913 . . . . . . . 8  |-  ( y  =  ( F `  x )  ->  ( E. s  e.  (UnifSt `  S ) ( s
" { y } )  C_  a  <->  E. s  e.  (UnifSt `  S )
( s " {
( F `  x
) } )  C_  a ) )
113112rspcv 3158 . . . . . . 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 62 . . . . . 6  |-  ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  ->  E. s  e.  (UnifSt `  S ) ( s
" { ( F `
 x ) } )  C_  a )
11592, 114r19.29a 2944 . . . . 5  |-  ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  ->  E. r  e.  (UnifSt `  R ) ( r
" { x }
)  C_  ( `' F " a ) )
116115ralrimiva 2814 . . . 4  |-  ( (
ph  /\  a  e.  K )  ->  A. x  e.  ( `' F "
a ) E. r  e.  (UnifSt `  R )
( r " {
x } )  C_  ( `' F " a ) )
1176simprbi 470 . . . . . . . 8  |-  ( R  e. UnifSp  ->  J  =  (unifTop `  (UnifSt `  R )
) )
1182, 117syl 17 . . . . . . 7  |-  ( ph  ->  J  =  (unifTop `  (UnifSt `  R ) ) )
119118adantr 471 . . . . . 6  |-  ( (
ph  /\  a  e.  K )  ->  J  =  (unifTop `  (UnifSt `  R
) ) )
120119eleq2d 2525 . . . . 5  |-  ( (
ph  /\  a  e.  K )  ->  (
( `' F "
a )  e.  J  <->  ( `' F " a )  e.  (unifTop `  (UnifSt `  R ) ) ) )
121 elutop 21297 . . . . . . 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 17 . . . . . 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 471 . . . . 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 261 . . . 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 938 . . 3  |-  ( (
ph  /\  a  e.  K )  ->  ( `' F " a )  e.  J )
126125ralrimiva 2814 . 2  |-  ( ph  ->  A. a  e.  K  ( `' F " a )  e.  J )
127 ucncn.3 . . . 4  |-  ( ph  ->  R  e.  TopSp )
1283, 5istps 20000 . . . 4  |-  ( R  e.  TopSp 
<->  J  e.  (TopOn `  ( Base `  R )
) )
129127, 128sylib 201 . . 3  |-  ( ph  ->  J  e.  (TopOn `  ( Base `  R )
) )
130 ucncn.4 . . . 4  |-  ( ph  ->  S  e.  TopSp )
13110, 12istps 20000 . . . 4  |-  ( S  e.  TopSp 
<->  K  e.  (TopOn `  ( Base `  S )
) )
132130, 131sylib 201 . . 3  |-  ( ph  ->  K  e.  (TopOn `  ( Base `  S )
) )
133 iscn 20300 . . 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 671 . 2  |-  ( ph  ->  ( F  e.  ( J  Cn  K )  <-> 
( F : (
Base `  R ) --> ( Base `  S )  /\  A. a  e.  K  ( `' F " a )  e.  J ) ) )
13519, 126, 134mpbir2and 938 1  |-  ( ph  ->  F  e.  ( J  Cn  K ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375    /\ w3a 991    = wceq 1455    e. wcel 1898   A.wral 2749   E.wrex 2750    C_ wss 3416   {csn 3980   class class class wbr 4416   `'ccnv 4852   dom cdm 4853   "cima 4856   Rel wrel 4858    Fn wfn 5596   -->wf 5597   ` cfv 5601  (class class class)co 6315   Basecbs 15170   TopOpenctopn 15369  TopOnctopon 19967   TopSpctps 19968    Cn ccn 20289  UnifOncust 21263  unifTopcutop 21294  UnifStcuss 21317  UnifSpcusp 21318   Cnucucn 21339
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-opab 4476  df-mpt 4477  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-fv 5609  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-map 7500  df-top 19970  df-topon 19972  df-topsp 19973  df-cn 20292  df-ust 21264  df-utop 21295  df-usp 21321  df-ucn 21340
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator