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.

Step	Hyp	Ref	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 )
6	3, 4, 5	isusp 20632	. . . . . . 7 |- ( R e. UnifSp <-> ( (UnifSt ` R ) e. (UnifOn ` ( Base ` R ) ) /\ J = (unifTop ` (UnifSt ` R ) ) ) )
7	6	simplbi 460	. . . . . 6 |- ( R e. UnifSp -> (UnifSt ` R ) e. (UnifOn ` ( Base ` R ) ) )
8	2, 7	syl 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 )
13	10, 11, 12	isusp 20632	. . . . . . 7 |- ( S e. UnifSp <-> ( (UnifSt ` S ) e. (UnifOn ` ( Base ` S ) ) /\ K = (unifTop ` (UnifSt ` S ) ) ) )
14	13	simplbi 460	. . . . . 6 |- ( S e. UnifSp -> (UnifSt ` S ) e. (UnifOn ` ( Base ` S ) ) )
15	9, 14	syl 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 ) ) ) ) )
17	8, 15, 16	syl2anc 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 ) ) ) ) )
18	1, 17	mpbid 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 ) ) ) )
19	18	simpld 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 ) )
22	19, 21	syl 16	. . . . . 6 |- ( ph -> dom F = ( Base ` R ) )
23	22	adantr 465	. . . . 5 |- ( ( ph /\ a e. K ) -> dom F = ( Base ` R ) )
24	20, 23	syl5sseq 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 ) )
27	24	ad2antrr 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 ) )
29	27, 28	sseldd 3510	. . . . . . . . 9 |- ( ( ( ( ph /\ a e. K ) /\ x e. ( `' F " a ) ) /\ s e. (UnifSt ` S ) ) -> x e. ( Base ` R ) )
30	18	simprd 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 ) ) )
31	30	r19.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 ) ) )
33	31, 32	syl 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 ) ) )
34	33	r19.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 ) ) )
35	25, 26, 29, 34	syl21anc 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 ) ) )
36	35	adantr 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 ) ) )
37	25	ad3antrrr 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 )
38	8	ad5antr 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 )
41	38, 39, 40	syl2anc 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 )
42	41	adantr 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 )
43	37, 8	syl 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 ) )
45	29	ad3antrrr 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 ) )
47	43, 44, 45, 46	syl3anc 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 )
51	15	ad5antr 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 )
54	51, 52, 53	syl2anc 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 ) ) )
56	54, 55	syl 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 ) ) )
57	56	biimpar 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 ) } ) )
58	50, 57	sseldd 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 )
59	58	adantlr 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 ) ) )
62	19, 60, 61	3syl 20	. . . . . . . . . . . . . . . 16 |- ( ph -> ( z e. ( `' F " a ) <-> ( z e. ( Base ` R ) /\ ( F ` z ) e. a ) ) )
63	62	ad7antr 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 ) ) )
64	49, 59, 63	mpbir2and 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 ) )
65	64	ex 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 ) ) )
66	65	ralrimiva 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 ) ) )
67	66	adantr 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 ) ) )
70	69	ralimi 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 ) ) )
71	68, 70	sylbir 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 ) ) )
72	48, 67, 71	syl2anc 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 ) )
76	75	biimpa 484	. . . . . . . . . . . . . 14 |- ( ( Rel r /\ y e. ( r " { x } ) ) -> x r y )
77	73, 74, 76	syl2anc 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 ) )
79	78, 74	sseldd 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 ) ) )
83	81, 82	imbi12d 320	. . . . . . . . . . . . . . 15 |- ( z = y -> ( ( x r z -> z e. ( `' F " a ) ) <-> ( x r y -> y e. ( `' F " a ) ) ) )
84	83	rspcv 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 ) ) ) )
85	79, 80, 84	sylc 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 ) ) )
86	77, 85	mpd 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 ) )
87	86	ex 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 ) ) )
88	87	ssrdv 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 ) )
89	37, 42, 47, 72, 88	syl121anc 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 ) )
90	89	ex 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 ) ) )
91	90	reximdva 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 ) ) )
92	36, 91	mpd 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 ) ) )
94	19, 60, 93	3syl 20	. . . . . . . . . 10 |- ( ph -> ( x e. ( `' F " a ) <-> ( x e. ( Base ` R ) /\ ( F ` x ) e. a ) ) )
95	94	adantr 465	. . . . . . . . 9 |- ( ( ph /\ a e. K ) -> ( x e. ( `' F " a ) <-> ( x e. ( Base ` R ) /\ ( F ` x ) e. a ) ) )
96	95	biimpa 484	. . . . . . . 8 |- ( ( ( ph /\ a e. K ) /\ x e. ( `' F " a ) ) -> ( x e. ( Base ` R ) /\ ( F ` x ) e. a ) )
97	96	simprd 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 )
99	13	simprbi 464	. . . . . . . . . . . . 13 |- ( S e. UnifSp -> K = (unifTop ` (UnifSt ` S ) ) )
100	9, 99	syl 16	. . . . . . . . . . . 12 |- ( ph -> K = (unifTop ` (UnifSt ` S ) ) )
101	100	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ a e. K ) -> K = (unifTop ` (UnifSt ` S ) ) )
102	98, 101	eleqtrd 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 ) ) )
104	15, 103	syl 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 ) ) )
105	104	adantr 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 ) ) )
106	102, 105	mpbid 210	. . . . . . . . 9 |- ( ( ph /\ a e. K ) -> ( a C_ ( Base ` S ) /\ A. y e. a E. s e. (UnifSt ` S ) ( s " { y } ) C_ a ) )
107	106	simprd 463	. . . . . . . 8 |- ( ( ph /\ a e. K ) -> A. y e. a E. s e. (UnifSt ` S ) ( s " { y } ) C_ a )
108	107	adantr 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 ) } )
110	109	imaeq2d 5343	. . . . . . . . . 10 |- ( y = ( F ` x ) -> ( s " { y } ) = ( s " { ( F ` x ) } ) )
111	110	sseq1d 3536	. . . . . . . . 9 |- ( y = ( F ` x ) -> ( ( s " { y } ) C_ a <-> ( s " { ( F ` x ) } ) C_ a ) )
112	111	rexbidv 2978	. . . . . . . 8 |- ( y = ( F ` x ) -> ( E. s e. (UnifSt ` S ) ( s " { y } ) C_ a <-> E. s e. (UnifSt ` S ) ( s " { ( F ` x ) } ) C_ a ) )
113	112	rspcv 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 ) )
114	97, 108, 113	sylc 60	. . . . . 6 |- ( ( ( ph /\ a e. K ) /\ x e. ( `' F " a ) ) -> E. s e. (UnifSt ` S ) ( s " { ( F ` x ) } ) C_ a )
115	92, 114	r19.29a 3008	. . . . 5 |- ( ( ( ph /\ a e. K ) /\ x e. ( `' F " a ) ) -> E. r e. (UnifSt ` R ) ( r " { x } ) C_ ( `' F " a ) )
116	115	ralrimiva 2881	. . . 4 |- ( ( ph /\ a e. K ) -> A. x e. ( `' F " a ) E. r e. (UnifSt ` R ) ( r " { x } ) C_ ( `' F " a ) )
117	6	simprbi 464	. . . . . . . 8 |- ( R e. UnifSp -> J = (unifTop ` (UnifSt ` R ) ) )
118	2, 117	syl 16	. . . . . . 7 |- ( ph -> J = (unifTop ` (UnifSt ` R ) ) )
119	118	adantr 465	. . . . . 6 |- ( ( ph /\ a e. K ) -> J = (unifTop ` (UnifSt ` R ) ) )
120	119	eleq2d 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 ) ) ) )
122	8, 121	syl 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 ) ) ) )
123	122	adantr 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 ) ) ) )
124	120, 123	bitrd 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 ) ) ) )
125	24, 116, 124	mpbir2and 920	. . 3 |- ( ( ph /\ a e. K ) -> ( `' F " a ) e. J )
126	125	ralrimiva 2881	. 2 |- ( ph -> A. a e. K ( `' F " a ) e. J )
127		ucncn.3	. . . 4 |- ( ph -> R e. TopSp )
128	3, 5	istps 19306	. . . 4 |- ( R e. TopSp <-> J e. (TopOn ` ( Base ` R ) ) )
129	127, 128	sylib 196	. . 3 |- ( ph -> J e. (TopOn ` ( Base ` R ) ) )
130		ucncn.4	. . . 4 |- ( ph -> S e. TopSp )
131	10, 12	istps 19306	. . . 4 |- ( S e. TopSp <-> K e. (TopOn ` ( Base ` S ) ) )
132	130, 131	sylib 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 ) ) )
134	129, 132, 133	syl2anc 661	. 2 |- ( ph -> ( F e. ( J Cn K ) <-> ( F : ( Base ` R ) --> ( Base ` S ) /\ A. a e. K ( `' F " a ) e. J ) ) )
135	19, 126, 134	mpbir2and 920	1 |- ( ph -> F e. ( J Cn K ) )

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   Cn_ucucn 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)