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

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

Proof of Theorem latmle2
StepHypRef Expression
1 latmle.b . 2 𝐵 = (Base‘𝐾)
2 latmle.l . 2 = (le‘𝐾)
3 latmle.m . 2 = (meet‘𝐾)
4 simp1 1159 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → 𝐾 ∈ Lat)
5 simp2 1160 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → 𝑋𝐵)
6 simp3 1161 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → 𝑌𝐵)
7 eqid 2813 . . . 4 (join‘𝐾) = (join‘𝐾)
81, 7, 3, 4, 5, 6latcl2 17256 . . 3 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (⟨𝑋, 𝑌⟩ ∈ dom (join‘𝐾) ∧ ⟨𝑋, 𝑌⟩ ∈ dom ))
98simprd 485 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → ⟨𝑋, 𝑌⟩ ∈ dom )
101, 2, 3, 4, 5, 6, 9lemeet2 17235 1 ((𝐾 ∈ Lat ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) 𝑌)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1100   = wceq 1637  wcel 2157  cop 4383   class class class wbr 4851  dom cdm 5318  cfv 6104  (class class class)co 6877  Basecbs 16071  lecple 16163  joincjn 17152  meetcmee 17153  Latclat 17253
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-rep 4971  ax-sep 4982  ax-nul 4990  ax-pow 5042  ax-pr 5103  ax-un 7182
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ne 2986  df-ral 3108  df-rex 3109  df-reu 3110  df-rab 3112  df-v 3400  df-sbc 3641  df-csb 3736  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-nul 4124  df-if 4287  df-pw 4360  df-sn 4378  df-pr 4380  df-op 4384  df-uni 4638  df-iun 4721  df-br 4852  df-opab 4914  df-mpt 4931  df-id 5226  df-xp 5324  df-rel 5325  df-cnv 5326  df-co 5327  df-dm 5328  df-rn 5329  df-res 5330  df-ima 5331  df-iota 6067  df-fun 6106  df-fn 6107  df-f 6108  df-f1 6109  df-fo 6110  df-f1o 6111  df-fv 6112  df-riota 6838  df-ov 6880  df-oprab 6881  df-glb 17183  df-meet 17185  df-lat 17254
This theorem is referenced by:  latmlem1  17289  latledi  17297  mod1ile  17313  oldmm1  34999  olm01  35018  cmtcomlemN  35030  cmtbr4N  35037  meetat  35078  cvrexchlem  35201  cvrat4  35225  2llnmj  35342  2lplnmj  35404  dalem25  35480  dalem54  35508  dalem57  35511  cdlema1N  35573  cdlemb  35576  llnexchb2lem  35650  llnexch2N  35652  dalawlem1  35653  dalawlem3  35655  pl42lem1N  35761  lhpelim  35819  lhpat3  35828  4atexlemunv  35848  4atexlemtlw  35849  4atexlemnclw  35852  4atexlemex2  35853  lautm  35876  trlle  35966  cdlemc2  35974  cdlemc5  35977  cdlemd2  35981  cdleme0b  35994  cdleme0c  35995  cdleme0fN  36000  cdleme01N  36003  cdleme0ex1N  36005  cdleme2  36010  cdleme3b  36011  cdleme3c  36012  cdleme3g  36016  cdleme3h  36017  cdleme7aa  36024  cdleme7c  36027  cdleme7d  36028  cdleme7e  36029  cdleme7ga  36030  cdleme11fN  36046  cdleme11k  36050  cdleme15d  36059  cdleme16f  36065  cdlemednpq  36081  cdleme19c  36087  cdleme20aN  36091  cdleme20c  36093  cdleme20j  36100  cdleme21c  36109  cdleme21ct  36111  cdleme22cN  36124  cdleme22f  36128  cdleme23a  36131  cdleme28a  36152  cdleme35d  36234  cdleme35f  36236  cdlemeg46frv  36307  cdlemeg46rgv  36310  cdlemeg46req  36311  cdlemg2fv2  36382  cdlemg2m  36386  cdlemg4  36399  cdlemg10bALTN  36418  cdlemg31b  36480  trlcolem  36508  cdlemk14  36636  dia2dimlem1  36846  docaclN  36906  doca2N  36908  djajN  36919  dihjustlem  36998  dihord1  37000  dihord2a  37001  dihord2b  37002  dihord2cN  37003  dihord11b  37004  dihord11c  37006  dihord2pre  37007  dihlsscpre  37016  dihvalcq2  37029  dihopelvalcpre  37030  dihord6apre  37038  dihord5b  37041  dihord5apre  37044  dihmeetlem1N  37072  dihglblem5apreN  37073  dihglblem3N  37077  dihmeetbclemN  37086  dihmeetlem4preN  37088  dihmeetlem7N  37092  dihmeetlem9N  37097  dihjatcclem4  37203
  Copyright terms: Public domain W3C validator