MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  latmle1 Structured version   Visualization version   GIF version

Theorem latmle1 17674
Description: A meet is less than or equal to its first argument. (Contributed by NM, 21-Oct-2011.)
Hypotheses
Ref Expression
latmle.b 𝐵 = (Base‘𝐾)
latmle.l = (le‘𝐾)
latmle.m = (meet‘𝐾)
Assertion
Ref Expression
latmle1 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) 𝑋)

Proof of Theorem latmle1
StepHypRef Expression
1 latmle.b . 2 𝐵 = (Base‘𝐾)
2 latmle.l . 2 = (le‘𝐾)
3 latmle.m . 2 = (meet‘𝐾)
4 simp1 1128 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → 𝐾 ∈ Lat)
5 simp2 1129 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → 𝑋𝐵)
6 simp3 1130 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → 𝑌𝐵)
7 eqid 2818 . . . 4 (join‘𝐾) = (join‘𝐾)
81, 7, 3, 4, 5, 6latcl2 17646 . . 3 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (⟨𝑋, 𝑌⟩ ∈ dom (join‘𝐾) ∧ ⟨𝑋, 𝑌⟩ ∈ dom ))
98simprd 496 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ⟨𝑋, 𝑌⟩ ∈ dom )
101, 2, 3, 4, 5, 6, 9lemeet1 17624 1 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) 𝑋)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1079   = wceq 1528  wcel 2105  cop 4563   class class class wbr 5057  dom cdm 5548  cfv 6348  (class class class)co 7145  Basecbs 16471  lecple 16560  joincjn 17542  meetcmee 17543  Latclat 17643
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-reu 3142  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7103  df-ov 7148  df-oprab 7149  df-glb 17573  df-meet 17575  df-lat 17644
This theorem is referenced by:  latleeqm1  17677  latmlem1  17679  latnlemlt  17682  latmidm  17684  latabs1  17685  latledi  17687  latmlej11  17688  oldmm1  36233  cmtbr3N  36270  cmtbr4N  36271  lecmtN  36272  cvrat4  36459  2llnmat  36540  llnmlplnN  36555  dalem3  36680  dalem27  36715  dalem54  36742  dalem55  36743  2lnat  36800  cdlema1N  36807  llnexchb2lem  36884  dalawlem1  36887  dalawlem6  36892  dalawlem11  36897  dalawlem12  36898  4atexlemunv  37082  4atexlemc  37085  4atexlemnclw  37086  4atexlemex2  37087  4atexlemcnd  37088  lautm  37110  trlval3  37203  cdlemeulpq  37236  cdleme3h  37251  cdleme4a  37255  cdleme9  37269  cdleme11g  37281  cdleme13  37288  cdleme16e  37298  cdlemednpq  37315  cdleme19b  37320  cdleme20e  37329  cdleme20j  37334  cdleme22cN  37358  cdleme22e  37360  cdleme22eALTN  37361  cdleme22g  37364  cdleme35b  37466  cdleme35f  37470  cdlemeg46vrg  37543  cdlemg11b  37658  cdlemg12f  37664  cdlemg19a  37699  cdlemg31a  37713  cdlemk12  37866  cdlemkole  37869  cdlemk12u  37888  cdlemk37  37930  dia2dimlem1  38080  dihopelvalcpre  38264  dihmeetlem1N  38306  dihglblem5apreN  38307  dihglblem2N  38310  dihmeetlem2N  38315
  Copyright terms: Public domain W3C validator