This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ucncn

Description: Uniform continuity implies continuity. Deduction form. Proposition 1 of BourbakiTop1 p. II.6. (Contributed by Thierry Arnoux, 30-Nov-2017)

Ref Expression
Hypotheses 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 ) uCn ( UnifSt ` S ) ) )
Assertion ucncn 
|- ( ph -> F e. ( J Cn K ) )

Proof

Step Hyp Ref Expression
1 ucncn.j 
 |-  J = ( TopOpen ` R )
2 ucncn.k 
 |-  K = ( TopOpen ` S )
3 ucncn.1 
 |-  ( ph -> R e. UnifSp )
4 ucncn.2 
 |-  ( ph -> S e. UnifSp )
5 ucncn.3 
 |-  ( ph -> R e. TopSp )
6 ucncn.4 
 |-  ( ph -> S e. TopSp )
7 ucncn.5 
 |-  ( ph -> F e. ( ( UnifSt ` R ) uCn ( UnifSt ` S ) ) )
8 eqid 
 |-  ( Base ` R ) = ( Base ` R )
9 eqid 
 |-  ( UnifSt ` R ) = ( UnifSt ` R )
10 8 9 1 isusp 
 |-  ( R e. UnifSp <-> ( ( UnifSt ` R ) e. ( UnifOn ` ( Base ` R ) ) /\ J = ( unifTop ` ( UnifSt ` R ) ) ) )
11 10 simplbi 
 |-  ( R e. UnifSp -> ( UnifSt ` R ) e. ( UnifOn ` ( Base ` R ) ) )
12 3 11 syl 
 |-  ( ph -> ( UnifSt ` R ) e. ( UnifOn ` ( Base ` R ) ) )
13 eqid 
 |-  ( Base ` S ) = ( Base ` S )
14 eqid 
 |-  ( UnifSt ` S ) = ( UnifSt ` S )
15 13 14 2 isusp 
 |-  ( S e. UnifSp <-> ( ( UnifSt ` S ) e. ( UnifOn ` ( Base ` S ) ) /\ K = ( unifTop ` ( UnifSt ` S ) ) ) )
16 15 simplbi 
 |-  ( S e. UnifSp -> ( UnifSt ` S ) e. ( UnifOn ` ( Base ` S ) ) )
17 4 16 syl 
 |-  ( ph -> ( UnifSt ` S ) e. ( UnifOn ` ( Base ` S ) ) )
18 isucn 
 |-  ( ( ( UnifSt ` R ) e. ( UnifOn ` ( Base ` R ) ) /\ ( UnifSt ` S ) e. ( UnifOn ` ( Base ` S ) ) ) -> ( F e. ( ( UnifSt ` R ) uCn ( 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 ) ) ) ) )
