Metamath Proof Explorer

Theorem 1cvratex

Description: There exists an atom less than an element covered by 1. (Contributed by NM, 7-May-2012) (Revised by Mario Carneiro, 13-Jun-2014)

Ref Expression
Hypotheses 1cvratex.b 
|- B = ( Base ` K )
1cvratex.s 
|- .< = ( lt ` K )
1cvratex.u 
|- .1. = ( 1. ` K )
1cvratex.c 
|- C = (
1cvratex.a 
|- A = ( Atoms ` K )
Assertion 1cvratex 
|- ( ( K e. HL /\ X e. B /\ X C .1. ) -> E. p e. A p .< X )

Proof

Step Hyp Ref Expression
1 1cvratex.b 
 |-  B = ( Base ` K )
2 1cvratex.s 
 |-  .< = ( lt ` K )
3 1cvratex.u 
 |-  .1. = ( 1. ` K )
4 1cvratex.c 
 |-  C = (
5 1cvratex.a 
 |-  A = ( Atoms ` K )
6 simp1 
 |-  ( ( K e. HL /\ X e. B /\ X C .1. ) -> K e. HL )
7 eqid 
 |-  ( oc ` K ) = ( oc ` K )
8 1 3 7 4 5 1cvrco 
 |-  ( ( K e. HL /\ X e. B ) -> ( X C .1. <-> ( ( oc ` K ) ` X ) e. A ) )
9 8 biimp3a 
 |-  ( ( K e. HL /\ X e. B /\ X C .1. ) -> ( ( oc ` K ) ` X ) e. A )
10 eqid 
 |-  ( join ` K ) = ( join ` K )
11 10 4 5 2dim 
 |-  ( ( K e. HL /\ ( ( oc ` K ) ` X ) e. A ) -> E. q e. A E. r e. A ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) )
12 6 9 11 syl2anc 
 |-  ( ( K e. HL /\ X e. B /\ X C .1. ) -> E. q e. A E. r e. A ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) )
13 simp11 
 |-  ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) -> K e. HL )
14 hlop 
 |-  ( K e. HL -> K e. OP )
15 13 14 syl 
 |-  ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) -> K e. OP )
16 13 hllatd 
 |-  ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) -> K e. Lat )
17 simp12 
 |-  ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) -> X e. B )
18 1 7 opoccl 
 |-  ( ( K e. OP /\ X e. B ) -> ( ( oc ` K ) ` X ) e. B )
19 15 17 18 syl2anc 
 |-  ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) -> ( ( oc ` K ) ` X ) e. B )
20 simp2l 
 |-  ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) -> q e. A )
21 1 5 atbase 
 |-  ( q e. A -> q e. B )
22 20 21 syl 
 |-  ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) -> q e. B )
23 1 10 latjcl 
 |-  ( ( K e. Lat /\ ( ( oc ` K ) ` X ) e. B /\ q e. B ) -> ( ( ( oc ` K ) ` X ) ( join ` K ) q ) e. B )
24 16 19 22 23 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) -> ( ( ( oc ` K ) ` X ) ( join ` K ) q ) e. B )
25 1 7 opoccl 
 |-  ( ( K e. OP /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) e. B ) -> ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ) e. B )
26 15 24 25 syl2anc 
 |-  ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) -> ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ) e. B )
27 simp2r 
 |-  ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) -> r e. A )
28 1 5 atbase 
 |-  ( r e. A -> r e. B )
29 27 28 syl 
 |-  ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) -> r e. B )
30 1 10 latjcl 
 |-  ( ( K e. Lat /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) e. B /\ r e. B ) -> ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) e. B )
31 16 24 29 30 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) -> ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) e. B )
32 1 7 opoccl 
 |-  ( ( K e. OP /\ ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) e. B ) -> ( ( oc ` K ) ` ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) e. B )
33 15 31 32 syl2anc 
 |-  ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) -> ( ( oc ` K ) ` ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) e. B )
34 eqid 
 |-  ( le ` K ) = ( le ` K )
35 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
36 1 34 35 op0le 
 |-  ( ( K e. OP /\ ( ( oc ` K ) ` ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) e. B ) -> ( 0. ` K ) ( le ` K ) ( ( oc ` K ) ` ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) )
37 15 33 36 syl2anc 
 |-  ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) -> ( 0. ` K ) ( le ` K ) ( ( oc ` K ) ` ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) )
38 simp3r 
 |-  ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) -> ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) )
39 1 2 4 cvrlt 
 |-  ( ( ( K e. HL /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) e. B /\ ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) e. B ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) -> ( ( ( oc ` K ) ` X ) ( join ` K ) q ) .< ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) )
40 13 24 31 38 39 syl31anc 
 |-  ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) -> ( ( ( oc ` K ) ` X ) ( join ` K ) q ) .< ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) )
41 1 2 7 opltcon3b 
 |-  ( ( K e. OP /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) e. B /\ ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) e. B ) -> ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) .< ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) <-> ( ( oc ` K ) ` ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) .< ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ) ) )
42 15 24 31 41 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) -> ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) .< ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) <-> ( ( oc ` K ) ` ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) .< ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ) ) )
43 40 42 mpbid 
 |-  ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) -> ( ( oc ` K ) ` ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) .< ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ) )
44 hlpos 
 |-  ( K e. HL -> K e. Poset )
45 13 44 syl 
 |-  ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) -> K e. Poset )
46 1 35 op0cl 
 |-  ( K e. OP -> ( 0. ` K ) e. B )
47 15 46 syl 
 |-  ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) -> ( 0. ` K ) e. B )
