Step |
Hyp |
Ref |
Expression |
1 |
|
stoweidlem50.1 |
|- F/_ t U |
2 |
|
stoweidlem50.2 |
|- F/ t ph |
3 |
|
stoweidlem50.3 |
|- K = ( topGen ` ran (,) ) |
4 |
|
stoweidlem50.4 |
|- Q = { h e. A | ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) } |
5 |
|
stoweidlem50.5 |
|- W = { w e. J | E. h e. Q w = { t e. T | 0 < ( h ` t ) } } |
6 |
|
stoweidlem50.6 |
|- T = U. J |
7 |
|
stoweidlem50.7 |
|- C = ( J Cn K ) |
8 |
|
stoweidlem50.8 |
|- ( ph -> J e. Comp ) |
9 |
|
stoweidlem50.9 |
|- ( ph -> A C_ C ) |
10 |
|
stoweidlem50.10 |
|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A ) |
11 |
|
stoweidlem50.11 |
|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A ) |
12 |
|
stoweidlem50.12 |
|- ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A ) |
13 |
|
stoweidlem50.13 |
|- ( ( ph /\ ( r e. T /\ t e. T /\ r =/= t ) ) -> E. q e. A ( q ` r ) =/= ( q ` t ) ) |
14 |
|
stoweidlem50.14 |
|- ( ph -> U e. J ) |
15 |
|
stoweidlem50.15 |
|- ( ph -> Z e. U ) |
16 |
|
nfrab1 |
|- F/_ h { h e. A | ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) } |
17 |
4 16
|
nfcxfr |
|- F/_ h Q |
18 |
|
nfv |
|- F/ q ph |
19 |
9 7
|
sseqtrdi |
|- ( ph -> A C_ ( J Cn K ) ) |
20 |
8
|
uniexd |
|- ( ph -> U. J e. _V ) |
21 |
6 20
|
eqeltrid |
|- ( ph -> T e. _V ) |
22 |
1 17 18 2 3 4 5 6 8 19 10 11 12 13 14 15 21
|
stoweidlem46 |
|- ( ph -> ( T \ U ) C_ U. W ) |
23 |
|
dfin4 |
|- ( T i^i U ) = ( T \ ( T \ U ) ) |
24 |
|
elssuni |
|- ( U e. J -> U C_ U. J ) |
25 |
14 24
|
syl |
|- ( ph -> U C_ U. J ) |
26 |
25 6
|
sseqtrrdi |
|- ( ph -> U C_ T ) |
27 |
|
sseqin2 |
|- ( U C_ T <-> ( T i^i U ) = U ) |
28 |
26 27
|
sylib |
|- ( ph -> ( T i^i U ) = U ) |
29 |
23 28
|
syl5eqr |
|- ( ph -> ( T \ ( T \ U ) ) = U ) |
30 |
29 14
|
eqeltrd |
|- ( ph -> ( T \ ( T \ U ) ) e. J ) |
31 |
|
cmptop |
|- ( J e. Comp -> J e. Top ) |
32 |
8 31
|
syl |
|- ( ph -> J e. Top ) |
33 |
|
difssd |
|- ( ph -> ( T \ U ) C_ T ) |
34 |
6
|
iscld2 |
|- ( ( J e. Top /\ ( T \ U ) C_ T ) -> ( ( T \ U ) e. ( Clsd ` J ) <-> ( T \ ( T \ U ) ) e. J ) ) |
35 |
32 33 34
|
syl2anc |
|- ( ph -> ( ( T \ U ) e. ( Clsd ` J ) <-> ( T \ ( T \ U ) ) e. J ) ) |
36 |
30 35
|
mpbird |
|- ( ph -> ( T \ U ) e. ( Clsd ` J ) ) |
37 |
|
cmpcld |
|- ( ( J e. Comp /\ ( T \ U ) e. ( Clsd ` J ) ) -> ( J |`t ( T \ U ) ) e. Comp ) |
38 |
8 36 37
|
syl2anc |
|- ( ph -> ( J |`t ( T \ U ) ) e. Comp ) |
39 |
6
|
cmpsub |
|- ( ( J e. Top /\ ( T \ U ) C_ T ) -> ( ( J |`t ( T \ U ) ) e. Comp <-> A. c e. ~P J ( ( T \ U ) C_ U. c -> E. u e. ( ~P c i^i Fin ) ( T \ U ) C_ U. u ) ) ) |
40 |
32 33 39
|
syl2anc |
|- ( ph -> ( ( J |`t ( T \ U ) ) e. Comp <-> A. c e. ~P J ( ( T \ U ) C_ U. c -> E. u e. ( ~P c i^i Fin ) ( T \ U ) C_ U. u ) ) ) |
41 |
38 40
|
mpbid |
|- ( ph -> A. c e. ~P J ( ( T \ U ) C_ U. c -> E. u e. ( ~P c i^i Fin ) ( T \ U ) C_ U. u ) ) |
42 |
|
ssrab2 |
|- { w e. J | E. h e. Q w = { t e. T | 0 < ( h ` t ) } } C_ J |
43 |
5 42
|
eqsstri |
|- W C_ J |
44 |
5 8
|
rabexd |
|- ( ph -> W e. _V ) |
45 |
|
elpwg |
|- ( W e. _V -> ( W e. ~P J <-> W C_ J ) ) |
46 |
44 45
|
syl |
|- ( ph -> ( W e. ~P J <-> W C_ J ) ) |
47 |
43 46
|
mpbiri |
|- ( ph -> W e. ~P J ) |
48 |
|
unieq |
|- ( c = W -> U. c = U. W ) |
49 |
48
|
sseq2d |
|- ( c = W -> ( ( T \ U ) C_ U. c <-> ( T \ U ) C_ U. W ) ) |
50 |
|
pweq |
|- ( c = W -> ~P c = ~P W ) |
51 |
50
|
ineq1d |
|- ( c = W -> ( ~P c i^i Fin ) = ( ~P W i^i Fin ) ) |
52 |
51
|
rexeqdv |
|- ( c = W -> ( E. u e. ( ~P c i^i Fin ) ( T \ U ) C_ U. u <-> E. u e. ( ~P W i^i Fin ) ( T \ U ) C_ U. u ) ) |
53 |
49 52
|
imbi12d |
|- ( c = W -> ( ( ( T \ U ) C_ U. c -> E. u e. ( ~P c i^i Fin ) ( T \ U ) C_ U. u ) <-> ( ( T \ U ) C_ U. W -> E. u e. ( ~P W i^i Fin ) ( T \ U ) C_ U. u ) ) ) |
54 |
53
|
rspccva |
|- ( ( A. c e. ~P J ( ( T \ U ) C_ U. c -> E. u e. ( ~P c i^i Fin ) ( T \ U ) C_ U. u ) /\ W e. ~P J ) -> ( ( T \ U ) C_ U. W -> E. u e. ( ~P W i^i Fin ) ( T \ U ) C_ U. u ) ) |
55 |
41 47 54
|
syl2anc |
|- ( ph -> ( ( T \ U ) C_ U. W -> E. u e. ( ~P W i^i Fin ) ( T \ U ) C_ U. u ) ) |
56 |
55
|
imp |
|- ( ( ph /\ ( T \ U ) C_ U. W ) -> E. u e. ( ~P W i^i Fin ) ( T \ U ) C_ U. u ) |
57 |
|
df-rex |
|- ( E. u e. ( ~P W i^i Fin ) ( T \ U ) C_ U. u <-> E. u ( u e. ( ~P W i^i Fin ) /\ ( T \ U ) C_ U. u ) ) |
58 |
56 57
|
sylib |
|- ( ( ph /\ ( T \ U ) C_ U. W ) -> E. u ( u e. ( ~P W i^i Fin ) /\ ( T \ U ) C_ U. u ) ) |
59 |
|
elinel2 |
|- ( u e. ( ~P W i^i Fin ) -> u e. Fin ) |
60 |
59
|
ad2antrl |
|- ( ( ( ph /\ ( T \ U ) C_ U. W ) /\ ( u e. ( ~P W i^i Fin ) /\ ( T \ U ) C_ U. u ) ) -> u e. Fin ) |
61 |
|
elinel1 |
|- ( u e. ( ~P W i^i Fin ) -> u e. ~P W ) |
62 |
61
|
ad2antrl |
|- ( ( ( ph /\ ( T \ U ) C_ U. W ) /\ ( u e. ( ~P W i^i Fin ) /\ ( T \ U ) C_ U. u ) ) -> u e. ~P W ) |
63 |
62
|
elpwid |
|- ( ( ( ph /\ ( T \ U ) C_ U. W ) /\ ( u e. ( ~P W i^i Fin ) /\ ( T \ U ) C_ U. u ) ) -> u C_ W ) |
64 |
|
simprr |
|- ( ( ( ph /\ ( T \ U ) C_ U. W ) /\ ( u e. ( ~P W i^i Fin ) /\ ( T \ U ) C_ U. u ) ) -> ( T \ U ) C_ U. u ) |
65 |
60 63 64
|
3jca |
|- ( ( ( ph /\ ( T \ U ) C_ U. W ) /\ ( u e. ( ~P W i^i Fin ) /\ ( T \ U ) C_ U. u ) ) -> ( u e. Fin /\ u C_ W /\ ( T \ U ) C_ U. u ) ) |
66 |
65
|
ex |
|- ( ( ph /\ ( T \ U ) C_ U. W ) -> ( ( u e. ( ~P W i^i Fin ) /\ ( T \ U ) C_ U. u ) -> ( u e. Fin /\ u C_ W /\ ( T \ U ) C_ U. u ) ) ) |
67 |
66
|
eximdv |
|- ( ( ph /\ ( T \ U ) C_ U. W ) -> ( E. u ( u e. ( ~P W i^i Fin ) /\ ( T \ U ) C_ U. u ) -> E. u ( u e. Fin /\ u C_ W /\ ( T \ U ) C_ U. u ) ) ) |
68 |
58 67
|
mpd |
|- ( ( ph /\ ( T \ U ) C_ U. W ) -> E. u ( u e. Fin /\ u C_ W /\ ( T \ U ) C_ U. u ) ) |
69 |
22 68
|
mpdan |
|- ( ph -> E. u ( u e. Fin /\ u C_ W /\ ( T \ U ) C_ U. u ) ) |