| 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
|
ispsubsp2 |
|- ( K e. D -> ( X e. S <-> ( X C_ A /\ A. p e. A ( E. q e. X E. r e. X p .<_ ( q .\/ r ) -> p e. X ) ) ) ) |
| 6 |
5
|
simplbda |
|- ( ( K e. D /\ X e. S ) -> A. p e. A ( E. q e. X E. r e. X p .<_ ( q .\/ r ) -> p e. X ) ) |
| 7 |
6
|
ex |
|- ( K e. D -> ( X e. S -> A. p e. A ( E. q e. X E. r e. X p .<_ ( q .\/ r ) -> p e. X ) ) ) |
| 8 |
|
breq1 |
|- ( p = P -> ( p .<_ ( q .\/ r ) <-> P .<_ ( q .\/ r ) ) ) |
| 9 |
8
|
2rexbidv |
|- ( p = P -> ( E. q e. X E. r e. X p .<_ ( q .\/ r ) <-> E. q e. X E. r e. X P .<_ ( q .\/ r ) ) ) |
| 10 |
|
eleq1 |
|- ( p = P -> ( p e. X <-> P e. X ) ) |
| 11 |
9 10
|
imbi12d |
|- ( p = P -> ( ( E. q e. X E. r e. X p .<_ ( q .\/ r ) -> p e. X ) <-> ( E. q e. X E. r e. X P .<_ ( q .\/ r ) -> P e. X ) ) ) |
| 12 |
11
|
rspccv |
|- ( A. p e. A ( E. q e. X E. r e. X p .<_ ( q .\/ r ) -> p e. X ) -> ( P e. A -> ( E. q e. X E. r e. X P .<_ ( q .\/ r ) -> P e. X ) ) ) |
| 13 |
7 12
|
syl6 |
|- ( K e. D -> ( X e. S -> ( P e. A -> ( E. q e. X E. r e. X P .<_ ( q .\/ r ) -> P e. X ) ) ) ) |
| 14 |
13
|
3imp1 |
|- ( ( ( K e. D /\ X e. S /\ P e. A ) /\ E. q e. X E. r e. X P .<_ ( q .\/ r ) ) -> P e. X ) |