19 12 17 18 syl2anc 
 |-  ( ph -> ( F e. ( ( UnifSt ` R ) uCn ( 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 ) ) ) ) )
20 7 19 mpbid 
 |-  ( 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 ) ) ) )
21 20 simpld 
 |-  ( ph -> F : ( Base ` R ) --> ( Base ` S ) )
22 cnvimass 
 |-  ( `' F " a ) C_ dom F
23 21 fdmd 
 |-  ( ph -> dom F = ( Base ` R ) )
24 23 adantr 
 |-  ( ( ph /\ a e. K ) -> dom F = ( Base ` R ) )
25 22 24 sseqtrid 
 |-  ( ( ph /\ a e. K ) -> ( `' F " a ) C_ ( Base ` R ) )
26 simplll 
 |-  ( ( ( ( ph /\ a e. K ) /\ x e. ( `' F " a ) ) /\ s e. ( UnifSt ` S ) ) -> ph )
27 simpr 
 |-  ( ( ( ( ph /\ a e. K ) /\ x e. ( `' F " a ) ) /\ s e. ( UnifSt ` S ) ) -> s e. ( UnifSt ` S ) )
28 25 ad2antrr 
 |-  ( ( ( ( ph /\ a e. K ) /\ x e. ( `' F " a ) ) /\ s e. ( UnifSt ` S ) ) -> ( `' F " a ) C_ ( Base ` R ) )
29 simplr 
 |-  ( ( ( ( ph /\ a e. K ) /\ x e. ( `' F " a ) ) /\ s e. ( UnifSt ` S ) ) -> x e. ( `' F " a ) )
30 28 29 sseldd 
 |-  ( ( ( ( ph /\ a e. K ) /\ x e. ( `' F " a ) ) /\ s e. ( UnifSt ` S ) ) -> x e. ( Base ` R ) )
31 20 simprd 
 |-  ( 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 ) ) )
32 31 r19.21bi 
 |-  ( ( 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 ) ) )
33 r19.12 
 |-  ( 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 ) ) )
34 32 33 syl 
 |-  ( ( 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 ) ) )
35 34 r19.21bi 
 |-  ( ( ( 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 ) ) )
36 26 27 30 35 syl21anc 
 |-  ( ( ( ( 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 ) ) )
37 36 adantr 
 |-  ( ( ( ( ( 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 ) ) )
38 26 ad3antrrr 
 |-  ( ( ( ( ( ( ( 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 )
39 12 ad5antr 
 |-  ( ( ( ( ( ( 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 ) ) )
40 simpr 
 |-  ( ( ( ( ( ( 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 ) )
41 ustrel 
 |-  ( ( ( UnifSt ` R ) e. ( UnifOn ` ( Base ` R ) ) /\ r e. ( UnifSt ` R ) ) -> Rel r )
42 39 40 41 syl2anc 
 |-  ( ( ( ( ( ( ph /\ a e. K ) /\ x e. ( `' F " a ) ) /\ s e. ( UnifSt ` S ) ) /\ ( s " { ( F ` x ) } ) C_ a ) /\ r e. ( UnifSt ` R ) ) -> Rel r )
43 42 adantr 
 |-  ( ( ( ( ( ( ( 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 )
44 38 12 syl 
 |-  ( ( ( ( ( ( ( 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 ) ) )
45 simplr 
 |-  ( ( ( ( ( ( ( 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 ) )
46 30 ad3antrrr 
 |-  ( ( ( ( ( ( ( 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 ) )
47 ustimasn 
 |-  ( ( ( UnifSt ` R ) e. ( UnifOn ` ( Base ` R ) ) /\ r e. ( UnifSt ` R ) /\ x e. ( Base ` R ) ) -> ( r " { x } ) C_ ( Base ` R ) )
48 44 45 46 47 syl3anc 
 |-  ( ( ( ( ( ( ( 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 ) )
49 simpr 
 |-  ( ( ( ( ( ( ( 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 ) ) )
50 simplr 
 |-  ( ( ( ( ( ( ( ( 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 ) )
51 simpllr 
 |-  ( ( ( ( ( ( ( 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 )
52 17 ad5antr 
 |-  ( ( ( ( ( ( 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 ) ) )
53 simpllr 
 |-  ( ( ( ( ( ( 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 ) )
54 ustrel 
 |-  ( ( ( UnifSt ` S ) e. ( UnifOn ` ( Base ` S ) ) /\ s e. ( UnifSt ` S ) ) -> Rel s )
55 52 53 54 syl2anc 
 |-  ( ( ( ( ( ( ph /\ a e. K ) /\ x e. ( `' F " a ) ) /\ s e. ( UnifSt ` S ) ) /\ ( s " { ( F ` x ) } ) C_ a ) /\ r e. ( UnifSt ` R ) ) -> Rel s )
56 elrelimasn 
 |-  ( Rel s -> ( ( F ` z ) e. ( s " { ( F ` x ) } ) <-> ( F ` x ) s ( F ` z ) ) )
57 55 56 syl 
 |-  ( ( ( ( ( ( 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 ) ) )
58 57 biimpar 
 |-  ( ( ( ( ( ( ( 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 ) } ) )
59 51 58 sseldd 
 |-  ( ( ( ( ( ( ( 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 )
60 59 adantlr 
 |-  ( ( ( ( ( ( ( ( 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 )
61 ffn 
 |-  ( F : ( Base ` R ) --> ( Base ` S ) -> F Fn ( Base ` R ) )
62 elpreima 
 |-  ( F Fn ( Base ` R ) -> ( z e. ( `' F " a ) <-> ( z e. ( Base ` R ) /\ ( F ` z ) e. a ) ) )
63 21 61 62 3syl 
 |-  ( ph -> ( z e. ( `' F " a ) <-> ( z e. ( Base ` R ) /\ ( F ` z ) e. a ) ) )
64 63 ad7antr 
 |-  ( ( ( ( ( ( ( ( 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 ) ) )
65 50 60 64 mpbir2and 
 |-  ( ( ( ( ( ( ( ( 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 ) )
66 65 ex 
 |-  ( ( ( ( ( ( ( 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 ) ) )
67 66 ralrimiva 
 |-  ( ( ( ( ( ( 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 ) ) )
68 67 adantr 
 |-  ( ( ( ( ( ( ( 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 ) ) )
69 r19.26 
 |-  ( 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 ) ) ) )
70 pm3.33 
 |-  ( ( ( x r z -> ( F ` x ) s ( F ` z ) ) /\ ( ( F ` x ) s ( F ` z ) -> z e. ( `' F " a ) ) ) -> ( x r z -> z e. ( `' F " a ) ) )
71 70 ralimi 
 |-  ( 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 ) ) )
72 69 71 sylbir 
 |-  ( ( 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 ) ) )
73 49 68 72 syl2anc 
 |-  ( ( ( ( ( ( ( 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 ) ) )
74 simpl2l 
 |-  ( ( ( 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 )
75 simpr 
 |-  ( ( ( 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 } ) )
76 elrelimasn 
 |-  ( Rel r -> ( y e. ( r " { x } ) <-> x r y ) )
77 76 biimpa 
 |-  ( ( Rel r /\ y e. ( r " { x } ) ) -> x r y )
78 74 75 77 syl2anc 
 |-  ( ( ( 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 )
79 breq2 
 |-  ( z = y -> ( x r z <-> x r y ) )
80 eleq1w 
 |-  ( z = y -> ( z e. ( `' F " a ) <-> y e. ( `' F " a ) ) )
81 79 80 imbi12d 
 |-  ( z = y -> ( ( x r z -> z e. ( `' F " a ) ) <-> ( x r y -> y e. ( `' F " a ) ) ) )
82 simpl3 
 |-  ( ( ( 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 ) ) )
83 simpl2r 
 |-  ( ( ( 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 ) )
84 83 75 sseldd 
 |-  ( ( ( 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 ) )
85 81 82 84 rspcdva 
 |-  ( ( ( 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 ) ) )
86 78 85 mpd 
 |-  ( ( ( 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 ) )
87 86 ex 
 |-  ( ( 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 ) ) )
88 87 ssrdv 
 |-  ( ( 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 ) )
89 38 43 48 73 88 syl121anc 
 |-  ( ( ( ( ( ( ( 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 ) )
90 89 ex 
 |-  ( ( ( ( ( ( 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 ) ) )
91 90 reximdva 
 |-  ( ( ( ( ( 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 ) ) )
92 37 91 mpd 
 |-  ( ( ( ( ( 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 sneq 
 |-  ( y = ( F ` x ) -> { y } = { ( F ` x ) } )
94 93 imaeq2d 
 |-  ( y = ( F ` x ) -> ( s " { y } ) = ( s " { ( F ` x ) } ) )
95 94 sseq1d 
 |-  ( y = ( F ` x ) -> ( ( s " { y } ) C_ a <-> ( s " { ( F ` x ) } ) C_ a ) )
96 95 rexbidv 
 |-  ( y = ( F ` x ) -> ( E. s e. ( UnifSt ` S ) ( s " { y } ) C_ a <-> E. s e. ( UnifSt ` S ) ( s " { ( F ` x ) } ) C_ a ) )
97 simpr 
 |-  ( ( ph /\ a e. K ) -> a e. K )
98 15 simprbi 
 |-  ( S e. UnifSp -> K = ( unifTop ` ( UnifSt ` S ) ) )
99 4 98 syl 
 |-  ( ph -> K = ( unifTop ` ( UnifSt ` S ) ) )
100 99 adantr 
 |-  ( ( ph /\ a e. K ) -> K = ( unifTop ` ( UnifSt ` S ) ) )
101 97 100 eleqtrd 
 |-  ( ( ph /\ a e. K ) -> a e. ( unifTop ` ( UnifSt ` S ) ) )
102 elutop 
 |-  ( ( 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 ) ) )
103 17 102 syl 
 |-  ( ph -> ( a e. ( unifTop ` ( UnifSt ` S ) ) <-> ( a C_ ( Base ` S ) /\ A. y e. a E. s e. ( UnifSt ` S ) ( s " { y } ) C_ a ) ) )
104 103 adantr 
 |-  ( ( 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 ) ) )
105 101 104 mpbid 
 |-  ( ( ph /\ a e. K ) -> ( a C_ ( Base ` S ) /\ A. y e. a E. s e. ( UnifSt ` S ) ( s " { y } ) C_ a ) )
106 105 simprd 
 |-  ( ( ph /\ a e. K ) -> A. y e. a E. s e. ( UnifSt ` S ) ( s " { y } ) C_ a )
107 106 adantr 
 |-  ( ( ( ph /\ a e. K ) /\ x e. ( `' F " a ) ) -> A. y e. a E. s e. ( UnifSt ` S ) ( s " { y } ) C_ a )
108 elpreima 
 |-  ( F Fn ( Base ` R ) -> ( x e. ( `' F " a ) <-> ( x e. ( Base ` R ) /\ ( F ` x ) e. a ) ) )
109 21 61 108 3syl 
 |-  ( ph -> ( x e. ( `' F " a ) <-> ( x e. ( Base ` R ) /\ ( F ` x ) e. a ) ) )
110 109 adantr 
 |-  ( ( ph /\ a e. K ) -> ( x e. ( `' F " a ) <-> ( x e. ( Base ` R ) /\ ( F ` x ) e. a ) ) )
111 110 biimpa 
 |-  ( ( ( ph /\ a e. K ) /\ x e. ( `' F " a ) ) -> ( x e. ( Base ` R ) /\ ( F ` x ) e. a ) )
112 111 simprd 
 |-  ( ( ( ph /\ a e. K ) /\ x e. ( `' F " a ) ) -> ( F ` x ) e. a )
113 96 107 112 rspcdva 
 |-  ( ( ( ph /\ a e. K ) /\ x e. ( `' F " a ) ) -> E. s e. ( UnifSt ` S ) ( s " { ( F ` x ) } ) C_ a )
114 92 113 r19.29a 
 |-  ( ( ( ph /\ a e. K ) /\ x e. ( `' F " a ) ) -> E. r e. ( UnifSt ` R ) ( r " { x } ) C_ ( `' F " a ) )
115 114 ralrimiva 
 |-  ( ( ph /\ a e. K ) -> A. x e. ( `' F " a ) E. r e. ( UnifSt ` R ) ( r " { x } ) C_ ( `' F " a ) )
116 10 simprbi 
 |-  ( R e. UnifSp -> J = ( unifTop ` ( UnifSt ` R ) ) )
117 3 116 syl 
 |-  ( ph -> J = ( unifTop ` ( UnifSt ` R ) ) )
118 117 adantr 
 |-  ( ( ph /\ a e. K ) -> J = ( unifTop ` ( UnifSt ` R ) ) )
119 118 eleq2d 
 |-  ( ( ph /\ a e. K ) -> ( ( `' F " a ) e. J <-> ( `' F " a ) e. ( unifTop ` ( UnifSt ` R ) ) ) )
120 elutop 
 |-  ( ( 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 ) ) ) )
121 12 120 syl 
 |-  ( 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 ) ) ) )
122 121 adantr 
 |-  ( ( 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 ) ) ) )
123 119 122 bitrd 
 |-  ( ( 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 ) ) ) )
124 25 115 123 mpbir2and 
 |-  ( ( ph /\ a e. K ) -> ( `' F " a ) e. J )
125 124 ralrimiva 
 |-  ( ph -> A. a e. K ( `' F " a ) e. J )
126 8 1 istps 
 |-  ( R e. TopSp <-> J e. ( TopOn ` ( Base ` R ) ) )
127 5 126 sylib 
 |-  ( ph -> J e. ( TopOn ` ( Base ` R ) ) )
128 13 2 istps 
 |-  ( S e. TopSp <-> K e. ( TopOn ` ( Base ` S ) ) )
129 6 128 sylib 
 |-  ( ph -> K e. ( TopOn ` ( Base ` S ) ) )
130 iscn 
 |-  ( ( 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 ) ) )
131 127 129 130 syl2anc 
 |-  ( ph -> ( F e. ( J Cn K ) <-> ( F : ( Base ` R ) --> ( Base ` S ) /\ A. a e. K ( `' F " a ) e. J ) ) )
132 21 125 131 mpbir2and 
 |-  ( ph -> F e. ( J Cn K ) )