48 1 34 2 plelttr 
 |-  ( ( K e. Poset /\ ( ( 0. ` K ) e. B /\ ( ( oc ` K ) ` ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) e. B /\ ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ) e. B ) ) -> ( ( ( 0. ` K ) ( le ` K ) ( ( oc ` K ) ` ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) /\ ( ( oc ` K ) ` ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) .< ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ) ) -> ( 0. ` K ) .< ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ) ) )
49 45 47 33 26 48 syl13anc 
 |-  ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) -> ( ( ( 0. ` K ) ( le ` K ) ( ( oc ` K ) ` ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) /\ ( ( oc ` K ) ` ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) .< ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ) ) -> ( 0. ` K ) .< ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ) ) )
50 37 43 49 mp2and 
 |-  ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) -> ( 0. ` K ) .< ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ) )
51 2 pltne 
 |-  ( ( K e. HL /\ ( 0. ` K ) e. B /\ ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ) e. B ) -> ( ( 0. ` K ) .< ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ) -> ( 0. ` K ) =/= ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ) ) )
52 13 47 26 51 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) -> ( ( 0. ` K ) .< ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ) -> ( 0. ` K ) =/= ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ) ) )
53 50 52 mpd 
 |-  ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) -> ( 0. ` K ) =/= ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ) )
54 53 necomd 
 |-  ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) -> ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ) =/= ( 0. ` K ) )
55 1 34 35 5 atle 
 |-  ( ( K e. HL /\ ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ) e. B /\ ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ) =/= ( 0. ` K ) ) -> E. p e. A p ( le ` K ) ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ) )
56 13 26 54 55 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) -> E. p e. A p ( le ` K ) ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ) )
57 simp3l 
 |-  ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) -> ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) )
58 1 2 4 cvrlt 
 |-  ( ( ( K e. HL /\ ( ( oc ` K ) ` X ) e. B /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) e. B ) /\ ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ) -> ( ( oc ` K ) ` X ) .< ( ( ( oc ` K ) ` X ) ( join ` K ) q ) )
59 13 19 24 57 58 syl31anc 
 |-  ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) -> ( ( oc ` K ) ` X ) .< ( ( ( oc ` K ) ` X ) ( join ` K ) q ) )
60 1 2 7 opltcon3b 
 |-  ( ( K e. OP /\ ( ( oc ` K ) ` X ) e. B /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) e. B ) -> ( ( ( oc ` K ) ` X ) .< ( ( ( oc ` K ) ` X ) ( join ` K ) q ) <-> ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ) .< ( ( oc ` K ) ` ( ( oc ` K ) ` X ) ) ) )
61 15 19 24 60 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) -> ( ( ( oc ` K ) ` X ) .< ( ( ( oc ` K ) ` X ) ( join ` K ) q ) <-> ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ) .< ( ( oc ` K ) ` ( ( oc ` K ) ` X ) ) ) )
62 59 61 mpbid 
 |-  ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) -> ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ) .< ( ( oc ` K ) ` ( ( oc ` K ) ` X ) ) )
63 1 7 opococ 
 |-  ( ( K e. OP /\ X e. B ) -> ( ( oc ` K ) ` ( ( oc ` K ) ` X ) ) = X )
64 15 17 63 syl2anc 
 |-  ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) -> ( ( oc ` K ) ` ( ( oc ` K ) ` X ) ) = X )
65 62 64 breqtrd 
 |-  ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) -> ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ) .< X )
66 65 adantr 
 |-  ( ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) /\ p e. A ) -> ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ) .< X )
67 simpl11 
 |-  ( ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) /\ p e. A ) -> K e. HL )
68 67 44 syl 
 |-  ( ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) /\ p e. A ) -> K e. Poset )
69 1 5 atbase 
 |-  ( p e. A -> p e. B )
70 69 adantl 
 |-  ( ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) /\ p e. A ) -> p e. B )
71 26 adantr 
 |-  ( ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) /\ p e. A ) -> ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ) e. B )
72 simpl12 
 |-  ( ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) /\ p e. A ) -> X e. B )
73 1 34 2 plelttr 
 |-  ( ( K e. Poset /\ ( p e. B /\ ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ) e. B /\ X e. B ) ) -> ( ( p ( le ` K ) ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ) /\ ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ) .< X ) -> p .< X ) )
74 68 70 71 72 73 syl13anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) /\ p e. A ) -> ( ( p ( le ` K ) ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ) /\ ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ) .< X ) -> p .< X ) )
75 66 74 mpan2d 
 |-  ( ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) /\ p e. A ) -> ( p ( le ` K ) ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ) -> p .< X ) )
76 75 reximdva 
 |-  ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) -> ( E. p e. A p ( le ` K ) ( ( oc ` K ) ` ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ) -> E. p e. A p .< X ) )
77 56 76 mpd 
 |-  ( ( ( K e. HL /\ X e. B /\ X C .1. ) /\ ( q e. A /\ r e. A ) /\ ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) ) -> E. p e. A p .< X )
78 77 3exp 
 |-  ( ( K e. HL /\ X e. B /\ X C .1. ) -> ( ( q e. A /\ r e. A ) -> ( ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) -> E. p e. A p .< X ) ) )
79 78 rexlimdvv 
 |-  ( ( K e. HL /\ X e. B /\ X C .1. ) -> ( E. q e. A E. r e. A ( ( ( oc ` K ) ` X ) C ( ( ( oc ` K ) ` X ) ( join ` K ) q ) /\ ( ( ( oc ` K ) ` X ) ( join ` K ) q ) C ( ( ( ( oc ` K ) ` X ) ( join ` K ) q ) ( join ` K ) r ) ) -> E. p e. A p .< X ) )
80 12 79 mpd 
 |-  ( ( K e. HL /\ X e. B /\ X C .1. ) -> E. p e. A p .< X )