Metamath Proof Explorer


Theorem 2atlt

Description: Given an atom less than an element, there is another atom less than the element. (Contributed by NM, 6-May-2012)

Ref Expression
Hypotheses 2atomslt.b
|- B = ( Base ` K )
2atomslt.s
|- .< = ( lt ` K )
2atomslt.a
|- A = ( Atoms ` K )
Assertion 2atlt
|- ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ P .< X ) -> E. q e. A ( q =/= P /\ q .< X ) )

Proof

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 ) )