Step |
Hyp |
Ref |
Expression |
1 |
|
bwt2.1 |
|- X = U. J |
2 |
|
pm3.24 |
|- -. ( ( A i^i b ) e. Fin /\ -. ( A i^i b ) e. Fin ) |
3 |
2
|
a1i |
|- ( b e. z -> -. ( ( A i^i b ) e. Fin /\ -. ( A i^i b ) e. Fin ) ) |
4 |
3
|
nrex |
|- -. E. b e. z ( ( A i^i b ) e. Fin /\ -. ( A i^i b ) e. Fin ) |
5 |
|
r19.29 |
|- ( ( A. b e. z ( A i^i b ) e. Fin /\ E. b e. z -. ( A i^i b ) e. Fin ) -> E. b e. z ( ( A i^i b ) e. Fin /\ -. ( A i^i b ) e. Fin ) ) |
6 |
4 5
|
mto |
|- -. ( A. b e. z ( A i^i b ) e. Fin /\ E. b e. z -. ( A i^i b ) e. Fin ) |
7 |
6
|
a1i |
|- ( z e. ( ~P J i^i Fin ) -> -. ( A. b e. z ( A i^i b ) e. Fin /\ E. b e. z -. ( A i^i b ) e. Fin ) ) |
8 |
7
|
nrex |
|- -. E. z e. ( ~P J i^i Fin ) ( A. b e. z ( A i^i b ) e. Fin /\ E. b e. z -. ( A i^i b ) e. Fin ) |
9 |
|
ralnex |
|- ( A. x e. X -. x e. ( ( limPt ` J ) ` A ) <-> -. E. x e. X x e. ( ( limPt ` J ) ` A ) ) |
10 |
|
cmptop |
|- ( J e. Comp -> J e. Top ) |
11 |
1
|
islp3 |
|- ( ( J e. Top /\ A C_ X /\ x e. X ) -> ( x e. ( ( limPt ` J ) ` A ) <-> A. b e. J ( x e. b -> ( b i^i ( A \ { x } ) ) =/= (/) ) ) ) |
12 |
11
|
3expa |
|- ( ( ( J e. Top /\ A C_ X ) /\ x e. X ) -> ( x e. ( ( limPt ` J ) ` A ) <-> A. b e. J ( x e. b -> ( b i^i ( A \ { x } ) ) =/= (/) ) ) ) |
13 |
12
|
notbid |
|- ( ( ( J e. Top /\ A C_ X ) /\ x e. X ) -> ( -. x e. ( ( limPt ` J ) ` A ) <-> -. A. b e. J ( x e. b -> ( b i^i ( A \ { x } ) ) =/= (/) ) ) ) |
14 |
13
|
ralbidva |
|- ( ( J e. Top /\ A C_ X ) -> ( A. x e. X -. x e. ( ( limPt ` J ) ` A ) <-> A. x e. X -. A. b e. J ( x e. b -> ( b i^i ( A \ { x } ) ) =/= (/) ) ) ) |
15 |
10 14
|
sylan |
|- ( ( J e. Comp /\ A C_ X ) -> ( A. x e. X -. x e. ( ( limPt ` J ) ` A ) <-> A. x e. X -. A. b e. J ( x e. b -> ( b i^i ( A \ { x } ) ) =/= (/) ) ) ) |
16 |
9 15
|
bitr3id |
|- ( ( J e. Comp /\ A C_ X ) -> ( -. E. x e. X x e. ( ( limPt ` J ) ` A ) <-> A. x e. X -. A. b e. J ( x e. b -> ( b i^i ( A \ { x } ) ) =/= (/) ) ) ) |
17 |
|
rexanali |
|- ( E. b e. J ( x e. b /\ -. ( b i^i ( A \ { x } ) ) =/= (/) ) <-> -. A. b e. J ( x e. b -> ( b i^i ( A \ { x } ) ) =/= (/) ) ) |
18 |
|
nne |
|- ( -. ( b i^i ( A \ { x } ) ) =/= (/) <-> ( b i^i ( A \ { x } ) ) = (/) ) |
19 |
|
vex |
|- x e. _V |
20 |
|
sneq |
|- ( o = x -> { o } = { x } ) |
21 |
20
|
difeq2d |
|- ( o = x -> ( A \ { o } ) = ( A \ { x } ) ) |
22 |
21
|
ineq2d |
|- ( o = x -> ( b i^i ( A \ { o } ) ) = ( b i^i ( A \ { x } ) ) ) |
23 |
22
|
eqeq1d |
|- ( o = x -> ( ( b i^i ( A \ { o } ) ) = (/) <-> ( b i^i ( A \ { x } ) ) = (/) ) ) |
24 |
19 23
|
spcev |
|- ( ( b i^i ( A \ { x } ) ) = (/) -> E. o ( b i^i ( A \ { o } ) ) = (/) ) |
25 |
18 24
|
sylbi |
|- ( -. ( b i^i ( A \ { x } ) ) =/= (/) -> E. o ( b i^i ( A \ { o } ) ) = (/) ) |
26 |
25
|
anim2i |
|- ( ( x e. b /\ -. ( b i^i ( A \ { x } ) ) =/= (/) ) -> ( x e. b /\ E. o ( b i^i ( A \ { o } ) ) = (/) ) ) |
27 |
26
|
reximi |
|- ( E. b e. J ( x e. b /\ -. ( b i^i ( A \ { x } ) ) =/= (/) ) -> E. b e. J ( x e. b /\ E. o ( b i^i ( A \ { o } ) ) = (/) ) ) |
28 |
17 27
|
sylbir |
|- ( -. A. b e. J ( x e. b -> ( b i^i ( A \ { x } ) ) =/= (/) ) -> E. b e. J ( x e. b /\ E. o ( b i^i ( A \ { o } ) ) = (/) ) ) |
29 |
28
|
ralimi |
|- ( A. x e. X -. A. b e. J ( x e. b -> ( b i^i ( A \ { x } ) ) =/= (/) ) -> A. x e. X E. b e. J ( x e. b /\ E. o ( b i^i ( A \ { o } ) ) = (/) ) ) |
30 |
1
|
cmpcov2 |
|- ( ( J e. Comp /\ A. x e. X E. b e. J ( x e. b /\ E. o ( b i^i ( A \ { o } ) ) = (/) ) ) -> E. z e. ( ~P J i^i Fin ) ( X = U. z /\ A. b e. z E. o ( b i^i ( A \ { o } ) ) = (/) ) ) |
31 |
30
|
ex |
|- ( J e. Comp -> ( A. x e. X E. b e. J ( x e. b /\ E. o ( b i^i ( A \ { o } ) ) = (/) ) -> E. z e. ( ~P J i^i Fin ) ( X = U. z /\ A. b e. z E. o ( b i^i ( A \ { o } ) ) = (/) ) ) ) |
32 |
29 31
|
syl5 |
|- ( J e. Comp -> ( A. x e. X -. A. b e. J ( x e. b -> ( b i^i ( A \ { x } ) ) =/= (/) ) -> E. z e. ( ~P J i^i Fin ) ( X = U. z /\ A. b e. z E. o ( b i^i ( A \ { o } ) ) = (/) ) ) ) |
33 |
32
|
adantr |
|- ( ( J e. Comp /\ A C_ X ) -> ( A. x e. X -. A. b e. J ( x e. b -> ( b i^i ( A \ { x } ) ) =/= (/) ) -> E. z e. ( ~P J i^i Fin ) ( X = U. z /\ A. b e. z E. o ( b i^i ( A \ { o } ) ) = (/) ) ) ) |
34 |
16 33
|
sylbid |
|- ( ( J e. Comp /\ A C_ X ) -> ( -. E. x e. X x e. ( ( limPt ` J ) ` A ) -> E. z e. ( ~P J i^i Fin ) ( X = U. z /\ A. b e. z E. o ( b i^i ( A \ { o } ) ) = (/) ) ) ) |
35 |
34
|
3adant3 |
|- ( ( J e. Comp /\ A C_ X /\ -. A e. Fin ) -> ( -. E. x e. X x e. ( ( limPt ` J ) ` A ) -> E. z e. ( ~P J i^i Fin ) ( X = U. z /\ A. b e. z E. o ( b i^i ( A \ { o } ) ) = (/) ) ) ) |
36 |
|
elinel2 |
|- ( z e. ( ~P J i^i Fin ) -> z e. Fin ) |
37 |
|
sseq2 |
|- ( X = U. z -> ( A C_ X <-> A C_ U. z ) ) |
38 |
37
|
biimpac |
|- ( ( A C_ X /\ X = U. z ) -> A C_ U. z ) |
39 |
|
infssuni |
|- ( ( -. A e. Fin /\ z e. Fin /\ A C_ U. z ) -> E. b e. z -. ( A i^i b ) e. Fin ) |
40 |
39
|
3expa |
|- ( ( ( -. A e. Fin /\ z e. Fin ) /\ A C_ U. z ) -> E. b e. z -. ( A i^i b ) e. Fin ) |
41 |
40
|
ancoms |
|- ( ( A C_ U. z /\ ( -. A e. Fin /\ z e. Fin ) ) -> E. b e. z -. ( A i^i b ) e. Fin ) |
42 |
38 41
|
sylan |
|- ( ( ( A C_ X /\ X = U. z ) /\ ( -. A e. Fin /\ z e. Fin ) ) -> E. b e. z -. ( A i^i b ) e. Fin ) |
43 |
42
|
an42s |
|- ( ( ( A C_ X /\ -. A e. Fin ) /\ ( z e. Fin /\ X = U. z ) ) -> E. b e. z -. ( A i^i b ) e. Fin ) |
44 |
43
|
anassrs |
|- ( ( ( ( A C_ X /\ -. A e. Fin ) /\ z e. Fin ) /\ X = U. z ) -> E. b e. z -. ( A i^i b ) e. Fin ) |
45 |
36 44
|
sylanl2 |
|- ( ( ( ( A C_ X /\ -. A e. Fin ) /\ z e. ( ~P J i^i Fin ) ) /\ X = U. z ) -> E. b e. z -. ( A i^i b ) e. Fin ) |
46 |
|
0fin |
|- (/) e. Fin |
47 |
|
eleq1 |
|- ( ( b i^i ( A \ { o } ) ) = (/) -> ( ( b i^i ( A \ { o } ) ) e. Fin <-> (/) e. Fin ) ) |
48 |
46 47
|
mpbiri |
|- ( ( b i^i ( A \ { o } ) ) = (/) -> ( b i^i ( A \ { o } ) ) e. Fin ) |
49 |
|
snfi |
|- { o } e. Fin |
50 |
|
unfi |
|- ( ( ( b i^i ( A \ { o } ) ) e. Fin /\ { o } e. Fin ) -> ( ( b i^i ( A \ { o } ) ) u. { o } ) e. Fin ) |
51 |
48 49 50
|
sylancl |
|- ( ( b i^i ( A \ { o } ) ) = (/) -> ( ( b i^i ( A \ { o } ) ) u. { o } ) e. Fin ) |
52 |
|
ssun1 |
|- b C_ ( b u. { o } ) |
53 |
|
ssun1 |
|- A C_ ( A u. { o } ) |
54 |
|
undif1 |
|- ( ( A \ { o } ) u. { o } ) = ( A u. { o } ) |
55 |
53 54
|
sseqtrri |
|- A C_ ( ( A \ { o } ) u. { o } ) |
56 |
|
ss2in |
|- ( ( b C_ ( b u. { o } ) /\ A C_ ( ( A \ { o } ) u. { o } ) ) -> ( b i^i A ) C_ ( ( b u. { o } ) i^i ( ( A \ { o } ) u. { o } ) ) ) |
57 |
52 55 56
|
mp2an |
|- ( b i^i A ) C_ ( ( b u. { o } ) i^i ( ( A \ { o } ) u. { o } ) ) |
58 |
|
incom |
|- ( A i^i b ) = ( b i^i A ) |
59 |
|
undir |
|- ( ( b i^i ( A \ { o } ) ) u. { o } ) = ( ( b u. { o } ) i^i ( ( A \ { o } ) u. { o } ) ) |
60 |
57 58 59
|
3sstr4i |
|- ( A i^i b ) C_ ( ( b i^i ( A \ { o } ) ) u. { o } ) |
61 |
|
ssfi |
|- ( ( ( ( b i^i ( A \ { o } ) ) u. { o } ) e. Fin /\ ( A i^i b ) C_ ( ( b i^i ( A \ { o } ) ) u. { o } ) ) -> ( A i^i b ) e. Fin ) |
62 |
51 60 61
|
sylancl |
|- ( ( b i^i ( A \ { o } ) ) = (/) -> ( A i^i b ) e. Fin ) |
63 |
62
|
exlimiv |
|- ( E. o ( b i^i ( A \ { o } ) ) = (/) -> ( A i^i b ) e. Fin ) |
64 |
63
|
ralimi |
|- ( A. b e. z E. o ( b i^i ( A \ { o } ) ) = (/) -> A. b e. z ( A i^i b ) e. Fin ) |
65 |
45 64
|
anim12ci |
|- ( ( ( ( ( A C_ X /\ -. A e. Fin ) /\ z e. ( ~P J i^i Fin ) ) /\ X = U. z ) /\ A. b e. z E. o ( b i^i ( A \ { o } ) ) = (/) ) -> ( A. b e. z ( A i^i b ) e. Fin /\ E. b e. z -. ( A i^i b ) e. Fin ) ) |
66 |
65
|
expl |
|- ( ( ( A C_ X /\ -. A e. Fin ) /\ z e. ( ~P J i^i Fin ) ) -> ( ( X = U. z /\ A. b e. z E. o ( b i^i ( A \ { o } ) ) = (/) ) -> ( A. b e. z ( A i^i b ) e. Fin /\ E. b e. z -. ( A i^i b ) e. Fin ) ) ) |
67 |
66
|
reximdva |
|- ( ( A C_ X /\ -. A e. Fin ) -> ( E. z e. ( ~P J i^i Fin ) ( X = U. z /\ A. b e. z E. o ( b i^i ( A \ { o } ) ) = (/) ) -> E. z e. ( ~P J i^i Fin ) ( A. b e. z ( A i^i b ) e. Fin /\ E. b e. z -. ( A i^i b ) e. Fin ) ) ) |
68 |
67
|
3adant1 |
|- ( ( J e. Comp /\ A C_ X /\ -. A e. Fin ) -> ( E. z e. ( ~P J i^i Fin ) ( X = U. z /\ A. b e. z E. o ( b i^i ( A \ { o } ) ) = (/) ) -> E. z e. ( ~P J i^i Fin ) ( A. b e. z ( A i^i b ) e. Fin /\ E. b e. z -. ( A i^i b ) e. Fin ) ) ) |
69 |
35 68
|
syld |
|- ( ( J e. Comp /\ A C_ X /\ -. A e. Fin ) -> ( -. E. x e. X x e. ( ( limPt ` J ) ` A ) -> E. z e. ( ~P J i^i Fin ) ( A. b e. z ( A i^i b ) e. Fin /\ E. b e. z -. ( A i^i b ) e. Fin ) ) ) |
70 |
8 69
|
mt3i |
|- ( ( J e. Comp /\ A C_ X /\ -. A e. Fin ) -> E. x e. X x e. ( ( limPt ` J ) ` A ) ) |