Step |
Hyp |
Ref |
Expression |
1 |
|
istopg |
|- ( J e. Top -> ( J e. Top <-> ( A. x ( x C_ J -> U. x e. J ) /\ A. x e. J A. y e. J ( x i^i y ) e. J ) ) ) |
2 |
1
|
ibi |
|- ( J e. Top -> ( A. x ( x C_ J -> U. x e. J ) /\ A. x e. J A. y e. J ( x i^i y ) e. J ) ) |
3 |
2
|
simprd |
|- ( J e. Top -> A. x e. J A. y e. J ( x i^i y ) e. J ) |
4 |
|
ineq1 |
|- ( x = A -> ( x i^i y ) = ( A i^i y ) ) |
5 |
4
|
eleq1d |
|- ( x = A -> ( ( x i^i y ) e. J <-> ( A i^i y ) e. J ) ) |
6 |
|
ineq2 |
|- ( y = B -> ( A i^i y ) = ( A i^i B ) ) |
7 |
6
|
eleq1d |
|- ( y = B -> ( ( A i^i y ) e. J <-> ( A i^i B ) e. J ) ) |
8 |
5 7
|
rspc2v |
|- ( ( A e. J /\ B e. J ) -> ( A. x e. J A. y e. J ( x i^i y ) e. J -> ( A i^i B ) e. J ) ) |
9 |
3 8
|
syl5com |
|- ( J e. Top -> ( ( A e. J /\ B e. J ) -> ( A i^i B ) e. J ) ) |
10 |
9
|
3impib |
|- ( ( J e. Top /\ A e. J /\ B e. J ) -> ( A i^i B ) e. J ) |