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

Theorem dihjatcclem3 32614
Description: Lemma for dihjatcc 32616. (Contributed by NM, 28-Sep-2014.)
Hypotheses
Ref Expression
dihjatcclem.b
dihjatcclem.l
dihjatcclem.h
dihjatcclem.j
dihjatcclem.m
dihjatcclem.a
dihjatcclem.u
dihjatcclem.s
dihjatcclem.i
dihjatcclem.v
dihjatcclem.k
dihjatcclem.p
dihjatcclem.q
dihjatcc.w
dihjatcc.t
dihjatcc.r
dihjatcc.e
dihjatcc.g
dihjatcc.dd
Assertion
Ref Expression
dihjatcclem3
Distinct variable groups:   ,   ,   ,   ,   ,   P,   ,   Q,   ,   ,
Allowed substitution hints:   ( )   ( )   ( )   ( )   ( )   ( )   ( )   I( )   ( )   ( )   ( )

Proof of Theorem dihjatcclem3
StepHypRef Expression
1 dihjatcclem.k . . 3
2 dihjatcclem.l . . . . . . 7
3 dihjatcclem.a . . . . . . 7
4 dihjatcclem.h . . . . . . 7
5 dihjatcc.w . . . . . . 7
62, 3, 4, 5lhpocnel2 31212 . . . . . 6
71, 6syl 16 . . . . 5
8 dihjatcclem.p . . . . 5
9 dihjatcc.t . . . . . 6
10 dihjatcc.g . . . . . 6
112, 3, 4, 9, 10ltrniotacl 31772 . . . . 5
121, 7, 8, 11syl3anc 1185 . . . 4
13 dihjatcclem.q . . . . . 6
14 dihjatcc.dd . . . . . . 7
152, 3, 4, 9, 14ltrniotacl 31772 . . . . . 6
161, 7, 13, 15syl3anc 1185 . . . . 5
174, 9ltrncnv 31339 . . . . 5
181, 16, 17syl2anc 644 . . . 4
194, 9ltrnco 31912 . . . 4
201, 12, 18, 19syl3anc 1185 . . 3
21 dihjatcclem.j . . . 4
22 dihjatcclem.m . . . 4
23 dihjatcc.r . . . 4
242, 21, 22, 3, 4, 9, 23trlval2 31356 . . 3
251, 20, 13, 24syl3anc 1185 . 2
2613simpld 447 . . . . . . . 8
272, 3, 4, 9ltrncoval 31338 . . . . . . . 8
281, 12, 18, 26, 27syl121anc 1190 . . . . . . 7
292, 3, 4, 9, 14ltrniotacnvval 31775 . . . . . . . . . 10
301, 7, 13, 29syl3anc 1185 . . . . . . . . 9
3130fveq2d 5783 . . . . . . . 8
322, 3, 4, 9, 10ltrniotaval 31774 . . . . . . . . 9
331, 7, 8, 32syl3anc 1185 . . . . . . . 8
3431, 33eqtrd 2479 . . . . . . 7
3528, 34eqtrd 2479 . . . . . 6
3635oveq2d 6149 . . . . 5
371simpld 447 . . . . . 6
388simpld 447 . . . . . 6
3921, 3hlatjcom 30561 . . . . . 6
4037, 38, 26, 39syl3anc 1185 . . . . 5
4136, 40eqtr4d 2482 . . . 4
4241oveq1d 6148 . . 3
43 dihjatcclem.v . . 3
4442, 43syl6eqr 2497 . 2
4525, 44eqtrd 2479 1
Colors of variables: wff set class
Syntax hints:  -.wn 3  ->wi 4  /\wa 360  =wceq 1654  e.wcel 1728   class class class wbr 4247  `'ccnv 4922  o.ccom 4927  `cfv 5505  (class class class)co 6133  iota_crio 6596   cbs 13524   cple 13591   coc 13592   cjn 14456   cmee 14457   clsm 15304   catm 30457   chlt 30544   clh 31177   cltrn 31294   ctrl 31351   ctendo 31945   cdvh 32272   cdih 32422
This theorem is referenced by:  dihjatcclem4  32615
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-13 1730  ax-14 1732  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1955  ax-ext 2428  ax-rep 4358  ax-sep 4368  ax-nul 4376  ax-pow 4420  ax-pr 4446  ax-un 4746
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-eu 2296  df-mo 2297  df-clab 2434  df-cleq 2440  df-clel 2443  df-nfc 2572  df-ne 2612  df-nel 2613  df-ral 2721  df-rex 2722  df-reu 2723  df-rmo 2724  df-rab 2725  df-v 2971  df-sbc 3175  df-csb 3275  df-dif 3316  df-un 3318  df-in 3320  df-ss 3327  df-nul 3621  df-if 3770  df-pw 3832  df-sn 3851  df-pr 3852  df-op 3854  df-uni 4048  df-iun 4128  df-iin 4129  df-br 4248  df-opab 4306  df-mpt 4307  df-id 4543  df-xp 4929  df-rel 4930  df-cnv 4931  df-co 4932  df-dm 4933  df-rn 4934  df-res 4935  df-ima 4936  df-iota 5468  df-fun 5507  df-fn 5508  df-f 5509  df-f1 5510  df-fo 5511  df-f1o 5512  df-fv 5513  df-ov 6136  df-oprab 6137  df-mpt2 6138  df-1st 6403  df-2nd 6404  df-undef 6597  df-riota 6603  df-map 7073  df-poset 14458  df-plt 14470  df-lub 14486  df-glb 14487  df-join 14488  df-meet 14489  df-p0 14523  df-p1 14524  df-lat 14530  df-clat 14592  df-oposet 30370  df-ol 30372  df-oml 30373  df-covers 30460  df-ats 30461  df-atl 30492  df-cvlat 30516  df-hlat 30545  df-llines 30691  df-lplanes 30692  df-lvols 30693  df-lines 30694  df-psubsp 30696  df-pmap 30697  df-padd 30989  df-lhyp 31181  df-laut 31182  df-ldil 31297  df-ltrn 31298  df-trl 31352
  Copyright terms: Public domain W3C validator