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

Theorem ucncn 20656
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 2467 . . . . . . . 8  |-  ( Base `  R )  =  (
Base `  R )
4 eqid 2467 . . . . . . . 8  |-  (UnifSt `  R )  =  (UnifSt `  R )
5 ucncn.j . . . . . . . 8  |-  J  =  ( TopOpen `  R )
63, 4, 5isusp 20632 . . . . . . 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 2467 . . . . . . . 8  |-  ( Base `  S )  =  (
Base `  S )
11 eqid 2467 . . . . . . . 8  |-  (UnifSt `  S )  =  (UnifSt `  S )
12 ucncn.k . . . . . . . 8  |-  K  =  ( TopOpen `  S )
1310, 11, 12isusp 20632 . . . . . . 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 20649 . . . . 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 5363 . . . . 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 3557 . . . 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 3510 . . . . . . . . 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 2836 . . . . . . . . . . 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 2993 . . . . . . . . . . 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 2836 . . . . . . . . 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 20582 . . . . . . . . . . . 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 20599 . . . . . . . . . . 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 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 20582 . . . . . . . . . . . . . . . . . . . 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 5367 . . . . . . . . . . . . . . . . . . 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 3510 . . . . . . . . . . . . . . . 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 920 . . . . . . . . . . . . . 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 2881 . . . . . . . . . . . 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 2994 . . . . . . . . . . . 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 2860 . . . . . . . . . . . 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 5367 . . . . . . . . . . . . . . 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 3510 . . . . . . . . . . . . . 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 4457 . . . . . . . . . . . . . . . 16  |-  ( z  =  y  ->  (
x r z  <->  x r
y ) )
82 eleq1 2539 . . . . . . . . . . . . . . . 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 3215 . . . . . . . . . . . . . 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 3515 . . . . . . . . . 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 2942 . . . . . . 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 2557 . . . . . . . . . 10  |-  ( (
ph  /\  a  e.  K )  ->  a  e.  (unifTop `  (UnifSt `  S
) ) )
103 elutop 20604 . . . . . . . . . . . 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 4043 . . . . . . . . . . 11  |-  ( y  =  ( F `  x )  ->  { y }  =  { ( F `  x ) } )
110109imaeq2d 5343 . . . . . . . . . 10  |-  ( y  =  ( F `  x )  ->  (
s " { y } )  =  ( s " { ( F `  x ) } ) )
111110sseq1d 3536 . . . . . . . . 9  |-  ( y  =  ( F `  x )  ->  (
( s " {
y } )  C_  a 
<->  ( s " {
( F `  x
) } )  C_  a ) )
112111rexbidv 2978 . . . . . . . 8  |-  ( y  =  ( F `  x )  ->  ( E. s  e.  (UnifSt `  S ) ( s
" { y } )  C_  a  <->  E. s  e.  (UnifSt `  S )
( s " {
( F `  x
) } )  C_  a ) )
113112rspcv 3215 . . . . . . 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 3008 . . . . 5  |-  ( ( ( ph  /\  a  e.  K )  /\  x  e.  ( `' F "
a ) )  ->  E. r  e.  (UnifSt `  R ) ( r
" { x }
)  C_  ( `' F " a ) )
116115ralrimiva 2881 . . . 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 2537 . . . . 5  |-  ( (
ph  /\  a  e.  K )  ->  (
( `' F "
a )  e.  J  <->  ( `' F " a )  e.  (unifTop `  (UnifSt `  R ) ) ) )
121 elutop 20604 . . . . . . 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 920 . . 3  |-  ( (
ph  /\  a  e.  K )  ->  ( `' F " a )  e.  J )
126125ralrimiva 2881 . 2  |-  ( ph  ->  A. a  e.  K  ( `' F " a )  e.  J )
127 ucncn.3 . . . 4  |-  ( ph  ->  R  e.  TopSp )
1283, 5istps 19306 . . . 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 19306 . . . 4  |-  ( S  e.  TopSp 
<->  K  e.  (TopOn `  ( Base `  S )
) )
132130, 131sylib 196 . . 3  |-  ( ph  ->  K  e.  (TopOn `  ( Base `  S )
) )
133 iscn 19604 . . 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 920 1  |-  ( ph  ->  F  e.  ( J  Cn  K ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 973    = wceq 1379    e. wcel 1767   A.wral 2817   E.wrex 2818    C_ wss 3481   {csn 4033   class class class wbr 4453   `'ccnv 5004   dom cdm 5005   "cima 5008   Rel wrel 5010    Fn wfn 5589   -->wf 5590   ` cfv 5594  (class class class)co 6295   Basecbs 14507   TopOpenctopn 14694  TopOnctopon 19264   TopSpctps 19266    Cn ccn 19593  UnifOncust 20570  unifTopcutop 20601  UnifStcuss 20624  UnifSpcusp 20625   Cnucucn 20646
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-rex 2823  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-op 4040  df-uni 4252  df-br 4454  df-opab 4512  df-mpt 4513  df-id 4801  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-fv 5602  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-map 7434  df-top 19268  df-topon 19271  df-topsp 19272  df-cn 19596  df-ust 20571  df-utop 20602  df-usp 20628  df-ucn 20647
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator