Step |
Hyp |
Ref |
Expression |
1 |
|
2atomslt.b |
|- B = ( Base ` K ) |
2 |
|
2atomslt.s |
|- .< = ( lt ` K ) |
3 |
|
2atomslt.a |
|- A = ( Atoms ` K ) |
4 |
1 3
|
atbase |
|- ( P e. A -> P e. B ) |
5 |
|
eqid |
|- ( le ` K ) = ( le ` K ) |
6 |
|
eqid |
|- ( join ` K ) = ( join ` K ) |
7 |
1 5 2 6 3
|
hlrelat |
|- ( ( ( K e. HL /\ P e. B /\ X e. B ) /\ P .< X ) -> E. q e. A ( P .< ( P ( join ` K ) q ) /\ ( P ( join ` K ) q ) ( le ` K ) X ) ) |
8 |
4 7
|
syl3anl2 |
|- ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ P .< X ) -> E. q e. A ( P .< ( P ( join ` K ) q ) /\ ( P ( join ` K ) q ) ( le ` K ) X ) ) |
9 |
|
simp3l |
|- ( ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ P .< X ) /\ q e. A /\ ( P .< ( P ( join ` K ) q ) /\ ( P ( join ` K ) q ) ( le ` K ) X ) ) -> P .< ( P ( join ` K ) q ) ) |
10 |
|
simp1l1 |
|- ( ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ P .< X ) /\ q e. A /\ ( P .< ( P ( join ` K ) q ) /\ ( P ( join ` K ) q ) ( le ` K ) X ) ) -> K e. HL ) |
11 |
|
simp1l2 |
|- ( ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ P .< X ) /\ q e. A /\ ( P .< ( P ( join ` K ) q ) /\ ( P ( join ` K ) q ) ( le ` K ) X ) ) -> P e. A ) |
12 |
|
simp2 |
|- ( ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ P .< X ) /\ q e. A /\ ( P .< ( P ( join ` K ) q ) /\ ( P ( join ` K ) q ) ( le ` K ) X ) ) -> q e. A ) |
13 |
|
eqid |
|- ( |
14 |
2 6 3 13
|
atltcvr |
|- ( ( K e. HL /\ ( P e. A /\ P e. A /\ q e. A ) ) -> ( P .< ( P ( join ` K ) q ) <-> P ( |
15 |
10 11 11 12 14
|
syl13anc |
|- ( ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ P .< X ) /\ q e. A /\ ( P .< ( P ( join ` K ) q ) /\ ( P ( join ` K ) q ) ( le ` K ) X ) ) -> ( P .< ( P ( join ` K ) q ) <-> P ( |
16 |
9 15
|
mpbid |
|- ( ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ P .< X ) /\ q e. A /\ ( P .< ( P ( join ` K ) q ) /\ ( P ( join ` K ) q ) ( le ` K ) X ) ) -> P ( |
17 |
6 13 3
|
atcvr1 |
|- ( ( K e. HL /\ P e. A /\ q e. A ) -> ( P =/= q <-> P ( |
18 |
10 11 12 17
|
syl3anc |
|- ( ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ P .< X ) /\ q e. A /\ ( P .< ( P ( join ` K ) q ) /\ ( P ( join ` K ) q ) ( le ` K ) X ) ) -> ( P =/= q <-> P ( |
19 |
16 18
|
mpbird |
|- ( ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ P .< X ) /\ q e. A /\ ( P .< ( P ( join ` K ) q ) /\ ( P ( join ` K ) q ) ( le ` K ) X ) ) -> P =/= q ) |
20 |
19
|
necomd |
|- ( ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ P .< X ) /\ q e. A /\ ( P .< ( P ( join ` K ) q ) /\ ( P ( join ` K ) q ) ( le ` K ) X ) ) -> q =/= P ) |
21 |
2 6 3
|
atlt |
|- ( ( K e. HL /\ q e. A /\ P e. A ) -> ( q .< ( q ( join ` K ) P ) <-> q =/= P ) ) |
22 |
10 12 11 21
|
syl3anc |
|- ( ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ P .< X ) /\ q e. A /\ ( P .< ( P ( join ` K ) q ) /\ ( P ( join ` K ) q ) ( le ` K ) X ) ) -> ( q .< ( q ( join ` K ) P ) <-> q =/= P ) ) |
23 |
20 22
|
mpbird |
|- ( ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ P .< X ) /\ q e. A /\ ( P .< ( P ( join ` K ) q ) /\ ( P ( join ` K ) q ) ( le ` K ) X ) ) -> q .< ( q ( join ` K ) P ) ) |
24 |
10
|
hllatd |
|- ( ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ P .< X ) /\ q e. A /\ ( P .< ( P ( join ` K ) q ) /\ ( P ( join ` K ) q ) ( le ` K ) X ) ) -> K e. Lat ) |
25 |
11 4
|
syl |
|- ( ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ P .< X ) /\ q e. A /\ ( P .< ( P ( join ` K ) q ) /\ ( P ( join ` K ) q ) ( le ` K ) X ) ) -> P e. B ) |
26 |
1 3
|
atbase |
|- ( q e. A -> q e. B ) |
27 |
26
|
3ad2ant2 |
|- ( ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ P .< X ) /\ q e. A /\ ( P .< ( P ( join ` K ) q ) /\ ( P ( join ` K ) q ) ( le ` K ) X ) ) -> q e. B ) |
28 |
1 6
|
latjcom |
|- ( ( K e. Lat /\ P e. B /\ q e. B ) -> ( P ( join ` K ) q ) = ( q ( join ` K ) P ) ) |
29 |
24 25 27 28
|
syl3anc |
|- ( ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ P .< X ) /\ q e. A /\ ( P .< ( P ( join ` K ) q ) /\ ( P ( join ` K ) q ) ( le ` K ) X ) ) -> ( P ( join ` K ) q ) = ( q ( join ` K ) P ) ) |
30 |
23 29
|
breqtrrd |
|- ( ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ P .< X ) /\ q e. A /\ ( P .< ( P ( join ` K ) q ) /\ ( P ( join ` K ) q ) ( le ` K ) X ) ) -> q .< ( P ( join ` K ) q ) ) |
31 |
|
simp3r |
|- ( ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ P .< X ) /\ q e. A /\ ( P .< ( P ( join ` K ) q ) /\ ( P ( join ` K ) q ) ( le ` K ) X ) ) -> ( P ( join ` K ) q ) ( le ` K ) X ) |
32 |
|
hlpos |
|- ( K e. HL -> K e. Poset ) |
33 |
10 32
|
syl |
|- ( ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ P .< X ) /\ q e. A /\ ( P .< ( P ( join ` K ) q ) /\ ( P ( join ` K ) q ) ( le ` K ) X ) ) -> K e. Poset ) |
34 |
1 6
|
latjcl |
|- ( ( K e. Lat /\ P e. B /\ q e. B ) -> ( P ( join ` K ) q ) e. B ) |
35 |
24 25 27 34
|
syl3anc |
|- ( ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ P .< X ) /\ q e. A /\ ( P .< ( P ( join ` K ) q ) /\ ( P ( join ` K ) q ) ( le ` K ) X ) ) -> ( P ( join ` K ) q ) e. B ) |
36 |
|
simp1l3 |
|- ( ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ P .< X ) /\ q e. A /\ ( P .< ( P ( join ` K ) q ) /\ ( P ( join ` K ) q ) ( le ` K ) X ) ) -> X e. B ) |
37 |
1 5 2
|
pltletr |
|- ( ( K e. Poset /\ ( q e. B /\ ( P ( join ` K ) q ) e. B /\ X e. B ) ) -> ( ( q .< ( P ( join ` K ) q ) /\ ( P ( join ` K ) q ) ( le ` K ) X ) -> q .< X ) ) |
38 |
33 27 35 36 37
|
syl13anc |
|- ( ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ P .< X ) /\ q e. A /\ ( P .< ( P ( join ` K ) q ) /\ ( P ( join ` K ) q ) ( le ` K ) X ) ) -> ( ( q .< ( P ( join ` K ) q ) /\ ( P ( join ` K ) q ) ( le ` K ) X ) -> q .< X ) ) |
39 |
30 31 38
|
mp2and |
|- ( ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ P .< X ) /\ q e. A /\ ( P .< ( P ( join ` K ) q ) /\ ( P ( join ` K ) q ) ( le ` K ) X ) ) -> q .< X ) |
40 |
20 39
|
jca |
|- ( ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ P .< X ) /\ q e. A /\ ( P .< ( P ( join ` K ) q ) /\ ( P ( join ` K ) q ) ( le ` K ) X ) ) -> ( q =/= P /\ q .< X ) ) |
41 |
40
|
3exp |
|- ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ P .< X ) -> ( q e. A -> ( ( P .< ( P ( join ` K ) q ) /\ ( P ( join ` K ) q ) ( le ` K ) X ) -> ( q =/= P /\ q .< X ) ) ) ) |
42 |
41
|
reximdvai |
|- ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ P .< X ) -> ( E. q e. A ( P .< ( P ( join ` K ) q ) /\ ( P ( join ` K ) q ) ( le ` K ) X ) -> E. q e. A ( q =/= P /\ q .< X ) ) ) |
43 |
8 42
|
mpd |
|- ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ P .< X ) -> E. q e. A ( q =/= P /\ q .< X ) ) |