Step |
Hyp |
Ref |
Expression |
1 |
|
eltg3 |
|- ( J e. Top -> ( x e. ( topGen ` J ) <-> E. y ( y C_ J /\ x = U. y ) ) ) |
2 |
|
simpr |
|- ( ( ( J e. Top /\ y C_ J ) /\ x = U. y ) -> x = U. y ) |
3 |
|
uniopn |
|- ( ( J e. Top /\ y C_ J ) -> U. y e. J ) |
4 |
3
|
adantr |
|- ( ( ( J e. Top /\ y C_ J ) /\ x = U. y ) -> U. y e. J ) |
5 |
2 4
|
eqeltrd |
|- ( ( ( J e. Top /\ y C_ J ) /\ x = U. y ) -> x e. J ) |
6 |
5
|
expl |
|- ( J e. Top -> ( ( y C_ J /\ x = U. y ) -> x e. J ) ) |
7 |
6
|
exlimdv |
|- ( J e. Top -> ( E. y ( y C_ J /\ x = U. y ) -> x e. J ) ) |
8 |
1 7
|
sylbid |
|- ( J e. Top -> ( x e. ( topGen ` J ) -> x e. J ) ) |
9 |
8
|
ssrdv |
|- ( J e. Top -> ( topGen ` J ) C_ J ) |
10 |
|
bastg |
|- ( J e. Top -> J C_ ( topGen ` J ) ) |
11 |
9 10
|
eqssd |
|- ( J e. Top -> ( topGen ` J ) = J ) |