Step |
Hyp |
Ref |
Expression |
1 |
|
ptcmp.1 |
|- S = ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) |
2 |
|
ptcmp.2 |
|- X = X_ n e. A U. ( F ` n ) |
3 |
|
ptcmp.3 |
|- ( ph -> A e. V ) |
4 |
|
ptcmp.4 |
|- ( ph -> F : A --> Comp ) |
5 |
|
ptcmp.5 |
|- ( ph -> X e. ( UFL i^i dom card ) ) |
6 |
4
|
ffnd |
|- ( ph -> F Fn A ) |
7 |
|
eqid |
|- { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } = { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } |
8 |
7
|
ptval |
|- ( ( A e. V /\ F Fn A ) -> ( Xt_ ` F ) = ( topGen ` { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } ) ) |
9 |
3 6 8
|
syl2anc |
|- ( ph -> ( Xt_ ` F ) = ( topGen ` { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } ) ) |
10 |
|
cmptop |
|- ( x e. Comp -> x e. Top ) |
11 |
10
|
ssriv |
|- Comp C_ Top |
12 |
|
fss |
|- ( ( F : A --> Comp /\ Comp C_ Top ) -> F : A --> Top ) |
13 |
4 11 12
|
sylancl |
|- ( ph -> F : A --> Top ) |
14 |
7 2
|
ptbasfi |
|- ( ( A e. V /\ F : A --> Top ) -> { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } = ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) ) |
15 |
3 13 14
|
syl2anc |
|- ( ph -> { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } = ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) ) |
16 |
|
uncom |
|- ( ran S u. { X } ) = ( { X } u. ran S ) |
17 |
1
|
rneqi |
|- ran S = ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) |
18 |
17
|
uneq2i |
|- ( { X } u. ran S ) = ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) |
19 |
16 18
|
eqtri |
|- ( ran S u. { X } ) = ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) |
20 |
19
|
fveq2i |
|- ( fi ` ( ran S u. { X } ) ) = ( fi ` ( { X } u. ran ( k e. A , u e. ( F ` k ) |-> ( `' ( w e. X |-> ( w ` k ) ) " u ) ) ) ) |
21 |
15 20
|
eqtr4di |
|- ( ph -> { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } = ( fi ` ( ran S u. { X } ) ) ) |
22 |
21
|
fveq2d |
|- ( ph -> ( topGen ` { x | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ x = X_ y e. A ( g ` y ) ) } ) = ( topGen ` ( fi ` ( ran S u. { X } ) ) ) ) |
23 |
9 22
|
eqtrd |
|- ( ph -> ( Xt_ ` F ) = ( topGen ` ( fi ` ( ran S u. { X } ) ) ) ) |
24 |
23
|
unieqd |
|- ( ph -> U. ( Xt_ ` F ) = U. ( topGen ` ( fi ` ( ran S u. { X } ) ) ) ) |
25 |
|
fibas |
|- ( fi ` ( ran S u. { X } ) ) e. TopBases |
26 |
|
unitg |
|- ( ( fi ` ( ran S u. { X } ) ) e. TopBases -> U. ( topGen ` ( fi ` ( ran S u. { X } ) ) ) = U. ( fi ` ( ran S u. { X } ) ) ) |
27 |
25 26
|
ax-mp |
|- U. ( topGen ` ( fi ` ( ran S u. { X } ) ) ) = U. ( fi ` ( ran S u. { X } ) ) |
28 |
24 27
|
eqtrdi |
|- ( ph -> U. ( Xt_ ` F ) = U. ( fi ` ( ran S u. { X } ) ) ) |
29 |
|
eqid |
|- ( Xt_ ` F ) = ( Xt_ ` F ) |
30 |
29
|
ptuni |
|- ( ( A e. V /\ F : A --> Top ) -> X_ n e. A U. ( F ` n ) = U. ( Xt_ ` F ) ) |
31 |
3 13 30
|
syl2anc |
|- ( ph -> X_ n e. A U. ( F ` n ) = U. ( Xt_ ` F ) ) |
32 |
2 31
|
syl5eq |
|- ( ph -> X = U. ( Xt_ ` F ) ) |
33 |
5
|
pwexd |
|- ( ph -> ~P X e. _V ) |
34 |
|
eqid |
|- ( w e. X |-> ( w ` k ) ) = ( w e. X |-> ( w ` k ) ) |
35 |
34
|
mptpreima |
|- ( `' ( w e. X |-> ( w ` k ) ) " u ) = { w e. X | ( w ` k ) e. u } |
36 |
35
|
ssrab3 |
|- ( `' ( w e. X |-> ( w ` k ) ) " u ) C_ X |
37 |
5
|
adantr |
|- ( ( ph /\ ( k e. A /\ u e. ( F ` k ) ) ) -> X e. ( UFL i^i dom card ) ) |
38 |
|
elpw2g |
|- ( X e. ( UFL i^i dom card ) -> ( ( `' ( w e. X |-> ( w ` k ) ) " u ) e. ~P X <-> ( `' ( w e. X |-> ( w ` k ) ) " u ) C_ X ) ) |
39 |
37 38
|
syl |
|- ( ( ph /\ ( k e. A /\ u e. ( F ` k ) ) ) -> ( ( `' ( w e. X |-> ( w ` k ) ) " u ) e. ~P X <-> ( `' ( w e. X |-> ( w ` k ) ) " u ) C_ X ) ) |
40 |
36 39
|
mpbiri |
|- ( ( ph /\ ( k e. A /\ u e. ( F ` k ) ) ) -> ( `' ( w e. X |-> ( w ` k ) ) " u ) e. ~P X ) |
41 |
40
|
ralrimivva |
|- ( ph -> A. k e. A A. u e. ( F ` k ) ( `' ( w e. X |-> ( w ` k ) ) " u ) e. ~P X ) |
42 |
1
|
fmpox |
|- ( A. k e. A A. u e. ( F ` k ) ( `' ( w e. X |-> ( w ` k ) ) " u ) e. ~P X <-> S : U_ k e. A ( { k } X. ( F ` k ) ) --> ~P X ) |
43 |
41 42
|
sylib |
|- ( ph -> S : U_ k e. A ( { k } X. ( F ` k ) ) --> ~P X ) |
44 |
43
|
frnd |
|- ( ph -> ran S C_ ~P X ) |
45 |
33 44
|
ssexd |
|- ( ph -> ran S e. _V ) |
46 |
|
snex |
|- { X } e. _V |
47 |
|
unexg |
|- ( ( ran S e. _V /\ { X } e. _V ) -> ( ran S u. { X } ) e. _V ) |
48 |
45 46 47
|
sylancl |
|- ( ph -> ( ran S u. { X } ) e. _V ) |
49 |
|
fiuni |
|- ( ( ran S u. { X } ) e. _V -> U. ( ran S u. { X } ) = U. ( fi ` ( ran S u. { X } ) ) ) |
50 |
48 49
|
syl |
|- ( ph -> U. ( ran S u. { X } ) = U. ( fi ` ( ran S u. { X } ) ) ) |
51 |
28 32 50
|
3eqtr4d |
|- ( ph -> X = U. ( ran S u. { X } ) ) |
52 |
51 23
|
jca |
|- ( ph -> ( X = U. ( ran S u. { X } ) /\ ( Xt_ ` F ) = ( topGen ` ( fi ` ( ran S u. { X } ) ) ) ) ) |