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

Theorem ucncn 20914
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 2457 . . . . . . . 8  |-  ( Base `  R )  =  (
Base `  R )
4 eqid 2457 . . . . . . . 8  |-  (UnifSt `  R )  =  (UnifSt `  R )
5 ucncn.j . . . . . . . 8  |-  J  =  ( TopOpen `  R )
63, 4, 5isusp 20890 . . . . . . 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 2457 . . . . . . . 8  |-  ( Base `  S )  =  (
Base `  S )
11 eqid 2457 . . . . . . . 8  |-  (UnifSt `  S )  =  (UnifSt `  S )
12 ucncn.k . . . . . . . 8  |-  K  =  ( TopOpen `  S )
1310, 11, 12isusp 20890 . . . . . . 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 20907 . . . . 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 5367 . . . . 5  |-  ( `' F " a ) 
C_  dom  F
21 fdm 5741 . . . . . . 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 3547 . . . 4  |-  ( (
ph  /\  a  e.  K )  ->  ( `' F " a ) 
C_  ( Base `  R
) )
25 simplll 759 . . . . . . . . 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 755 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F " a ) )  /\  s  e.  (UnifSt `  S )
)  ->  x  e.  ( `' F " a ) )
2927, 28sseldd 3500 . . . . . . . . 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 2826 . . . . . . . . . . 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 2983 . . . . . . . . . . 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 2826 . . . . . . . . 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 1227 . . . . . . . 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 20840 . . . . . . . . . . . 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 755 . . . . . . . . . . 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 20857 . . . . . . . . . . 11  |-  ( ( (UnifSt `  R )  e.  (UnifOn `  ( Base `  R ) )  /\  r  e.  (UnifSt `  R
)  /\  x  e.  ( Base `  R )
)  ->  ( r " { x } ) 
C_  ( Base `  R
) )
4743, 44, 45, 46syl3anc 1228 . . . . . . . . . 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 755 . . . . . . . . . . . . . . 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 760 . . . . . . . . . . . . . . . . 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 760 . . . . . . . . . . . . . . . . . . . 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 20840 . . . . . . . . . . . . . . . . . . . 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 5371 . . . . . . . . . . . . . . . . . . 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 3500 . . . . . . . . . . . . . . . 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 5737 . . . . . . . . . . . . . . . . 17  |-  ( F : ( Base `  R
) --> ( Base `  S
)  ->  F  Fn  ( Base `  R )
)
61 elpreima 6008 . . . . . . . . . . . . . . . . 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 922 . . . . . . . . . . . . . 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 2871 . . . . . . . . . . . 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 2984 . . . . . . . . . . . 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 2850 . . . . . . . . . . . 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 1049 . . . . . . . . . . . . . 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 5371 . . . . . . . . . . . . . . 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 1050 . . . . . . . . . . . . . . 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 3500 . . . . . . . . . . . . . 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 1001 . . . . . . . . . . . . . 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 4460 . . . . . . . . . . . . . . . 16  |-  ( z  =  y  ->  (
x r z  <->  x r
y ) )
82 eleq1 2529 . . . . . . . . . . . . . . . 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 3206 . . . . . . . . . . . . . 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 3505 . . . . . . . . . 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 1233 . . . . . . . . 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 2932 . . . . . . 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 6008 . . . . . . . . . . 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 2547 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  K )  ->  a  e.  (unifTop `  (UnifSt `  S
) ) )
103 elutop 20862 . . . . . . . . . . . 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 4042 . . . . . . . . . . 11  |-  ( y  =  ( F `  x )  ->  { y }  =  { ( F `  x ) } )
110109imaeq2d 5347 . . . . . . . . . 10  |-  ( y  =  ( F `  x )  ->  (
s " { y } )  =  ( s " { ( F `  x ) } ) )
111110sseq1d 3526 . . . . . . . . 9  |-  ( y  =  ( F `  x )  ->  (
( s " {
y } )  C_  a 
<->  ( s " {
( F `  x
) } )  C_  a ) )
112111rexbidv 2968 . . . . . . . 8  |-  ( y  =  ( F `  x )  ->  ( E. s  e.  (UnifSt `  S ) ( s
" { y } )  C_  a  <->  E. s  e.  (UnifSt `  S )
( s " {
( F `  x
) } )  C_  a ) )
113112rspcv 3206 . . . . . . 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 2999 . . . . 5  |-  ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  ->  E. r  e.  (UnifSt `  R ) ( r
" { x }
)  C_  ( `' F " a ) )
116115ralrimiva 2871 . . . 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 2527 . . . . 5  |-  ( (
ph  /\  a  e.  K )  ->  (
( `' F "
a )  e.  J  <->  ( `' F " a )  e.  (unifTop `  (UnifSt `  R ) ) ) )
121 elutop 20862 . . . . . . 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 922 . . 3  |-  ( (
ph  /\  a  e.  K )  ->  ( `' F " a )  e.  J )
126125ralrimiva 2871 . 2  |-  ( ph  ->  A. a  e.  K  ( `' F " a )  e.  J )
127 ucncn.3 . . . 4  |-  ( ph  ->  R  e.  TopSp )
1283, 5istps 19564 . . . 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 19564 . . . 4  |-  ( S  e.  TopSp 
<->  K  e.  (TopOn `  ( Base `  S )
) )
132130, 131sylib 196 . . 3  |-  ( ph  ->  K  e.  (TopOn `  ( Base `  S )
) )
133 iscn 19863 . . 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 922 1  |-  ( ph  ->  F  e.  ( J  Cn  K ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 973    = wceq 1395    e. wcel 1819   A.wral 2807   E.wrex 2808    C_ wss 3471   {csn 4032   class class class wbr 4456   `'ccnv 5007   dom cdm 5008   "cima 5011   Rel wrel 5013    Fn wfn 5589   -->wf 5590   ` cfv 5594  (class class class)co 6296   Basecbs 14644   TopOpenctopn 14839  TopOnctopon 19522   TopSpctps 19524    Cn ccn 19852  UnifOncust 20828  unifTopcutop 20859  UnifStcuss 20882  UnifSpcusp 20883   Cnucucn 20904
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-br 4457  df-opab 4516  df-mpt 4517  df-id 4804  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-fv 5602  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-map 7440  df-top 19526  df-topon 19529  df-topsp 19530  df-cn 19855  df-ust 20829  df-utop 20860  df-usp 20886  df-ucn 20905
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator