Step |
Hyp |
Ref |
Expression |
1 |
|
tgval |
|- ( B e. V -> ( topGen ` B ) = { x | x C_ U. ( B i^i ~P x ) } ) |
2 |
|
inss1 |
|- ( B i^i ~P x ) C_ B |
3 |
2
|
unissi |
|- U. ( B i^i ~P x ) C_ U. B |
4 |
3
|
sseli |
|- ( y e. U. ( B i^i ~P x ) -> y e. U. B ) |
5 |
4
|
pm4.71ri |
|- ( y e. U. ( B i^i ~P x ) <-> ( y e. U. B /\ y e. U. ( B i^i ~P x ) ) ) |
6 |
5
|
ralbii |
|- ( A. y e. x y e. U. ( B i^i ~P x ) <-> A. y e. x ( y e. U. B /\ y e. U. ( B i^i ~P x ) ) ) |
7 |
|
r19.26 |
|- ( A. y e. x ( y e. U. B /\ y e. U. ( B i^i ~P x ) ) <-> ( A. y e. x y e. U. B /\ A. y e. x y e. U. ( B i^i ~P x ) ) ) |
8 |
6 7
|
bitri |
|- ( A. y e. x y e. U. ( B i^i ~P x ) <-> ( A. y e. x y e. U. B /\ A. y e. x y e. U. ( B i^i ~P x ) ) ) |
9 |
|
dfss3 |
|- ( x C_ U. ( B i^i ~P x ) <-> A. y e. x y e. U. ( B i^i ~P x ) ) |
10 |
|
dfss3 |
|- ( x C_ U. B <-> A. y e. x y e. U. B ) |
11 |
|
elin |
|- ( z e. ( B i^i ~P x ) <-> ( z e. B /\ z e. ~P x ) ) |
12 |
11
|
anbi2i |
|- ( ( y e. z /\ z e. ( B i^i ~P x ) ) <-> ( y e. z /\ ( z e. B /\ z e. ~P x ) ) ) |
13 |
|
an12 |
|- ( ( y e. z /\ ( z e. B /\ z e. ~P x ) ) <-> ( z e. B /\ ( y e. z /\ z e. ~P x ) ) ) |
14 |
12 13
|
bitri |
|- ( ( y e. z /\ z e. ( B i^i ~P x ) ) <-> ( z e. B /\ ( y e. z /\ z e. ~P x ) ) ) |
15 |
14
|
exbii |
|- ( E. z ( y e. z /\ z e. ( B i^i ~P x ) ) <-> E. z ( z e. B /\ ( y e. z /\ z e. ~P x ) ) ) |
16 |
|
eluni |
|- ( y e. U. ( B i^i ~P x ) <-> E. z ( y e. z /\ z e. ( B i^i ~P x ) ) ) |
17 |
|
df-rex |
|- ( E. z e. B ( y e. z /\ z e. ~P x ) <-> E. z ( z e. B /\ ( y e. z /\ z e. ~P x ) ) ) |
18 |
15 16 17
|
3bitr4i |
|- ( y e. U. ( B i^i ~P x ) <-> E. z e. B ( y e. z /\ z e. ~P x ) ) |
19 |
|
velpw |
|- ( z e. ~P x <-> z C_ x ) |
20 |
19
|
anbi2i |
|- ( ( y e. z /\ z e. ~P x ) <-> ( y e. z /\ z C_ x ) ) |
21 |
20
|
rexbii |
|- ( E. z e. B ( y e. z /\ z e. ~P x ) <-> E. z e. B ( y e. z /\ z C_ x ) ) |
22 |
18 21
|
bitr2i |
|- ( E. z e. B ( y e. z /\ z C_ x ) <-> y e. U. ( B i^i ~P x ) ) |
23 |
22
|
ralbii |
|- ( A. y e. x E. z e. B ( y e. z /\ z C_ x ) <-> A. y e. x y e. U. ( B i^i ~P x ) ) |
24 |
10 23
|
anbi12i |
|- ( ( x C_ U. B /\ A. y e. x E. z e. B ( y e. z /\ z C_ x ) ) <-> ( A. y e. x y e. U. B /\ A. y e. x y e. U. ( B i^i ~P x ) ) ) |
25 |
8 9 24
|
3bitr4i |
|- ( x C_ U. ( B i^i ~P x ) <-> ( x C_ U. B /\ A. y e. x E. z e. B ( y e. z /\ z C_ x ) ) ) |
26 |
25
|
abbii |
|- { x | x C_ U. ( B i^i ~P x ) } = { x | ( x C_ U. B /\ A. y e. x E. z e. B ( y e. z /\ z C_ x ) ) } |
27 |
1 26
|
eqtrdi |
|- ( B e. V -> ( topGen ` B ) = { x | ( x C_ U. B /\ A. y e. x E. z e. B ( y e. z /\ z C_ x ) ) } ) |