Step |
Hyp |
Ref |
Expression |
1 |
|
elfvdm |
|- ( A e. ( topGen ` B ) -> B e. dom topGen ) |
2 |
|
inex1g |
|- ( B e. dom topGen -> ( B i^i ~P A ) e. _V ) |
3 |
1 2
|
syl |
|- ( A e. ( topGen ` B ) -> ( B i^i ~P A ) e. _V ) |
4 |
|
eltg4i |
|- ( A e. ( topGen ` B ) -> A = U. ( B i^i ~P A ) ) |
5 |
|
inss1 |
|- ( B i^i ~P A ) C_ B |
6 |
|
sseq1 |
|- ( x = ( B i^i ~P A ) -> ( x C_ B <-> ( B i^i ~P A ) C_ B ) ) |
7 |
5 6
|
mpbiri |
|- ( x = ( B i^i ~P A ) -> x C_ B ) |
8 |
7
|
biantrurd |
|- ( x = ( B i^i ~P A ) -> ( A = U. x <-> ( x C_ B /\ A = U. x ) ) ) |
9 |
|
unieq |
|- ( x = ( B i^i ~P A ) -> U. x = U. ( B i^i ~P A ) ) |
10 |
9
|
eqeq2d |
|- ( x = ( B i^i ~P A ) -> ( A = U. x <-> A = U. ( B i^i ~P A ) ) ) |
11 |
8 10
|
bitr3d |
|- ( x = ( B i^i ~P A ) -> ( ( x C_ B /\ A = U. x ) <-> A = U. ( B i^i ~P A ) ) ) |
12 |
3 4 11
|
spcedv |
|- ( A e. ( topGen ` B ) -> E. x ( x C_ B /\ A = U. x ) ) |
13 |
|
eltg3i |
|- ( ( B e. V /\ x C_ B ) -> U. x e. ( topGen ` B ) ) |
14 |
|
eleq1 |
|- ( A = U. x -> ( A e. ( topGen ` B ) <-> U. x e. ( topGen ` B ) ) ) |
15 |
13 14
|
syl5ibrcom |
|- ( ( B e. V /\ x C_ B ) -> ( A = U. x -> A e. ( topGen ` B ) ) ) |
16 |
15
|
expimpd |
|- ( B e. V -> ( ( x C_ B /\ A = U. x ) -> A e. ( topGen ` B ) ) ) |
17 |
16
|
exlimdv |
|- ( B e. V -> ( E. x ( x C_ B /\ A = U. x ) -> A e. ( topGen ` B ) ) ) |
18 |
12 17
|
impbid2 |
|- ( B e. V -> ( A e. ( topGen ` B ) <-> E. x ( x C_ B /\ A = U. x ) ) ) |