MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xkococnlem Structured version   Visualization version   Unicode version
Theorem xkococnlem 21462
Description: Continuity of the composition operation as a function on continuous function spaces. (Contributed by Mario Carneiro, 20-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
Hypotheses
Ref Expression
xkococn.1 |- F = ( f e. ( S Cn T ) , g e. ( R Cn S ) |-> ( f o. g ) )
xkococn.s |- ( ph -> S e. 𝑛Locally Comp )
xkococn.k |- ( ph -> K C_ U. R )
xkococn.c |- ( ph -> ( R ↾t K ) e. Comp )
xkococn.v |- ( ph -> V e. T )
xkococn.a |- ( ph -> A e. ( S Cn T ) )
xkococn.b |- ( ph -> B e. ( R Cn S ) )
xkococn.i |- ( ph -> ( ( A o. B ) " K ) C_ V )
Assertion
Ref Expression
xkococnlem |- ( ph -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( <. A , B >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " K ) C_ V } ) ) )
Distinct variable groups:   z, A   z, B   f, g, h, z, R   S, f, g, z   h, K, z   T, f, g, h, z   z, F   h, V, z
Allowed substitution hints:   ph( z, f, g, h)   A( f, g, h)   B( f, g, h)   S( h)   F( f, g, h)   K( f, g)   V( f, g)
Proof of Theorem xkococnlem
Dummy variables k a s u v w x y b are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xkococn.b . . . 4 |- ( ph -> B e. ( R Cn S ) )
2 xkococn.c . . . 4 |- ( ph -> ( R ↾t K ) e. Comp )
3 imacmp 21200 . . . 4 |- ( ( B e. ( R Cn S ) /\ ( R ↾t K ) e. Comp ) -> ( S ↾t ( B " K ) ) e. Comp )
41, 2, 3syl2anc 693 . . 3 |- ( ph -> ( S ↾t ( B " K ) ) e. Comp )
5 xkococn.s . . . . . . . . 9 |- ( ph -> S e. 𝑛Locally Comp )
65adantr 481 . . . . . . . 8 |- ( ( ph /\ x e. ( B " K ) ) -> S e. 𝑛Locally Comp )
7 xkococn.a . . . . . . . . . 10 |- ( ph -> A e. ( S Cn T ) )
8 xkococn.v . . . . . . . . . 10 |- ( ph -> V e. T )
9 cnima 21069 . . . . . . . . . 10 |- ( ( A e. ( S Cn T ) /\ V e. T ) -> ( `' A " V ) e. S )
107, 8, 9syl2anc 693 . . . . . . . . 9 |- ( ph -> ( `' A " V ) e. S )
1110adantr 481 . . . . . . . 8 |- ( ( ph /\ x e. ( B " K ) ) -> ( `' A " V ) e. S )
12 imaco 5640 . . . . . . . . . . 11 |- ( ( A o. B ) " K ) = ( A " ( B " K ) )
13 xkococn.i . . . . . . . . . . 11 |- ( ph -> ( ( A o. B ) " K ) C_ V )
1412, 13syl5eqssr 3650 . . . . . . . . . 10 |- ( ph -> ( A " ( B " K ) ) C_ V )
15 eqid 2622 . . . . . . . . . . . . 13 |- U. S = U. S
16 eqid 2622 . . . . . . . . . . . . 13 |- U. T = U. T
1715, 16cnf 21050 . . . . . . . . . . . 12 |- ( A e. ( S Cn T ) -> A : U. S --> U. T )
18 ffun 6048 . . . . . . . . . . . 12 |- ( A : U. S --> U. T -> Fun A )
197, 17, 183syl 18 . . . . . . . . . . 11 |- ( ph -> Fun A )
20 imassrn 5477 . . . . . . . . . . . . 13 |- ( B " K ) C_ ran B
21 eqid 2622 . . . . . . . . . . . . . . 15 |- U. R = U. R
2221, 15cnf 21050 . . . . . . . . . . . . . 14 |- ( B e. ( R Cn S ) -> B : U. R --> U. S )
23 frn 6053 . . . . . . . . . . . . . 14 |- ( B : U. R --> U. S -> ran B C_ U. S )
241, 22, 233syl 18 . . . . . . . . . . . . 13 |- ( ph -> ran B C_ U. S )
2520, 24syl5ss 3614 . . . . . . . . . . . 12 |- ( ph -> ( B " K ) C_ U. S )
26 fdm 6051 . . . . . . . . . . . . 13 |- ( A : U. S --> U. T -> dom A = U. S )
277, 17, 263syl 18 . . . . . . . . . . . 12 |- ( ph -> dom A = U. S )
2825, 27sseqtr4d 3642 . . . . . . . . . . 11 |- ( ph -> ( B " K ) C_ dom A )
29 funimass3 6333 . . . . . . . . . . 11 |- ( ( Fun A /\ ( B " K ) C_ dom A ) -> ( ( A " ( B " K ) ) C_ V <-> ( B " K ) C_ ( `' A " V ) ) )
3019, 28, 29syl2anc 693 . . . . . . . . . 10 |- ( ph -> ( ( A " ( B " K ) ) C_ V <-> ( B " K ) C_ ( `' A " V ) ) )
3114, 30mpbid 222 . . . . . . . . 9 |- ( ph -> ( B " K ) C_ ( `' A " V ) )
3231sselda 3603 . . . . . . . 8 |- ( ( ph /\ x e. ( B " K ) ) -> x e. ( `' A " V ) )
33 nlly2i 21279 . . . . . . . 8 |- ( ( S e. 𝑛Locally Comp /\ ( `' A " V ) e. S /\ x e. ( `' A " V ) ) -> E. s e. ~P ( `' A " V ) E. u e. S ( x e. u /\ u C_ s /\ ( S ↾t s ) e. Comp ) )
346, 11, 32, 33syl3anc 1326 . . . . . . 7 |- ( ( ph /\ x e. ( B " K ) ) -> E. s e. ~P ( `' A " V ) E. u e. S ( x e. u /\ u C_ s /\ ( S ↾t s ) e. Comp ) )
35 nllytop 21276 . . . . . . . . . . . . 13 |- ( S e. 𝑛Locally Comp -> S e. Top )
365, 35syl 17 . . . . . . . . . . . 12 |- ( ph -> S e. Top )
3736ad3antrrr 766 . . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. ( B " K ) ) /\ s e. ~P ( `' A " V ) ) /\ ( u e. S /\ ( x e. u /\ u C_ s /\ ( S ↾t s ) e. Comp ) ) ) -> S e. Top )
38 imaexg 7103 . . . . . . . . . . . . 13 |- ( B e. ( R Cn S ) -> ( B " K ) e. _V )
391, 38syl 17 . . . . . . . . . . . 12 |- ( ph -> ( B " K ) e. _V )
4039ad3antrrr 766 . . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. ( B " K ) ) /\ s e. ~P ( `' A " V ) ) /\ ( u e. S /\ ( x e. u /\ u C_ s /\ ( S ↾t s ) e. Comp ) ) ) -> ( B " K ) e. _V )
41 simprl 794 . . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. ( B " K ) ) /\ s e. ~P ( `' A " V ) ) /\ ( u e. S /\ ( x e. u /\ u C_ s /\ ( S ↾t s ) e. Comp ) ) ) -> u e. S )
42 elrestr 16089 . . . . . . . . . . 11 |- ( ( S e. Top /\ ( B " K ) e. _V /\ u e. S ) -> ( u i^i ( B " K ) ) e. ( S ↾t ( B " K ) ) )
4337, 40, 41, 42syl3anc 1326 . . . . . . . . . 10 |- ( ( ( ( ph /\ x e. ( B " K ) ) /\ s e. ~P ( `' A " V ) ) /\ ( u e. S /\ ( x e. u /\ u C_ s /\ ( S ↾t s ) e. Comp ) ) ) -> ( u i^i ( B " K ) ) e. ( S ↾t ( B " K ) ) )
44 simprr1 1109 . . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. ( B " K ) ) /\ s e. ~P ( `' A " V ) ) /\ ( u e. S /\ ( x e. u /\ u C_ s /\ ( S ↾t s ) e. Comp ) ) ) -> x e. u )
45 simpllr 799 . . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. ( B " K ) ) /\ s e. ~P ( `' A " V ) ) /\ ( u e. S /\ ( x e. u /\ u C_ s /\ ( S ↾t s ) e. Comp ) ) ) -> x e. ( B " K ) )
4644, 45elind 3798 . . . . . . . . . 10 |- ( ( ( ( ph /\ x e. ( B " K ) ) /\ s e. ~P ( `' A " V ) ) /\ ( u e. S /\ ( x e. u /\ u C_ s /\ ( S ↾t s ) e. Comp ) ) ) -> x e. ( u i^i ( B " K ) ) )
47 inss1 3833 . . . . . . . . . . . 12 |- ( u i^i ( B " K ) ) C_ u
48 elpwi 4168 . . . . . . . . . . . . . . 15 |- ( s e. ~P ( `' A " V ) -> s C_ ( `' A " V ) )
4948ad2antlr 763 . . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ x e. ( B " K ) ) /\ s e. ~P ( `' A " V ) ) /\ ( u e. S /\ ( x e. u /\ u C_ s /\ ( S ↾t s ) e. Comp ) ) ) -> s C_ ( `' A " V ) )
50 elssuni 4467 . . . . . . . . . . . . . . . 16 |- ( ( `' A " V ) e. S -> ( `' A " V ) C_ U. S )
5110, 50syl 17 . . . . . . . . . . . . . . 15 |- ( ph -> ( `' A " V ) C_ U. S )
5251ad3antrrr 766 . . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ x e. ( B " K ) ) /\ s e. ~P ( `' A " V ) ) /\ ( u e. S /\ ( x e. u /\ u C_ s /\ ( S ↾t s ) e. Comp ) ) ) -> ( `' A " V ) C_ U. S )
5349, 52sstrd 3613 . . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. ( B " K ) ) /\ s e. ~P ( `' A " V ) ) /\ ( u e. S /\ ( x e. u /\ u C_ s /\ ( S ↾t s ) e. Comp ) ) ) -> s C_ U. S )
54 simprr2 1110 . . . . . . . . . . . . 13 |- ( ( ( ( ph /\ x e. ( B " K ) ) /\ s e. ~P ( `' A " V ) ) /\ ( u e. S /\ ( x e. u /\ u C_ s /\ ( S ↾t s ) e. Comp ) ) ) -> u C_ s )
5515ssntr 20862 . . . . . . . . . . . . 13 |- ( ( ( S e. Top /\ s C_ U. S ) /\ ( u e. S /\ u C_ s ) ) -> u C_ ( ( int ` S ) ` s ) )
5637, 53, 41, 54, 55syl22anc 1327 . . . . . . . . . . . 12 |- ( ( ( ( ph /\ x e. ( B " K ) ) /\ s e. ~P ( `' A " V ) ) /\ ( u e. S /\ ( x e. u /\ u C_ s /\ ( S ↾t s ) e. Comp ) ) ) -> u C_ ( ( int ` S ) ` s ) )
5747, 56syl5ss 3614 . . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. ( B " K ) ) /\ s e. ~P ( `' A " V ) ) /\ ( u e. S /\ ( x e. u /\ u C_ s /\ ( S ↾t s ) e. Comp ) ) ) -> ( u i^i ( B " K ) ) C_ ( ( int ` S ) ` s ) )
58 simprr3 1111 . . . . . . . . . . 11 |- ( ( ( ( ph /\ x e. ( B " K ) ) /\ s e. ~P ( `' A " V ) ) /\ ( u e. S /\ ( x e. u /\ u C_ s /\ ( S ↾t s ) e. Comp ) ) ) -> ( S ↾t s ) e. Comp )
5957, 58jca 554 . . . . . . . . . 10 |- ( ( ( ( ph /\ x e. ( B " K ) ) /\ s e. ~P ( `' A " V ) ) /\ ( u e. S /\ ( x e. u /\ u C_ s /\ ( S ↾t s ) e. Comp ) ) ) -> ( ( u i^i ( B " K ) ) C_ ( ( int ` S ) ` s ) /\ ( S ↾t s ) e. Comp ) )
60 eleq2 2690 . . . . . . . . . . . 12 |- ( y = ( u i^i ( B " K ) ) -> ( x e. y <-> x e. ( u i^i ( B " K ) ) ) )
61 sseq1 3626 . . . . . . . . . . . . 13 |- ( y = ( u i^i ( B " K ) ) -> ( y C_ ( ( int ` S ) ` s ) <-> ( u i^i ( B " K ) ) C_ ( ( int ` S ) ` s ) ) )
6261anbi1d 741 . . . . . . . . . . . 12 |- ( y = ( u i^i ( B " K ) ) -> ( ( y C_ ( ( int ` S ) ` s ) /\ ( S ↾t s ) e. Comp ) <-> ( ( u i^i ( B " K ) ) C_ ( ( int ` S ) ` s ) /\ ( S ↾t s ) e. Comp ) ) )
6360, 62anbi12d 747 . . . . . . . . . . 11 |- ( y = ( u i^i ( B " K ) ) -> ( ( x e. y /\ ( y C_ ( ( int ` S ) ` s ) /\ ( S ↾t s ) e. Comp ) ) <-> ( x e. ( u i^i ( B " K ) ) /\ ( ( u i^i ( B " K ) ) C_ ( ( int ` S ) ` s ) /\ ( S ↾t s ) e. Comp ) ) ) )
6463rspcev 3309 . . . . . . . . . 10 |- ( ( ( u i^i ( B " K ) ) e. ( S ↾t ( B " K ) ) /\ ( x e. ( u i^i ( B " K ) ) /\ ( ( u i^i ( B " K ) ) C_ ( ( int ` S ) ` s ) /\ ( S ↾t s ) e. Comp ) ) ) -> E. y e. ( S ↾t ( B " K ) ) ( x e. y /\ ( y C_ ( ( int ` S ) ` s ) /\ ( S ↾t s ) e. Comp ) ) )
6543, 46, 59, 64syl12anc 1324 . . . . . . . . 9 |- ( ( ( ( ph /\ x e. ( B " K ) ) /\ s e. ~P ( `' A " V ) ) /\ ( u e. S /\ ( x e. u /\ u C_ s /\ ( S ↾t s ) e. Comp ) ) ) -> E. y e. ( S ↾t ( B " K ) ) ( x e. y /\ ( y C_ ( ( int ` S ) ` s ) /\ ( S ↾t s ) e. Comp ) ) )
6665rexlimdvaa 3032 . . . . . . . 8 |- ( ( ( ph /\ x e. ( B " K ) ) /\ s e. ~P ( `' A " V ) ) -> ( E. u e. S ( x e. u /\ u C_ s /\ ( S ↾t s ) e. Comp ) -> E. y e. ( S ↾t ( B " K ) ) ( x e. y /\ ( y C_ ( ( int ` S ) ` s ) /\ ( S ↾t s ) e. Comp ) ) ) )
6766reximdva 3017 . . . . . . 7 |- ( ( ph /\ x e. ( B " K ) ) -> ( E. s e. ~P ( `' A " V ) E. u e. S ( x e. u /\ u C_ s /\ ( S ↾t s ) e. Comp ) -> E. s e. ~P ( `' A " V ) E. y e. ( S ↾t ( B " K ) ) ( x e. y /\ ( y C_ ( ( int ` S ) ` s ) /\ ( S ↾t s ) e. Comp ) ) ) )
6834, 67mpd 15 . . . . . 6 |- ( ( ph /\ x e. ( B " K ) ) -> E. s e. ~P ( `' A " V ) E. y e. ( S ↾t ( B " K ) ) ( x e. y /\ ( y C_ ( ( int ` S ) ` s ) /\ ( S ↾t s ) e. Comp ) ) )
69 rexcom 3099 . . . . . . 7 |- ( E. s e. ~P ( `' A " V ) E. y e. ( S ↾t ( B " K ) ) ( x e. y /\ ( y C_ ( ( int ` S ) ` s ) /\ ( S ↾t s ) e. Comp ) ) <-> E. y e. ( S ↾t ( B " K ) ) E. s e. ~P ( `' A " V ) ( x e. y /\ ( y C_ ( ( int ` S ) ` s ) /\ ( S ↾t s ) e. Comp ) ) )
70 r19.42v 3092 . . . . . . . 8 |- ( E. s e. ~P ( `' A " V ) ( x e. y /\ ( y C_ ( ( int ` S ) ` s ) /\ ( S ↾t s ) e. Comp ) ) <-> ( x e. y /\ E. s e. ~P ( `' A " V ) ( y C_ ( ( int ` S ) ` s ) /\ ( S ↾t s ) e. Comp ) ) )
7170rexbii 3041 . . . . . . 7 |- ( E. y e. ( S ↾t ( B " K ) ) E. s e. ~P ( `' A " V ) ( x e. y /\ ( y C_ ( ( int ` S ) ` s ) /\ ( S ↾t s ) e. Comp ) ) <-> E. y e. ( S ↾t ( B " K ) ) ( x e. y /\ E. s e. ~P ( `' A " V ) ( y C_ ( ( int ` S ) ` s ) /\ ( S ↾t s ) e. Comp ) ) )
7269, 71bitri 264 . . . . . 6 |- ( E. s e. ~P ( `' A " V ) E. y e. ( S ↾t ( B " K ) ) ( x e. y /\ ( y C_ ( ( int ` S ) ` s ) /\ ( S ↾t s ) e. Comp ) ) <-> E. y e. ( S ↾t ( B " K ) ) ( x e. y /\ E. s e. ~P ( `' A " V ) ( y C_ ( ( int ` S ) ` s ) /\ ( S ↾t s ) e. Comp ) ) )
7368, 72sylib 208 . . . . 5 |- ( ( ph /\ x e. ( B " K ) ) -> E. y e. ( S ↾t ( B " K ) ) ( x e. y /\ E. s e. ~P ( `' A " V ) ( y C_ ( ( int ` S ) ` s ) /\ ( S ↾t s ) e. Comp ) ) )
7473ralrimiva 2966 . . . 4 |- ( ph -> A. x e. ( B " K ) E. y e. ( S ↾t ( B " K ) ) ( x e. y /\ E. s e. ~P ( `' A " V ) ( y C_ ( ( int ` S ) ` s ) /\ ( S ↾t s ) e. Comp ) ) )
7515restuni 20966 . . . . . 6 |- ( ( S e. Top /\ ( B " K ) C_ U. S ) -> ( B " K ) = U. ( S ↾t ( B " K ) ) )
7636, 25, 75syl2anc 693 . . . . 5 |- ( ph -> ( B " K ) = U. ( S ↾t ( B " K ) ) )
7776raleqdv 3144 . . . 4 |- ( ph -> ( A. x e. ( B " K ) E. y e. ( S ↾t ( B " K ) ) ( x e. y /\ E. s e. ~P ( `' A " V ) ( y C_ ( ( int ` S ) ` s ) /\ ( S ↾t s ) e. Comp ) ) <-> A. x e. U. ( S ↾t ( B " K ) ) E. y e. ( S ↾t ( B " K ) ) ( x e. y /\ E. s e. ~P ( `' A " V ) ( y C_ ( ( int ` S ) ` s ) /\ ( S ↾t s ) e. Comp ) ) ) )
7874, 77mpbid 222 . . 3 |- ( ph -> A. x e. U. ( S ↾t ( B " K ) ) E. y e. ( S ↾t ( B " K ) ) ( x e. y /\ E. s e. ~P ( `' A " V ) ( y C_ ( ( int ` S ) ` s ) /\ ( S ↾t s ) e. Comp ) ) )
79 eqid 2622 . . . 4 |- U. ( S ↾t ( B " K ) ) = U. ( S ↾t ( B " K ) )
80 fveq2 6191 . . . . . 6 |- ( s = ( k ` y ) -> ( ( int ` S ) ` s ) = ( ( int ` S ) ` ( k ` y ) ) )
8180sseq2d 3633 . . . . 5 |- ( s = ( k ` y ) -> ( y C_ ( ( int ` S ) ` s ) <-> y C_ ( ( int ` S ) ` ( k ` y ) ) ) )
82 oveq2 6658 . . . . . 6 |- ( s = ( k ` y ) -> ( S ↾t s ) = ( S ↾t ( k ` y ) ) )
8382eleq1d 2686 . . . . 5 |- ( s = ( k ` y ) -> ( ( S ↾t s ) e. Comp <-> ( S ↾t ( k ` y ) ) e. Comp ) )
8481, 83anbi12d 747 . . . 4 |- ( s = ( k ` y ) -> ( ( y C_ ( ( int ` S ) ` s ) /\ ( S ↾t s ) e. Comp ) <-> ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) )
8579, 84cmpcovf 21194 . . 3 |- ( ( ( S ↾t ( B " K ) ) e. Comp /\ A. x e. U. ( S ↾t ( B " K ) ) E. y e. ( S ↾t ( B " K ) ) ( x e. y /\ E. s e. ~P ( `' A " V ) ( y C_ ( ( int ` S ) ` s ) /\ ( S ↾t s ) e. Comp ) ) ) -> E. w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ( U. ( S ↾t ( B " K ) ) = U. w /\ E. k ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) )
864, 78, 85syl2anc 693 . 2 |- ( ph -> E. w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ( U. ( S ↾t ( B " K ) ) = U. w /\ E. k ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) )
8776adantr 481 . . . . . . 7 |- ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) -> ( B " K ) = U. ( S ↾t ( B " K ) ) )
8887eqeq1d 2624 . . . . . 6 |- ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) -> ( ( B " K ) = U. w <-> U. ( S ↾t ( B " K ) ) = U. w ) )
8988biimpar 502 . . . . 5 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ U. ( S ↾t ( B " K ) ) = U. w ) -> ( B " K ) = U. w )
9036ad2antrr 762 . . . . . . . . . 10 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> S e. Top )
91 cntop2 21045 . . . . . . . . . . . 12 |- ( A e. ( S Cn T ) -> T e. Top )
927, 91syl 17 . . . . . . . . . . 11 |- ( ph -> T e. Top )
9392ad2antrr 762 . . . . . . . . . 10 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> T e. Top )
94 xkotop 21391 . . . . . . . . . 10 |- ( ( S e. Top /\ T e. Top ) -> ( T ^ko S ) e. Top )
9590, 93, 94syl2anc 693 . . . . . . . . 9 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> ( T ^ko S ) e. Top )
96 cntop1 21044 . . . . . . . . . . . 12 |- ( B e. ( R Cn S ) -> R e. Top )
971, 96syl 17 . . . . . . . . . . 11 |- ( ph -> R e. Top )
9897ad2antrr 762 . . . . . . . . . 10 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> R e. Top )
99 xkotop 21391 . . . . . . . . . 10 |- ( ( R e. Top /\ S e. Top ) -> ( S ^ko R ) e. Top )
10098, 90, 99syl2anc 693 . . . . . . . . 9 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> ( S ^ko R ) e. Top )
101 simprrl 804 . . . . . . . . . . . . 13 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> k : w --> ~P ( `' A " V ) )
102 frn 6053 . . . . . . . . . . . . 13 |- ( k : w --> ~P ( `' A " V ) -> ran k C_ ~P ( `' A " V ) )
103101, 102syl 17 . . . . . . . . . . . 12 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> ran k C_ ~P ( `' A " V ) )
104 sspwuni 4611 . . . . . . . . . . . 12 |- ( ran k C_ ~P ( `' A " V ) <-> U. ran k C_ ( `' A " V ) )
105103, 104sylib 208 . . . . . . . . . . 11 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> U. ran k C_ ( `' A " V ) )
10610ad2antrr 762 . . . . . . . . . . . 12 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> ( `' A " V ) e. S )
107106, 50syl 17 . . . . . . . . . . 11 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> ( `' A " V ) C_ U. S )
108105, 107sstrd 3613 . . . . . . . . . 10 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> U. ran k C_ U. S )
109 ffn 6045 . . . . . . . . . . . . 13 |- ( k : w --> ~P ( `' A " V ) -> k Fn w )
110 fniunfv 6505 . . . . . . . . . . . . 13 |- ( k Fn w -> U_ y e. w ( k ` y ) = U. ran k )
111101, 109, 1103syl 18 . . . . . . . . . . . 12 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> U_ y e. w ( k ` y ) = U. ran k )
112111oveq2d 6666 . . . . . . . . . . 11 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> ( S ↾t U_ y e. w ( k ` y ) ) = ( S ↾t U. ran k ) )
113 inss2 3834 . . . . . . . . . . . . 13 |- ( ~P ( S ↾t ( B " K ) ) i^i Fin ) C_ Fin
114 simplr 792 . . . . . . . . . . . . 13 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) )
115113, 114sseldi 3601 . . . . . . . . . . . 12 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> w e. Fin )
116 simprrr 805 . . . . . . . . . . . . 13 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) )
117 simpr 477 . . . . . . . . . . . . . 14 |- ( ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) -> ( S ↾t ( k ` y ) ) e. Comp )
118117ralimi 2952 . . . . . . . . . . . . 13 |- ( A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) -> A. y e. w ( S ↾t ( k ` y ) ) e. Comp )
119116, 118syl 17 . . . . . . . . . . . 12 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> A. y e. w ( S ↾t ( k ` y ) ) e. Comp )
12015fiuncmp 21207 . . . . . . . . . . . 12 |- ( ( S e. Top /\ w e. Fin /\ A. y e. w ( S ↾t ( k ` y ) ) e. Comp ) -> ( S ↾t U_ y e. w ( k ` y ) ) e. Comp )
12190, 115, 119, 120syl3anc 1326 . . . . . . . . . . 11 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> ( S ↾t U_ y e. w ( k ` y ) ) e. Comp )
122112, 121eqeltrrd 2702 . . . . . . . . . 10 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> ( S ↾t U. ran k ) e. Comp )
1238ad2antrr 762 . . . . . . . . . 10 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> V e. T )
12415, 90, 93, 108, 122, 123xkoopn 21392 . . . . . . . . 9 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } e. ( T ^ko S ) )
125 xkococn.k . . . . . . . . . . 11 |- ( ph -> K C_ U. R )
126125ad2antrr 762 . . . . . . . . . 10 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> K C_ U. R )
1272ad2antrr 762 . . . . . . . . . 10 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> ( R ↾t K ) e. Comp )
128111, 108eqsstrd 3639 . . . . . . . . . . . . 13 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> U_ y e. w ( k ` y ) C_ U. S )
129 iunss 4561 . . . . . . . . . . . . 13 |- ( U_ y e. w ( k ` y ) C_ U. S <-> A. y e. w ( k ` y ) C_ U. S )
130128, 129sylib 208 . . . . . . . . . . . 12 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> A. y e. w ( k ` y ) C_ U. S )
13115ntropn 20853 . . . . . . . . . . . . . 14 |- ( ( S e. Top /\ ( k ` y ) C_ U. S ) -> ( ( int ` S ) ` ( k ` y ) ) e. S )
132131ex 450 . . . . . . . . . . . . 13 |- ( S e. Top -> ( ( k ` y ) C_ U. S -> ( ( int ` S ) ` ( k ` y ) ) e. S ) )
133132ralimdv 2963 . . . . . . . . . . . 12 |- ( S e. Top -> ( A. y e. w ( k ` y ) C_ U. S -> A. y e. w ( ( int ` S ) ` ( k ` y ) ) e. S ) )
13490, 130, 133sylc 65 . . . . . . . . . . 11 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> A. y e. w ( ( int ` S ) ` ( k ` y ) ) e. S )
135 iunopn 20703 . . . . . . . . . . 11 |- ( ( S e. Top /\ A. y e. w ( ( int ` S ) ` ( k ` y ) ) e. S ) -> U_ y e. w ( ( int ` S ) ` ( k ` y ) ) e. S )
13690, 134, 135syl2anc 693 . . . . . . . . . 10 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> U_ y e. w ( ( int ` S ) ` ( k ` y ) ) e. S )
13721, 98, 90, 126, 127, 136xkoopn 21392 . . . . . . . . 9 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } e. ( S ^ko R ) )
138 txopn 21405 . . . . . . . . 9 |- ( ( ( ( T ^ko S ) e. Top /\ ( S ^ko R ) e. Top ) /\ ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } e. ( T ^ko S ) /\ { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } e. ( S ^ko R ) ) ) -> ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) e. ( ( T ^ko S ) tX ( S ^ko R ) ) )
13995, 100, 124, 137, 138syl22anc 1327 . . . . . . . 8 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) e. ( ( T ^ko S ) tX ( S ^ko R ) ) )
1407ad2antrr 762 . . . . . . . . . 10 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> A e. ( S Cn T ) )
141 imaiun 6503 . . . . . . . . . . . 12 |- ( A " U_ y e. w ( k ` y ) ) = U_ y e. w ( A " ( k ` y ) )
142111imaeq2d 5466 . . . . . . . . . . . 12 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> ( A " U_ y e. w ( k ` y ) ) = ( A " U. ran k ) )
143141, 142syl5eqr 2670 . . . . . . . . . . 11 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> U_ y e. w ( A " ( k ` y ) ) = ( A " U. ran k ) )
144111, 105eqsstrd 3639 . . . . . . . . . . . 12 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> U_ y e. w ( k ` y ) C_ ( `' A " V ) )
14519ad2antrr 762 . . . . . . . . . . . . 13 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> Fun A )
146101, 109syl 17 . . . . . . . . . . . . 13 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> k Fn w )
14727ad2antrr 762 . . . . . . . . . . . . . 14 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> dom A = U. S )
148108, 147sseqtr4d 3642 . . . . . . . . . . . . 13 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> U. ran k C_ dom A )
149 simpl1 1064 . . . . . . . . . . . . . . . 16 |- ( ( ( Fun A /\ k Fn w /\ U. ran k C_ dom A ) /\ y e. w ) -> Fun A )
1501103ad2ant2 1083 . . . . . . . . . . . . . . . . . . 19 |- ( ( Fun A /\ k Fn w /\ U. ran k C_ dom A ) -> U_ y e. w ( k ` y ) = U. ran k )
151 simp3 1063 . . . . . . . . . . . . . . . . . . 19 |- ( ( Fun A /\ k Fn w /\ U. ran k C_ dom A ) -> U. ran k C_ dom A )
152150, 151eqsstrd 3639 . . . . . . . . . . . . . . . . . 18 |- ( ( Fun A /\ k Fn w /\ U. ran k C_ dom A ) -> U_ y e. w ( k ` y ) C_ dom A )
153 iunss 4561 . . . . . . . . . . . . . . . . . 18 |- ( U_ y e. w ( k ` y ) C_ dom A <-> A. y e. w ( k ` y ) C_ dom A )
154152, 153sylib 208 . . . . . . . . . . . . . . . . 17 |- ( ( Fun A /\ k Fn w /\ U. ran k C_ dom A ) -> A. y e. w ( k ` y ) C_ dom A )
155154r19.21bi 2932 . . . . . . . . . . . . . . . 16 |- ( ( ( Fun A /\ k Fn w /\ U. ran k C_ dom A ) /\ y e. w ) -> ( k ` y ) C_ dom A )
156 funimass3 6333 . . . . . . . . . . . . . . . 16 |- ( ( Fun A /\ ( k ` y ) C_ dom A ) -> ( ( A " ( k ` y ) ) C_ V <-> ( k ` y ) C_ ( `' A " V ) ) )
157149, 155, 156syl2anc 693 . . . . . . . . . . . . . . 15 |- ( ( ( Fun A /\ k Fn w /\ U. ran k C_ dom A ) /\ y e. w ) -> ( ( A " ( k ` y ) ) C_ V <-> ( k ` y ) C_ ( `' A " V ) ) )
158157ralbidva 2985 . . . . . . . . . . . . . 14 |- ( ( Fun A /\ k Fn w /\ U. ran k C_ dom A ) -> ( A. y e. w ( A " ( k ` y ) ) C_ V <-> A. y e. w ( k ` y ) C_ ( `' A " V ) ) )
159 iunss 4561 . . . . . . . . . . . . . 14 |- ( U_ y e. w ( A " ( k ` y ) ) C_ V <-> A. y e. w ( A " ( k ` y ) ) C_ V )
160 iunss 4561 . . . . . . . . . . . . . 14 |- ( U_ y e. w ( k ` y ) C_ ( `' A " V ) <-> A. y e. w ( k ` y ) C_ ( `' A " V ) )
161158, 159, 1603bitr4g 303 . . . . . . . . . . . . 13 |- ( ( Fun A /\ k Fn w /\ U. ran k C_ dom A ) -> ( U_ y e. w ( A " ( k ` y ) ) C_ V <-> U_ y e. w ( k ` y ) C_ ( `' A " V ) ) )
162145, 146, 148, 161syl3anc 1326 . . . . . . . . . . . 12 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> ( U_ y e. w ( A " ( k ` y ) ) C_ V <-> U_ y e. w ( k ` y ) C_ ( `' A " V ) ) )
163144, 162mpbird 247 . . . . . . . . . . 11 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> U_ y e. w ( A " ( k ` y ) ) C_ V )
164143, 163eqsstr3d 3640 . . . . . . . . . 10 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> ( A " U. ran k ) C_ V )
165 imaeq1 5461 . . . . . . . . . . . 12 |- ( a = A -> ( a " U. ran k ) = ( A " U. ran k ) )
166165sseq1d 3632 . . . . . . . . . . 11 |- ( a = A -> ( ( a " U. ran k ) C_ V <-> ( A " U. ran k ) C_ V ) )
167166elrab 3363 . . . . . . . . . 10 |- ( A e. { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } <-> ( A e. ( S Cn T ) /\ ( A " U. ran k ) C_ V ) )
168140, 164, 167sylanbrc 698 . . . . . . . . 9 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> A e. { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } )
1691ad2antrr 762 . . . . . . . . . 10 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> B e. ( R Cn S ) )
170 simprl 794 . . . . . . . . . . . 12 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> ( B " K ) = U. w )
171 uniiun 4573 . . . . . . . . . . . 12 |- U. w = U_ y e. w y
172170, 171syl6eq 2672 . . . . . . . . . . 11 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> ( B " K ) = U_ y e. w y )
173 simpl 473 . . . . . . . . . . . . 13 |- ( ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) -> y C_ ( ( int ` S ) ` ( k ` y ) ) )
174173ralimi 2952 . . . . . . . . . . . 12 |- ( A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) -> A. y e. w y C_ ( ( int ` S ) ` ( k ` y ) ) )
175 ss2iun 4536 . . . . . . . . . . . 12 |- ( A. y e. w y C_ ( ( int ` S ) ` ( k ` y ) ) -> U_ y e. w y C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) )
176116, 174, 1753syl 18 . . . . . . . . . . 11 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> U_ y e. w y C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) )
177172, 176eqsstrd 3639 . . . . . . . . . 10 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> ( B " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) )
178 imaeq1 5461 . . . . . . . . . . . 12 |- ( b = B -> ( b " K ) = ( B " K ) )
179178sseq1d 3632 . . . . . . . . . . 11 |- ( b = B -> ( ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) <-> ( B " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) ) )
180179elrab 3363 . . . . . . . . . 10 |- ( B e. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } <-> ( B e. ( R Cn S ) /\ ( B " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) ) )
181169, 177, 180sylanbrc 698 . . . . . . . . 9 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> B e. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } )
182 opelxpi 5148 . . . . . . . . 9 |- ( ( A e. { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } /\ B e. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) -> <. A , B >. e. ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) )
183168, 181, 182syl2anc 693 . . . . . . . 8 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> <. A , B >. e. ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) )
184 imaeq1 5461 . . . . . . . . . . . . . . 15 |- ( a = u -> ( a " U. ran k ) = ( u " U. ran k ) )
185184sseq1d 3632 . . . . . . . . . . . . . 14 |- ( a = u -> ( ( a " U. ran k ) C_ V <-> ( u " U. ran k ) C_ V ) )
186185elrab 3363 . . . . . . . . . . . . 13 |- ( u e. { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } <-> ( u e. ( S Cn T ) /\ ( u " U. ran k ) C_ V ) )
187 imaeq1 5461 . . . . . . . . . . . . . . 15 |- ( b = v -> ( b " K ) = ( v " K ) )
188187sseq1d 3632 . . . . . . . . . . . . . 14 |- ( b = v -> ( ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) <-> ( v " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) ) )
189188elrab 3363 . . . . . . . . . . . . 13 |- ( v e. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } <-> ( v e. ( R Cn S ) /\ ( v " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) ) )
190186, 189anbi12i 733 . . . . . . . . . . . 12 |- ( ( u e. { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } /\ v e. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) <-> ( ( u e. ( S Cn T ) /\ ( u " U. ran k ) C_ V ) /\ ( v e. ( R Cn S ) /\ ( v " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) ) ) )
191 simprll 802 . . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) /\ ( ( u e. ( S Cn T ) /\ ( u " U. ran k ) C_ V ) /\ ( v e. ( R Cn S ) /\ ( v " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) ) ) ) -> u e. ( S Cn T ) )
192 simprrl 804 . . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) /\ ( ( u e. ( S Cn T ) /\ ( u " U. ran k ) C_ V ) /\ ( v e. ( R Cn S ) /\ ( v " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) ) ) ) -> v e. ( R Cn S ) )
193 coeq1 5279 . . . . . . . . . . . . . . 15 |- ( f = u -> ( f o. g ) = ( u o. g ) )
194 coeq2 5280 . . . . . . . . . . . . . . 15 |- ( g = v -> ( u o. g ) = ( u o. v ) )
195 xkococn.1 . . . . . . . . . . . . . . 15 |- F = ( f e. ( S Cn T ) , g e. ( R Cn S ) |-> ( f o. g ) )
196 vex 3203 . . . . . . . . . . . . . . . 16 |- u e. _V
197 vex 3203 . . . . . . . . . . . . . . . 16 |- v e. _V
198196, 197coex 7118 . . . . . . . . . . . . . . 15 |- ( u o. v ) e. _V
199193, 194, 195, 198ovmpt2 6796 . . . . . . . . . . . . . 14 |- ( ( u e. ( S Cn T ) /\ v e. ( R Cn S ) ) -> ( u F v ) = ( u o. v ) )
200191, 192, 199syl2anc 693 . . . . . . . . . . . . 13 |- ( ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) /\ ( ( u e. ( S Cn T ) /\ ( u " U. ran k ) C_ V ) /\ ( v e. ( R Cn S ) /\ ( v " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) ) ) ) -> ( u F v ) = ( u o. v ) )
201 cnco 21070 . . . . . . . . . . . . . . 15 |- ( ( v e. ( R Cn S ) /\ u e. ( S Cn T ) ) -> ( u o. v ) e. ( R Cn T ) )
202192, 191, 201syl2anc 693 . . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) /\ ( ( u e. ( S Cn T ) /\ ( u " U. ran k ) C_ V ) /\ ( v e. ( R Cn S ) /\ ( v " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) ) ) ) -> ( u o. v ) e. ( R Cn T ) )
203 imaco 5640 . . . . . . . . . . . . . . 15 |- ( ( u o. v ) " K ) = ( u " ( v " K ) )
204 simprrr 805 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) /\ ( ( u e. ( S Cn T ) /\ ( u " U. ran k ) C_ V ) /\ ( v e. ( R Cn S ) /\ ( v " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) ) ) ) -> ( v " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) )
20515ntrss2 20861 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( S e. Top /\ ( k ` y ) C_ U. S ) -> ( ( int ` S ) ` ( k ` y ) ) C_ ( k ` y ) )
206205ex 450 . . . . . . . . . . . . . . . . . . . . . . 23 |- ( S e. Top -> ( ( k ` y ) C_ U. S -> ( ( int ` S ) ` ( k ` y ) ) C_ ( k ` y ) ) )
207206ralimdv 2963 . . . . . . . . . . . . . . . . . . . . . 22 |- ( S e. Top -> ( A. y e. w ( k ` y ) C_ U. S -> A. y e. w ( ( int ` S ) ` ( k ` y ) ) C_ ( k ` y ) ) )
20890, 130, 207sylc 65 . . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> A. y e. w ( ( int ` S ) ` ( k ` y ) ) C_ ( k ` y ) )
209 ss2iun 4536 . . . . . . . . . . . . . . . . . . . . 21 |- ( A. y e. w ( ( int ` S ) ` ( k ` y ) ) C_ ( k ` y ) -> U_ y e. w ( ( int ` S ) ` ( k ` y ) ) C_ U_ y e. w ( k ` y ) )
210208, 209syl 17 . . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> U_ y e. w ( ( int ` S ) ` ( k ` y ) ) C_ U_ y e. w ( k ` y ) )
211210, 111sseqtrd 3641 . . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> U_ y e. w ( ( int ` S ) ` ( k ` y ) ) C_ U. ran k )
212211adantr 481 . . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) /\ ( ( u e. ( S Cn T ) /\ ( u " U. ran k ) C_ V ) /\ ( v e. ( R Cn S ) /\ ( v " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) ) ) ) -> U_ y e. w ( ( int ` S ) ` ( k ` y ) ) C_ U. ran k )
213204, 212sstrd 3613 . . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) /\ ( ( u e. ( S Cn T ) /\ ( u " U. ran k ) C_ V ) /\ ( v e. ( R Cn S ) /\ ( v " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) ) ) ) -> ( v " K ) C_ U. ran k )
214 imass2 5501 . . . . . . . . . . . . . . . . 17 |- ( ( v " K ) C_ U. ran k -> ( u " ( v " K ) ) C_ ( u " U. ran k ) )
215213, 214syl 17 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) /\ ( ( u e. ( S Cn T ) /\ ( u " U. ran k ) C_ V ) /\ ( v e. ( R Cn S ) /\ ( v " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) ) ) ) -> ( u " ( v " K ) ) C_ ( u " U. ran k ) )
216 simprlr 803 . . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) /\ ( ( u e. ( S Cn T ) /\ ( u " U. ran k ) C_ V ) /\ ( v e. ( R Cn S ) /\ ( v " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) ) ) ) -> ( u " U. ran k ) C_ V )
217215, 216sstrd 3613 . . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) /\ ( ( u e. ( S Cn T ) /\ ( u " U. ran k ) C_ V ) /\ ( v e. ( R Cn S ) /\ ( v " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) ) ) ) -> ( u " ( v " K ) ) C_ V )
218203, 217syl5eqss 3649 . . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) /\ ( ( u e. ( S Cn T ) /\ ( u " U. ran k ) C_ V ) /\ ( v e. ( R Cn S ) /\ ( v " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) ) ) ) -> ( ( u o. v ) " K ) C_ V )
219 imaeq1 5461 . . . . . . . . . . . . . . . 16 |- ( h = ( u o. v ) -> ( h " K ) = ( ( u o. v ) " K ) )
220219sseq1d 3632 . . . . . . . . . . . . . . 15 |- ( h = ( u o. v ) -> ( ( h " K ) C_ V <-> ( ( u o. v ) " K ) C_ V ) )
221220elrab 3363 . . . . . . . . . . . . . 14 |- ( ( u o. v ) e. { h e. ( R Cn T ) | ( h " K ) C_ V } <-> ( ( u o. v ) e. ( R Cn T ) /\ ( ( u o. v ) " K ) C_ V ) )
222202, 218, 221sylanbrc 698 . . . . . . . . . . . . 13 |- ( ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) /\ ( ( u e. ( S Cn T ) /\ ( u " U. ran k ) C_ V ) /\ ( v e. ( R Cn S ) /\ ( v " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) ) ) ) -> ( u o. v ) e. { h e. ( R Cn T ) | ( h " K ) C_ V } )
223200, 222eqeltrd 2701 . . . . . . . . . . . 12 |- ( ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) /\ ( ( u e. ( S Cn T ) /\ ( u " U. ran k ) C_ V ) /\ ( v e. ( R Cn S ) /\ ( v " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) ) ) ) -> ( u F v ) e. { h e. ( R Cn T ) | ( h " K ) C_ V } )
224190, 223sylan2b 492 . . . . . . . . . . 11 |- ( ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) /\ ( u e. { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } /\ v e. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) ) -> ( u F v ) e. { h e. ( R Cn T ) | ( h " K ) C_ V } )
225224ralrimivva 2971 . . . . . . . . . 10 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> A. u e. { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } A. v e. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ( u F v ) e. { h e. ( R Cn T ) | ( h " K ) C_ V } )
226195mpt2fun 6762 . . . . . . . . . . 11 |- Fun F
227 ssrab2 3687 . . . . . . . . . . . . 13 |- { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } C_ ( S Cn T )
228 ssrab2 3687 . . . . . . . . . . . . 13 |- { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } C_ ( R Cn S )
229 xpss12 5225 . . . . . . . . . . . . 13 |- ( ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } C_ ( S Cn T ) /\ { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } C_ ( R Cn S ) ) -> ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) C_ ( ( S Cn T ) X. ( R Cn S ) ) )
230227, 228, 229mp2an 708 . . . . . . . . . . . 12 |- ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) C_ ( ( S Cn T ) X. ( R Cn S ) )
231 vex 3203 . . . . . . . . . . . . . 14 |- f e. _V
232 vex 3203 . . . . . . . . . . . . . 14 |- g e. _V
233231, 232coex 7118 . . . . . . . . . . . . 13 |- ( f o. g ) e. _V
234195, 233dmmpt2 7240 . . . . . . . . . . . 12 |- dom F = ( ( S Cn T ) X. ( R Cn S ) )
235230, 234sseqtr4i 3638 . . . . . . . . . . 11 |- ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) C_ dom F
236 funimassov 6811 . . . . . . . . . . 11 |- ( ( Fun F /\ ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) C_ dom F ) -> ( ( F " ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) ) C_ { h e. ( R Cn T ) | ( h " K ) C_ V } <-> A. u e. { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } A. v e. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ( u F v ) e. { h e. ( R Cn T ) | ( h " K ) C_ V } ) )
237226, 235, 236mp2an 708 . . . . . . . . . 10 |- ( ( F " ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) ) C_ { h e. ( R Cn T ) | ( h " K ) C_ V } <-> A. u e. { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } A. v e. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ( u F v ) e. { h e. ( R Cn T ) | ( h " K ) C_ V } )
238225, 237sylibr 224 . . . . . . . . 9 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> ( F " ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) ) C_ { h e. ( R Cn T ) | ( h " K ) C_ V } )
239 funimass3 6333 . . . . . . . . . 10 |- ( ( Fun F /\ ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) C_ dom F ) -> ( ( F " ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) ) C_ { h e. ( R Cn T ) | ( h " K ) C_ V } <-> ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) C_ ( `' F " { h e. ( R Cn T ) | ( h " K ) C_ V } ) ) )
240226, 235, 239mp2an 708 . . . . . . . . 9 |- ( ( F " ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) ) C_ { h e. ( R Cn T ) | ( h " K ) C_ V } <-> ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) C_ ( `' F " { h e. ( R Cn T ) | ( h " K ) C_ V } ) )
241238, 240sylib 208 . . . . . . . 8 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) C_ ( `' F " { h e. ( R Cn T ) | ( h " K ) C_ V } ) )
242 eleq2 2690 . . . . . . . . . 10 |- ( z = ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) -> ( <. A , B >. e. z <-> <. A , B >. e. ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) ) )
243 sseq1 3626 . . . . . . . . . 10 |- ( z = ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) -> ( z C_ ( `' F " { h e. ( R Cn T ) | ( h " K ) C_ V } ) <-> ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) C_ ( `' F " { h e. ( R Cn T ) | ( h " K ) C_ V } ) ) )
244242, 243anbi12d 747 . . . . . . . . 9 |- ( z = ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) -> ( ( <. A , B >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " K ) C_ V } ) ) <-> ( <. A , B >. e. ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) /\ ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) C_ ( `' F " { h e. ( R Cn T ) | ( h " K ) C_ V } ) ) ) )
245244rspcev 3309 . . . . . . . 8 |- ( ( ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) e. ( ( T ^ko S ) tX ( S ^ko R ) ) /\ ( <. A , B >. e. ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) /\ ( { a e. ( S Cn T ) | ( a " U. ran k ) C_ V } X. { b e. ( R Cn S ) | ( b " K ) C_ U_ y e. w ( ( int ` S ) ` ( k ` y ) ) } ) C_ ( `' F " { h e. ( R Cn T ) | ( h " K ) C_ V } ) ) ) -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( <. A , B >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " K ) C_ V } ) ) )
246139, 183, 241, 245syl12anc 1324 . . . . . . 7 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( ( B " K ) = U. w /\ ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) ) -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( <. A , B >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " K ) C_ V } ) ) )
247246expr 643 . . . . . 6 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( B " K ) = U. w ) -> ( ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( <. A , B >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " K ) C_ V } ) ) ) )
248247exlimdv 1861 . . . . 5 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ ( B " K ) = U. w ) -> ( E. k ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( <. A , B >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " K ) C_ V } ) ) ) )
24989, 248syldan 487 . . . 4 |- ( ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) /\ U. ( S ↾t ( B " K ) ) = U. w ) -> ( E. k ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( <. A , B >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " K ) C_ V } ) ) ) )
250249expimpd 629 . . 3 |- ( ( ph /\ w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ) -> ( ( U. ( S ↾t ( B " K ) ) = U. w /\ E. k ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( <. A , B >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " K ) C_ V } ) ) ) )
251250rexlimdva 3031 . 2 |- ( ph -> ( E. w e. ( ~P ( S ↾t ( B " K ) ) i^i Fin ) ( U. ( S ↾t ( B " K ) ) = U. w /\ E. k ( k : w --> ~P ( `' A " V ) /\ A. y e. w ( y C_ ( ( int ` S ) ` ( k ` y ) ) /\ ( S ↾t ( k ` y ) ) e. Comp ) ) ) -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( <. A , B >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " K ) C_ V } ) ) ) )
25286, 251mpd 15 1 |- ( ph -> E. z e. ( ( T ^ko S ) tX ( S ^ko R ) ) ( <. A , B >. e. z /\ z C_ ( `' F " { h e. ( R Cn T ) | ( h " K ) C_ V } ) ) )
Colors of variables: wff setvar class
Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   E.wex 1704   e. wcel 1990   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   i^i cin 3573   C_ wss 3574   ~Pcpw 4158   <.cop 4183   U.cuni 4436   U_ciun 4520   X. cxp 5112   `'ccnv 5113   dom cdm 5114   ran crn 5115   "cima 5117   o. ccom 5118   Fun wfun 5882   Fn wfn 5883   -->wf 5884   ` cfv 5888  (class class class)co 6650   |-> cmpt2 6652   Fincfn 7955   ↾t crest 16081   Topctop 20698   intcnt 20821   Cn ccn 21028   Compccmp 21189  𝑛Locally cnlly 21268   tX ctx 21363   ^ko cxko 21364
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-fin 7959  df-fi 8317  df-rest 16083  df-topgen 16104  df-top 20699  df-topon 20716  df-bases 20750  df-ntr 20824  df-nei 20902  df-cn 21031  df-cmp 21190  df-nlly 21270  df-tx 21365  df-xko 21366
This theorem is referenced by:  xkococn  21463
  Copyright terms: Public domain W3C validator