Step |
Hyp |
Ref |
Expression |
1 |
|
atlelt.b |
|- B = ( Base ` K ) |
2 |
|
atlelt.l |
|- .<_ = ( le ` K ) |
3 |
|
atlelt.s |
|- .< = ( lt ` K ) |
4 |
|
atlelt.a |
|- A = ( Atoms ` K ) |
5 |
|
simp3r |
|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ X e. B ) /\ ( P .<_ X /\ Q .< X ) ) -> Q .< X ) |
6 |
|
breq1 |
|- ( P = Q -> ( P .< X <-> Q .< X ) ) |
7 |
5 6
|
syl5ibrcom |
|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ X e. B ) /\ ( P .<_ X /\ Q .< X ) ) -> ( P = Q -> P .< X ) ) |
8 |
|
simp1 |
|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ X e. B ) /\ ( P .<_ X /\ Q .< X ) ) -> K e. HL ) |
9 |
|
simp21 |
|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ X e. B ) /\ ( P .<_ X /\ Q .< X ) ) -> P e. A ) |
10 |
|
simp22 |
|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ X e. B ) /\ ( P .<_ X /\ Q .< X ) ) -> Q e. A ) |
11 |
|
eqid |
|- ( join ` K ) = ( join ` K ) |
12 |
3 11 4
|
atlt |
|- ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .< ( P ( join ` K ) Q ) <-> P =/= Q ) ) |
13 |
8 9 10 12
|
syl3anc |
|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ X e. B ) /\ ( P .<_ X /\ Q .< X ) ) -> ( P .< ( P ( join ` K ) Q ) <-> P =/= Q ) ) |
14 |
|
simp3l |
|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ X e. B ) /\ ( P .<_ X /\ Q .< X ) ) -> P .<_ X ) |
15 |
|
simp23 |
|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ X e. B ) /\ ( P .<_ X /\ Q .< X ) ) -> X e. B ) |
16 |
8 10 15
|
3jca |
|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ X e. B ) /\ ( P .<_ X /\ Q .< X ) ) -> ( K e. HL /\ Q e. A /\ X e. B ) ) |
17 |
2 3
|
pltle |
|- ( ( K e. HL /\ Q e. A /\ X e. B ) -> ( Q .< X -> Q .<_ X ) ) |
18 |
16 5 17
|
sylc |
|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ X e. B ) /\ ( P .<_ X /\ Q .< X ) ) -> Q .<_ X ) |
19 |
|
hllat |
|- ( K e. HL -> K e. Lat ) |
20 |
19
|
3ad2ant1 |
|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ X e. B ) /\ ( P .<_ X /\ Q .< X ) ) -> K e. Lat ) |
21 |
1 4
|
atbase |
|- ( P e. A -> P e. B ) |
22 |
9 21
|
syl |
|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ X e. B ) /\ ( P .<_ X /\ Q .< X ) ) -> P e. B ) |
23 |
1 4
|
atbase |
|- ( Q e. A -> Q e. B ) |
24 |
10 23
|
syl |
|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ X e. B ) /\ ( P .<_ X /\ Q .< X ) ) -> Q e. B ) |
25 |
1 2 11
|
latjle12 |
|- ( ( K e. Lat /\ ( P e. B /\ Q e. B /\ X e. B ) ) -> ( ( P .<_ X /\ Q .<_ X ) <-> ( P ( join ` K ) Q ) .<_ X ) ) |
26 |
20 22 24 15 25
|
syl13anc |
|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ X e. B ) /\ ( P .<_ X /\ Q .< X ) ) -> ( ( P .<_ X /\ Q .<_ X ) <-> ( P ( join ` K ) Q ) .<_ X ) ) |
27 |
14 18 26
|
mpbi2and |
|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ X e. B ) /\ ( P .<_ X /\ Q .< X ) ) -> ( P ( join ` K ) Q ) .<_ X ) |
28 |
|
hlpos |
|- ( K e. HL -> K e. Poset ) |
29 |
28
|
3ad2ant1 |
|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ X e. B ) /\ ( P .<_ X /\ Q .< X ) ) -> K e. Poset ) |
30 |
1 11
|
latjcl |
|- ( ( K e. Lat /\ P e. B /\ Q e. B ) -> ( P ( join ` K ) Q ) e. B ) |
31 |
20 22 24 30
|
syl3anc |
|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ X e. B ) /\ ( P .<_ X /\ Q .< X ) ) -> ( P ( join ` K ) Q ) e. B ) |
32 |
1 2 3
|
pltletr |
|- ( ( K e. Poset /\ ( P e. B /\ ( P ( join ` K ) Q ) e. B /\ X e. B ) ) -> ( ( P .< ( P ( join ` K ) Q ) /\ ( P ( join ` K ) Q ) .<_ X ) -> P .< X ) ) |
33 |
29 22 31 15 32
|
syl13anc |
|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ X e. B ) /\ ( P .<_ X /\ Q .< X ) ) -> ( ( P .< ( P ( join ` K ) Q ) /\ ( P ( join ` K ) Q ) .<_ X ) -> P .< X ) ) |
34 |
27 33
|
mpan2d |
|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ X e. B ) /\ ( P .<_ X /\ Q .< X ) ) -> ( P .< ( P ( join ` K ) Q ) -> P .< X ) ) |
35 |
13 34
|
sylbird |
|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ X e. B ) /\ ( P .<_ X /\ Q .< X ) ) -> ( P =/= Q -> P .< X ) ) |
36 |
7 35
|
pm2.61dne |
|- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ X e. B ) /\ ( P .<_ X /\ Q .< X ) ) -> P .< X ) |