Step |
Hyp |
Ref |
Expression |
1 |
|
eltg2 |
|- ( B e. V -> ( A e. ( topGen ` B ) <-> ( A C_ U. B /\ A. x e. A E. y e. B ( x e. y /\ y C_ A ) ) ) ) |
2 |
|
simpl |
|- ( ( x e. y /\ y C_ A ) -> x e. y ) |
3 |
2
|
reximi |
|- ( E. y e. B ( x e. y /\ y C_ A ) -> E. y e. B x e. y ) |
4 |
|
eluni2 |
|- ( x e. U. B <-> E. y e. B x e. y ) |
5 |
3 4
|
sylibr |
|- ( E. y e. B ( x e. y /\ y C_ A ) -> x e. U. B ) |
6 |
5
|
ralimi |
|- ( A. x e. A E. y e. B ( x e. y /\ y C_ A ) -> A. x e. A x e. U. B ) |
7 |
|
dfss3 |
|- ( A C_ U. B <-> A. x e. A x e. U. B ) |
8 |
6 7
|
sylibr |
|- ( A. x e. A E. y e. B ( x e. y /\ y C_ A ) -> A C_ U. B ) |
9 |
8
|
pm4.71ri |
|- ( A. x e. A E. y e. B ( x e. y /\ y C_ A ) <-> ( A C_ U. B /\ A. x e. A E. y e. B ( x e. y /\ y C_ A ) ) ) |
10 |
1 9
|
bitr4di |
|- ( B e. V -> ( A e. ( topGen ` B ) <-> A. x e. A E. y e. B ( x e. y /\ y C_ A ) ) ) |