Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cdlemh1 Unicode version

Theorem cdlemh1 31237
 Description: Part of proof of Lemma H of [Crawley] p. 118. (Contributed by NM, 17-Jun-2013.)
Hypotheses
Ref Expression
cdlemh.b
cdlemh.l
cdlemh.j
cdlemh.m
cdlemh.a
cdlemh.h
cdlemh.t
cdlemh.r
cdlemh.s
Assertion
Ref Expression
cdlemh1

Proof of Theorem cdlemh1
StepHypRef Expression
1 cdlemh.s . . 3
21oveq1i 6044 . 2
3 simp11l 1068 . . . 4
4 simp11 987 . . . . 5
5 simp13 989 . . . . 5
6 simp12 988 . . . . 5
7 simp3r 986 . . . . . 6
87necomd 2647 . . . . 5
9 cdlemh.a . . . . . 6
10 cdlemh.h . . . . . 6
11 cdlemh.t . . . . . 6
12 cdlemh.r . . . . . 6
139, 10, 11, 12trlcocnvat 31146 . . . . 5
144, 5, 6, 8, 13syl121anc 1189 . . . 4
15 hllat 29786 . . . . . 6
163, 15syl 16 . . . . 5
17 simp2l 983 . . . . . 6
18 cdlemh.b . . . . . . 7
1918, 9atbase 29712 . . . . . 6
2017, 19syl 16 . . . . 5
2118, 10, 11, 12trlcl 30586 . . . . . 6
224, 5, 21syl2anc 643 . . . . 5
23 cdlemh.j . . . . . 6
2418, 23latjcl 14420 . . . . 5
2516, 20, 22, 24syl3anc 1184 . . . 4
26 simp2r 984 . . . . 5
2718, 23, 9hlatjcl 29789 . . . . 5
283, 26, 14, 27syl3anc 1184 . . . 4
29 cdlemh.l . . . . . 6
3029, 23, 9hlatlej2 29798 . . . . 5
313, 26, 14, 30syl3anc 1184 . . . 4
32 cdlemh.m . . . . 5
3318, 29, 23, 32, 9atmod4i1 30288 . . . 4
343, 14, 25, 28, 31, 33syl131anc 1197 . . 3
3510, 11ltrncnv 30568 . . . . . . . . 9
364, 6, 35syl2anc 643 . . . . . . . 8
3723, 10, 11, 12trljco2 31163 . . . . . . . 8
384, 5, 36, 37syl3anc 1184 . . . . . . 7
3910, 11, 12trlcnv 30587 . . . . . . . . 9
404, 6, 39syl2anc 643 . . . . . . . 8
4140oveq1d 6049 . . . . . . 7
4238, 41eqtrd 2433 . . . . . 6
4342oveq2d 6050 . . . . 5
4410, 11ltrnco 31141 . . . . . . . 8
454, 5, 36, 44syl3anc 1184 . . . . . . 7
4618, 10, 11, 12trlcl 30586 . . . . . . 7
474, 45, 46syl2anc 643 . . . . . 6
4818, 23latjass 14465 . . . . . 6
4916, 20, 22, 47, 48syl13anc 1186 . . . . 5
5018, 10, 11, 12trlcl 30586 . . . . . . 7
514, 6, 50syl2anc 643 . . . . . 6
5218, 23latjass 14465 . . . . . 6
5316, 20, 51, 47, 52syl13anc 1186 . . . . 5
5443, 49, 533eqtr4d 2443 . . . 4
5554oveq1d 6049 . . 3
56 simp3l 985 . . . . 5
5718, 9atbase 29712 . . . . . . 7
5826, 57syl 16 . . . . . 6
5918, 23latjcl 14420 . . . . . . 7
6016, 20, 51, 59syl3anc 1184 . . . . . 6
6118, 29, 23latjlej1 14435 . . . . . 6
6216, 58, 60, 47, 61syl13anc 1186 . . . . 5
6356, 62mpd 15 . . . 4
6418, 23latjcl 14420 . . . . . 6
6516, 60, 47, 64syl3anc 1184 . . . . 5
6618, 29, 32latleeqm2 14450 . . . . 5
6716, 28, 65, 66syl3anc 1184 . . . 4
6863, 67mpbid 202 . . 3
6934, 55, 683eqtrd 2437 . 2
702, 69syl5eq 2445 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359   w3a 936   wceq 1649   wcel 1721   wne 2564   class class class wbr 4167  ccnv 4831   ccom 4836  cfv 5408  (class class class)co 6034  cbs 13410  cple 13477  cjn 14342  cmee 14343  clat 14415  catm 29686  chlt 29773  clh 30406  cltrn 30523  ctrl 30580 This theorem is referenced by:  cdlemh  31239 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2382  ax-rep 4275  ax-sep 4285  ax-nul 4293  ax-pow 4332  ax-pr 4358  ax-un 4655 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2256  df-mo 2257  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2526  df-ne 2566  df-nel 2567  df-ral 2668  df-rex 2669  df-reu 2670  df-rmo 2671  df-rab 2672  df-v 2915  df-sbc 3119  df-csb 3209  df-dif 3280  df-un 3282  df-in 3284  df-ss 3291  df-nul 3586  df-if 3697  df-pw 3758  df-sn 3777  df-pr 3778  df-op 3780  df-uni 3972  df-iun 4051  df-iin 4052  df-br 4168  df-opab 4222  df-mpt 4223  df-id 4453  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5372  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-ov 6037  df-oprab 6038  df-mpt2 6039  df-1st 6302  df-2nd 6303  df-undef 6493  df-riota 6499  df-map 6970  df-poset 14344  df-plt 14356  df-lub 14372  df-glb 14373  df-join 14374  df-meet 14375  df-p0 14409  df-p1 14410  df-lat 14416  df-clat 14478  df-oposet 29599  df-ol 29601  df-oml 29602  df-covers 29689  df-ats 29690  df-atl 29721  df-cvlat 29745  df-hlat 29774  df-llines 29920  df-lplanes 29921  df-lvols 29922  df-lines 29923  df-psubsp 29925  df-pmap 29926  df-padd 30218  df-lhyp 30410  df-laut 30411  df-ldil 30526  df-ltrn 30527  df-trl 30581
 Copyright terms: Public domain W3C validator