Step |
Hyp |
Ref |
Expression |
1 |
|
ptbas.1 |
|- B = { 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 ) ) } |
2 |
|
simpl |
|- ( ( A e. V /\ F : A --> Top ) -> A e. V ) |
3 |
|
0fin |
|- (/) e. Fin |
4 |
3
|
a1i |
|- ( ( A e. V /\ F : A --> Top ) -> (/) e. Fin ) |
5 |
|
ffvelrn |
|- ( ( F : A --> Top /\ k e. A ) -> ( F ` k ) e. Top ) |
6 |
5
|
adantll |
|- ( ( ( A e. V /\ F : A --> Top ) /\ k e. A ) -> ( F ` k ) e. Top ) |
7 |
|
eqid |
|- U. ( F ` k ) = U. ( F ` k ) |
8 |
7
|
topopn |
|- ( ( F ` k ) e. Top -> U. ( F ` k ) e. ( F ` k ) ) |
9 |
6 8
|
syl |
|- ( ( ( A e. V /\ F : A --> Top ) /\ k e. A ) -> U. ( F ` k ) e. ( F ` k ) ) |
10 |
|
eqidd |
|- ( ( ( A e. V /\ F : A --> Top ) /\ k e. ( A \ (/) ) ) -> U. ( F ` k ) = U. ( F ` k ) ) |
11 |
1 2 4 9 10
|
elptr2 |
|- ( ( A e. V /\ F : A --> Top ) -> X_ k e. A U. ( F ` k ) e. B ) |