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