Step |
Hyp |
Ref |
Expression |
1 |
|
psubspset.l |
|- .<_ = ( le ` K ) |
2 |
|
psubspset.j |
|- .\/ = ( join ` K ) |
3 |
|
psubspset.a |
|- A = ( Atoms ` K ) |
4 |
|
psubspset.s |
|- S = ( PSubSp ` K ) |
5 |
1 2 3 4
|
psubspset |
|- ( K e. D -> S = { x | ( x C_ A /\ A. p e. x A. q e. x A. r e. A ( r .<_ ( p .\/ q ) -> r e. x ) ) } ) |
6 |
5
|
eleq2d |
|- ( K e. D -> ( X e. S <-> X e. { x | ( x C_ A /\ A. p e. x A. q e. x A. r e. A ( r .<_ ( p .\/ q ) -> r e. x ) ) } ) ) |
7 |
3
|
fvexi |
|- A e. _V |
8 |
7
|
ssex |
|- ( X C_ A -> X e. _V ) |
9 |
8
|
adantr |
|- ( ( X C_ A /\ A. p e. X A. q e. X A. r e. A ( r .<_ ( p .\/ q ) -> r e. X ) ) -> X e. _V ) |
10 |
|
sseq1 |
|- ( x = X -> ( x C_ A <-> X C_ A ) ) |
11 |
|
eleq2 |
|- ( x = X -> ( r e. x <-> r e. X ) ) |
12 |
11
|
imbi2d |
|- ( x = X -> ( ( r .<_ ( p .\/ q ) -> r e. x ) <-> ( r .<_ ( p .\/ q ) -> r e. X ) ) ) |
13 |
12
|
ralbidv |
|- ( x = X -> ( A. r e. A ( r .<_ ( p .\/ q ) -> r e. x ) <-> A. r e. A ( r .<_ ( p .\/ q ) -> r e. X ) ) ) |
14 |
13
|
raleqbi1dv |
|- ( x = X -> ( A. q e. x A. r e. A ( r .<_ ( p .\/ q ) -> r e. x ) <-> A. q e. X A. r e. A ( r .<_ ( p .\/ q ) -> r e. X ) ) ) |
15 |
14
|
raleqbi1dv |
|- ( x = X -> ( A. p e. x A. q e. x A. r e. A ( r .<_ ( p .\/ q ) -> r e. x ) <-> A. p e. X A. q e. X A. r e. A ( r .<_ ( p .\/ q ) -> r e. X ) ) ) |
16 |
10 15
|
anbi12d |
|- ( x = X -> ( ( x C_ A /\ A. p e. x A. q e. x A. r e. A ( r .<_ ( p .\/ q ) -> r e. x ) ) <-> ( X C_ A /\ A. p e. X A. q e. X A. r e. A ( r .<_ ( p .\/ q ) -> r e. X ) ) ) ) |
17 |
9 16
|
elab3 |
|- ( X e. { x | ( x C_ A /\ A. p e. x A. q e. x A. r e. A ( r .<_ ( p .\/ q ) -> r e. x ) ) } <-> ( X C_ A /\ A. p e. X A. q e. X A. r e. A ( r .<_ ( p .\/ q ) -> r e. X ) ) ) |
18 |
6 17
|
bitrdi |
|- ( K e. D -> ( X e. S <-> ( X C_ A /\ A. p e. X A. q e. X A. r e. A ( r .<_ ( p .\/ q ) -> r e. X ) ) ) ) |