| Step |
Hyp |
Ref |
Expression |
| 1 |
|
isbasis2g |
|- ( B e. TopBases -> ( B e. TopBases <-> A. y e. B A. z e. B A. w e. ( y i^i z ) E. x e. B ( w e. x /\ x C_ ( y i^i z ) ) ) ) |
| 2 |
1
|
ibi |
|- ( B e. TopBases -> A. y e. B A. z e. B A. w e. ( y i^i z ) E. x e. B ( w e. x /\ x C_ ( y i^i z ) ) ) |
| 3 |
|
ineq1 |
|- ( y = C -> ( y i^i z ) = ( C i^i z ) ) |
| 4 |
|
sseq2 |
|- ( ( y i^i z ) = ( C i^i z ) -> ( x C_ ( y i^i z ) <-> x C_ ( C i^i z ) ) ) |
| 5 |
4
|
anbi2d |
|- ( ( y i^i z ) = ( C i^i z ) -> ( ( w e. x /\ x C_ ( y i^i z ) ) <-> ( w e. x /\ x C_ ( C i^i z ) ) ) ) |
| 6 |
5
|
rexbidv |
|- ( ( y i^i z ) = ( C i^i z ) -> ( E. x e. B ( w e. x /\ x C_ ( y i^i z ) ) <-> E. x e. B ( w e. x /\ x C_ ( C i^i z ) ) ) ) |
| 7 |
6
|
raleqbi1dv |
|- ( ( y i^i z ) = ( C i^i z ) -> ( A. w e. ( y i^i z ) E. x e. B ( w e. x /\ x C_ ( y i^i z ) ) <-> A. w e. ( C i^i z ) E. x e. B ( w e. x /\ x C_ ( C i^i z ) ) ) ) |
| 8 |
3 7
|
syl |
|- ( y = C -> ( A. w e. ( y i^i z ) E. x e. B ( w e. x /\ x C_ ( y i^i z ) ) <-> A. w e. ( C i^i z ) E. x e. B ( w e. x /\ x C_ ( C i^i z ) ) ) ) |
| 9 |
|
ineq2 |
|- ( z = D -> ( C i^i z ) = ( C i^i D ) ) |
| 10 |
|
sseq2 |
|- ( ( C i^i z ) = ( C i^i D ) -> ( x C_ ( C i^i z ) <-> x C_ ( C i^i D ) ) ) |
| 11 |
10
|
anbi2d |
|- ( ( C i^i z ) = ( C i^i D ) -> ( ( w e. x /\ x C_ ( C i^i z ) ) <-> ( w e. x /\ x C_ ( C i^i D ) ) ) ) |
| 12 |
11
|
rexbidv |
|- ( ( C i^i z ) = ( C i^i D ) -> ( E. x e. B ( w e. x /\ x C_ ( C i^i z ) ) <-> E. x e. B ( w e. x /\ x C_ ( C i^i D ) ) ) ) |
| 13 |
12
|
raleqbi1dv |
|- ( ( C i^i z ) = ( C i^i D ) -> ( A. w e. ( C i^i z ) E. x e. B ( w e. x /\ x C_ ( C i^i z ) ) <-> A. w e. ( C i^i D ) E. x e. B ( w e. x /\ x C_ ( C i^i D ) ) ) ) |
| 14 |
9 13
|
syl |
|- ( z = D -> ( A. w e. ( C i^i z ) E. x e. B ( w e. x /\ x C_ ( C i^i z ) ) <-> A. w e. ( C i^i D ) E. x e. B ( w e. x /\ x C_ ( C i^i D ) ) ) ) |
| 15 |
8 14
|
rspc2v |
|- ( ( C e. B /\ D e. B ) -> ( A. y e. B A. z e. B A. w e. ( y i^i z ) E. x e. B ( w e. x /\ x C_ ( y i^i z ) ) -> A. w e. ( C i^i D ) E. x e. B ( w e. x /\ x C_ ( C i^i D ) ) ) ) |
| 16 |
|
eleq1 |
|- ( w = A -> ( w e. x <-> A e. x ) ) |
| 17 |
16
|
anbi1d |
|- ( w = A -> ( ( w e. x /\ x C_ ( C i^i D ) ) <-> ( A e. x /\ x C_ ( C i^i D ) ) ) ) |
| 18 |
17
|
rexbidv |
|- ( w = A -> ( E. x e. B ( w e. x /\ x C_ ( C i^i D ) ) <-> E. x e. B ( A e. x /\ x C_ ( C i^i D ) ) ) ) |
| 19 |
18
|
rspccv |
|- ( A. w e. ( C i^i D ) E. x e. B ( w e. x /\ x C_ ( C i^i D ) ) -> ( A e. ( C i^i D ) -> E. x e. B ( A e. x /\ x C_ ( C i^i D ) ) ) ) |
| 20 |
15 19
|
syl6com |
|- ( A. y e. B A. z e. B A. w e. ( y i^i z ) E. x e. B ( w e. x /\ x C_ ( y i^i z ) ) -> ( ( C e. B /\ D e. B ) -> ( A e. ( C i^i D ) -> E. x e. B ( A e. x /\ x C_ ( C i^i D ) ) ) ) ) |
| 21 |
2 20
|
syl |
|- ( B e. TopBases -> ( ( C e. B /\ D e. B ) -> ( A e. ( C i^i D ) -> E. x e. B ( A e. x /\ x C_ ( C i^i D ) ) ) ) ) |
| 22 |
21
|
expd |
|- ( B e. TopBases -> ( C e. B -> ( D e. B -> ( A e. ( C i^i D ) -> E. x e. B ( A e. x /\ x C_ ( C i^i D ) ) ) ) ) ) |
| 23 |
22
|
imp43 |
|- ( ( ( B e. TopBases /\ C e. B ) /\ ( D e. B /\ A e. ( C i^i D ) ) ) -> E. x e. B ( A e. x /\ x C_ ( C i^i D ) ) ) |