| Step |
Hyp |
Ref |
Expression |
| 1 |
|
elinel1 |
|- ( J e. ( Top i^i Fin ) -> J e. Top ) |
| 2 |
|
elinel2 |
|- ( J e. ( Top i^i Fin ) -> J e. Fin ) |
| 3 |
|
vex |
|- y e. _V |
| 4 |
3
|
pwid |
|- y e. ~P y |
| 5 |
|
velpw |
|- ( y e. ~P J <-> y C_ J ) |
| 6 |
|
ssfi |
|- ( ( J e. Fin /\ y C_ J ) -> y e. Fin ) |
| 7 |
5 6
|
sylan2b |
|- ( ( J e. Fin /\ y e. ~P J ) -> y e. Fin ) |
| 8 |
|
elin |
|- ( y e. ( ~P y i^i Fin ) <-> ( y e. ~P y /\ y e. Fin ) ) |
| 9 |
|
unieq |
|- ( z = y -> U. z = U. y ) |
| 10 |
9
|
rspceeqv |
|- ( ( y e. ( ~P y i^i Fin ) /\ U. J = U. y ) -> E. z e. ( ~P y i^i Fin ) U. J = U. z ) |
| 11 |
10
|
ex |
|- ( y e. ( ~P y i^i Fin ) -> ( U. J = U. y -> E. z e. ( ~P y i^i Fin ) U. J = U. z ) ) |
| 12 |
8 11
|
sylbir |
|- ( ( y e. ~P y /\ y e. Fin ) -> ( U. J = U. y -> E. z e. ( ~P y i^i Fin ) U. J = U. z ) ) |
| 13 |
4 7 12
|
sylancr |
|- ( ( J e. Fin /\ y e. ~P J ) -> ( U. J = U. y -> E. z e. ( ~P y i^i Fin ) U. J = U. z ) ) |
| 14 |
13
|
ralrimiva |
|- ( J e. Fin -> A. y e. ~P J ( U. J = U. y -> E. z e. ( ~P y i^i Fin ) U. J = U. z ) ) |
| 15 |
2 14
|
syl |
|- ( J e. ( Top i^i Fin ) -> A. y e. ~P J ( U. J = U. y -> E. z e. ( ~P y i^i Fin ) U. J = U. z ) ) |
| 16 |
|
eqid |
|- U. J = U. J |
| 17 |
16
|
iscmp |
|- ( J e. Comp <-> ( J e. Top /\ A. y e. ~P J ( U. J = U. y -> E. z e. ( ~P y i^i Fin ) U. J = U. z ) ) ) |
| 18 |
1 15 17
|
sylanbrc |
|- ( J e. ( Top i^i Fin ) -> J e. Comp ) |