| Step |
Hyp |
Ref |
Expression |
| 1 |
|
isbasisg |
|- ( B e. TopBases -> ( B e. TopBases <-> A. x e. B A. y e. B ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) ) ) |
| 2 |
1
|
ibi |
|- ( B e. TopBases -> A. x e. B A. y e. B ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) ) |
| 3 |
|
ineq1 |
|- ( x = C -> ( x i^i y ) = ( C i^i y ) ) |
| 4 |
3
|
pweqd |
|- ( x = C -> ~P ( x i^i y ) = ~P ( C i^i y ) ) |
| 5 |
4
|
ineq2d |
|- ( x = C -> ( B i^i ~P ( x i^i y ) ) = ( B i^i ~P ( C i^i y ) ) ) |
| 6 |
5
|
unieqd |
|- ( x = C -> U. ( B i^i ~P ( x i^i y ) ) = U. ( B i^i ~P ( C i^i y ) ) ) |
| 7 |
3 6
|
sseq12d |
|- ( x = C -> ( ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) <-> ( C i^i y ) C_ U. ( B i^i ~P ( C i^i y ) ) ) ) |
| 8 |
|
ineq2 |
|- ( y = D -> ( C i^i y ) = ( C i^i D ) ) |
| 9 |
8
|
pweqd |
|- ( y = D -> ~P ( C i^i y ) = ~P ( C i^i D ) ) |
| 10 |
9
|
ineq2d |
|- ( y = D -> ( B i^i ~P ( C i^i y ) ) = ( B i^i ~P ( C i^i D ) ) ) |
| 11 |
10
|
unieqd |
|- ( y = D -> U. ( B i^i ~P ( C i^i y ) ) = U. ( B i^i ~P ( C i^i D ) ) ) |
| 12 |
8 11
|
sseq12d |
|- ( y = D -> ( ( C i^i y ) C_ U. ( B i^i ~P ( C i^i y ) ) <-> ( C i^i D ) C_ U. ( B i^i ~P ( C i^i D ) ) ) ) |
| 13 |
7 12
|
rspc2v |
|- ( ( C e. B /\ D e. B ) -> ( A. x e. B A. y e. B ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) -> ( C i^i D ) C_ U. ( B i^i ~P ( C i^i D ) ) ) ) |
| 14 |
2 13
|
syl5com |
|- ( B e. TopBases -> ( ( C e. B /\ D e. B ) -> ( C i^i D ) C_ U. ( B i^i ~P ( C i^i D ) ) ) ) |
| 15 |
14
|
3impib |
|- ( ( B e. TopBases /\ C e. B /\ D e. B ) -> ( C i^i D ) C_ U. ( B i^i ~P ( C i^i D ) ) ) |