Step |
Hyp |
Ref |
Expression |
1 |
|
poml4.a |
|- A = ( Atoms ` K ) |
2 |
|
poml4.p |
|- ._|_ = ( _|_P ` K ) |
3 |
|
simp1 |
|- ( ( K e. HL /\ Y C_ A /\ X C_ ( ._|_ ` Y ) ) -> K e. HL ) |
4 |
|
simp3 |
|- ( ( K e. HL /\ Y C_ A /\ X C_ ( ._|_ ` Y ) ) -> X C_ ( ._|_ ` Y ) ) |
5 |
1 2
|
polssatN |
|- ( ( K e. HL /\ Y C_ A ) -> ( ._|_ ` Y ) C_ A ) |
6 |
5
|
3adant3 |
|- ( ( K e. HL /\ Y C_ A /\ X C_ ( ._|_ ` Y ) ) -> ( ._|_ ` Y ) C_ A ) |
7 |
4 6
|
sstrd |
|- ( ( K e. HL /\ Y C_ A /\ X C_ ( ._|_ ` Y ) ) -> X C_ A ) |
8 |
3 7 6
|
3jca |
|- ( ( K e. HL /\ Y C_ A /\ X C_ ( ._|_ ` Y ) ) -> ( K e. HL /\ X C_ A /\ ( ._|_ ` Y ) C_ A ) ) |
9 |
1 2
|
3polN |
|- ( ( K e. HL /\ Y C_ A ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` Y ) ) ) = ( ._|_ ` Y ) ) |
10 |
9
|
3adant3 |
|- ( ( K e. HL /\ Y C_ A /\ X C_ ( ._|_ ` Y ) ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` Y ) ) ) = ( ._|_ ` Y ) ) |
11 |
4 10
|
jca |
|- ( ( K e. HL /\ Y C_ A /\ X C_ ( ._|_ ` Y ) ) -> ( X C_ ( ._|_ ` Y ) /\ ( ._|_ ` ( ._|_ ` ( ._|_ ` Y ) ) ) = ( ._|_ ` Y ) ) ) |
12 |
1 2
|
poml4N |
|- ( ( K e. HL /\ X C_ A /\ ( ._|_ ` Y ) C_ A ) -> ( ( X C_ ( ._|_ ` Y ) /\ ( ._|_ ` ( ._|_ ` ( ._|_ ` Y ) ) ) = ( ._|_ ` Y ) ) -> ( ( ._|_ ` ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) ) i^i ( ._|_ ` Y ) ) = ( ._|_ ` ( ._|_ ` X ) ) ) ) |
13 |
8 11 12
|
sylc |
|- ( ( K e. HL /\ Y C_ A /\ X C_ ( ._|_ ` Y ) ) -> ( ( ._|_ ` ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) ) i^i ( ._|_ ` Y ) ) = ( ._|_ ` ( ._|_ ` X ) ) ) |