| Step |
Hyp |
Ref |
Expression |
| 1 |
|
tgval |
|- ( B e. V -> ( topGen ` B ) = { x | x C_ U. ( B i^i ~P x ) } ) |
| 2 |
1
|
eleq2d |
|- ( B e. V -> ( A e. ( topGen ` B ) <-> A e. { x | x C_ U. ( B i^i ~P x ) } ) ) |
| 3 |
|
elex |
|- ( A e. { x | x C_ U. ( B i^i ~P x ) } -> A e. _V ) |
| 4 |
3
|
adantl |
|- ( ( B e. V /\ A e. { x | x C_ U. ( B i^i ~P x ) } ) -> A e. _V ) |
| 5 |
|
inex1g |
|- ( B e. V -> ( B i^i ~P A ) e. _V ) |
| 6 |
5
|
uniexd |
|- ( B e. V -> U. ( B i^i ~P A ) e. _V ) |
| 7 |
|
ssexg |
|- ( ( A C_ U. ( B i^i ~P A ) /\ U. ( B i^i ~P A ) e. _V ) -> A e. _V ) |
| 8 |
6 7
|
sylan2 |
|- ( ( A C_ U. ( B i^i ~P A ) /\ B e. V ) -> A e. _V ) |
| 9 |
8
|
ancoms |
|- ( ( B e. V /\ A C_ U. ( B i^i ~P A ) ) -> A e. _V ) |
| 10 |
|
id |
|- ( x = A -> x = A ) |
| 11 |
|
pweq |
|- ( x = A -> ~P x = ~P A ) |
| 12 |
11
|
ineq2d |
|- ( x = A -> ( B i^i ~P x ) = ( B i^i ~P A ) ) |
| 13 |
12
|
unieqd |
|- ( x = A -> U. ( B i^i ~P x ) = U. ( B i^i ~P A ) ) |
| 14 |
10 13
|
sseq12d |
|- ( x = A -> ( x C_ U. ( B i^i ~P x ) <-> A C_ U. ( B i^i ~P A ) ) ) |
| 15 |
14
|
elabg |
|- ( A e. _V -> ( A e. { x | x C_ U. ( B i^i ~P x ) } <-> A C_ U. ( B i^i ~P A ) ) ) |
| 16 |
4 9 15
|
pm5.21nd |
|- ( B e. V -> ( A e. { x | x C_ U. ( B i^i ~P x ) } <-> A C_ U. ( B i^i ~P A ) ) ) |
| 17 |
2 16
|
bitrd |
|- ( B e. V -> ( A e. ( topGen ` B ) <-> A C_ U. ( B i^i ~P A ) ) ) |