Step |
Hyp |
Ref |
Expression |
1 |
|
df-topgen |
|- topGen = ( y e. _V |-> { x | x C_ U. ( y i^i ~P x ) } ) |
2 |
|
ineq1 |
|- ( y = B -> ( y i^i ~P x ) = ( B i^i ~P x ) ) |
3 |
2
|
unieqd |
|- ( y = B -> U. ( y i^i ~P x ) = U. ( B i^i ~P x ) ) |
4 |
3
|
sseq2d |
|- ( y = B -> ( x C_ U. ( y i^i ~P x ) <-> x C_ U. ( B i^i ~P x ) ) ) |
5 |
4
|
abbidv |
|- ( y = B -> { x | x C_ U. ( y i^i ~P x ) } = { x | x C_ U. ( B i^i ~P x ) } ) |
6 |
|
elex |
|- ( B e. V -> B e. _V ) |
7 |
|
uniexg |
|- ( B e. V -> U. B e. _V ) |
8 |
|
abssexg |
|- ( U. B e. _V -> { x | ( x C_ U. B /\ x C_ U. ~P x ) } e. _V ) |
9 |
|
uniin |
|- U. ( B i^i ~P x ) C_ ( U. B i^i U. ~P x ) |
10 |
|
sstr |
|- ( ( x C_ U. ( B i^i ~P x ) /\ U. ( B i^i ~P x ) C_ ( U. B i^i U. ~P x ) ) -> x C_ ( U. B i^i U. ~P x ) ) |
11 |
9 10
|
mpan2 |
|- ( x C_ U. ( B i^i ~P x ) -> x C_ ( U. B i^i U. ~P x ) ) |
12 |
|
ssin |
|- ( ( x C_ U. B /\ x C_ U. ~P x ) <-> x C_ ( U. B i^i U. ~P x ) ) |
13 |
11 12
|
sylibr |
|- ( x C_ U. ( B i^i ~P x ) -> ( x C_ U. B /\ x C_ U. ~P x ) ) |
14 |
13
|
ss2abi |
|- { x | x C_ U. ( B i^i ~P x ) } C_ { x | ( x C_ U. B /\ x C_ U. ~P x ) } |
15 |
|
ssexg |
|- ( ( { x | x C_ U. ( B i^i ~P x ) } C_ { x | ( x C_ U. B /\ x C_ U. ~P x ) } /\ { x | ( x C_ U. B /\ x C_ U. ~P x ) } e. _V ) -> { x | x C_ U. ( B i^i ~P x ) } e. _V ) |
16 |
14 15
|
mpan |
|- ( { x | ( x C_ U. B /\ x C_ U. ~P x ) } e. _V -> { x | x C_ U. ( B i^i ~P x ) } e. _V ) |
17 |
7 8 16
|
3syl |
|- ( B e. V -> { x | x C_ U. ( B i^i ~P x ) } e. _V ) |
18 |
1 5 6 17
|
fvmptd3 |
|- ( B e. V -> ( topGen ` B ) = { x | x C_ U. ( B i^i ~P x ) } ) |