Step |
Hyp |
Ref |
Expression |
1 |
|
indif1 |
|- ( ( B \ { (/) } ) i^i ~P x ) = ( ( B i^i ~P x ) \ { (/) } ) |
2 |
1
|
unieqi |
|- U. ( ( B \ { (/) } ) i^i ~P x ) = U. ( ( B i^i ~P x ) \ { (/) } ) |
3 |
|
unidif0 |
|- U. ( ( B i^i ~P x ) \ { (/) } ) = U. ( B i^i ~P x ) |
4 |
2 3
|
eqtri |
|- U. ( ( B \ { (/) } ) i^i ~P x ) = U. ( B i^i ~P x ) |
5 |
4
|
sseq2i |
|- ( x C_ U. ( ( B \ { (/) } ) i^i ~P x ) <-> x C_ U. ( B i^i ~P x ) ) |
6 |
5
|
abbii |
|- { x | x C_ U. ( ( B \ { (/) } ) i^i ~P x ) } = { x | x C_ U. ( B i^i ~P x ) } |
7 |
|
difexg |
|- ( B e. _V -> ( B \ { (/) } ) e. _V ) |
8 |
|
tgval |
|- ( ( B \ { (/) } ) e. _V -> ( topGen ` ( B \ { (/) } ) ) = { x | x C_ U. ( ( B \ { (/) } ) i^i ~P x ) } ) |
9 |
7 8
|
syl |
|- ( B e. _V -> ( topGen ` ( B \ { (/) } ) ) = { x | x C_ U. ( ( B \ { (/) } ) i^i ~P x ) } ) |
10 |
|
tgval |
|- ( B e. _V -> ( topGen ` B ) = { x | x C_ U. ( B i^i ~P x ) } ) |
11 |
6 9 10
|
3eqtr4a |
|- ( B e. _V -> ( topGen ` ( B \ { (/) } ) ) = ( topGen ` B ) ) |
12 |
|
difsnexi |
|- ( ( B \ { (/) } ) e. _V -> B e. _V ) |
13 |
|
fvprc |
|- ( -. ( B \ { (/) } ) e. _V -> ( topGen ` ( B \ { (/) } ) ) = (/) ) |
14 |
12 13
|
nsyl5 |
|- ( -. B e. _V -> ( topGen ` ( B \ { (/) } ) ) = (/) ) |
15 |
|
fvprc |
|- ( -. B e. _V -> ( topGen ` B ) = (/) ) |
16 |
14 15
|
eqtr4d |
|- ( -. B e. _V -> ( topGen ` ( B \ { (/) } ) ) = ( topGen ` B ) ) |
17 |
11 16
|
pm2.61i |
|- ( topGen ` ( B \ { (/) } ) ) = ( topGen ` B ) |