Step |
Hyp |
Ref |
Expression |
1 |
|
trlne.l |
|- .<_ = ( le ` K ) |
2 |
|
trlne.a |
|- A = ( Atoms ` K ) |
3 |
|
trlne.h |
|- H = ( LHyp ` K ) |
4 |
|
trlne.t |
|- T = ( ( LTrn ` K ) ` W ) |
5 |
|
trlne.r |
|- R = ( ( trL ` K ) ` W ) |
6 |
|
simp3r |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> -. P .<_ W ) |
7 |
1 3 4 5
|
trlle |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` F ) .<_ W ) |
8 |
7
|
3adant3 |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( R ` F ) .<_ W ) |
9 |
|
breq1 |
|- ( P = ( R ` F ) -> ( P .<_ W <-> ( R ` F ) .<_ W ) ) |
10 |
8 9
|
syl5ibrcom |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( P = ( R ` F ) -> P .<_ W ) ) |
11 |
10
|
necon3bd |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( -. P .<_ W -> P =/= ( R ` F ) ) ) |
12 |
6 11
|
mpd |
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> P =/= ( R ` F ) ) |