Theorem latmle2 18522

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

Step	Hyp	Ref	Expression
1		latmle.b	. 2 ⊢ 𝐵 = (Base‘𝐾)
2		latmle.l	. 2 ⊢ ≤ = (le‘𝐾)
3		latmle.m	. 2 ⊢ ∧ = (meet‘𝐾)
4		simp1 1135	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ Lat)
5		simp2 1136	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∈ 𝐵)
6		simp3 1137	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝐵)
7		eqid 2734	. . . 4 ⊢ (join‘𝐾) = (join‘𝐾)
8	1, 7, 3, 4, 5, 6	latcl2 18493	. . 3 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (⟨𝑋, 𝑌⟩ ∈ dom (join‘𝐾) ∧ ⟨𝑋, 𝑌⟩ ∈ dom ∧ ))
9	8	simprd 495	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ⟨𝑋, 𝑌⟩ ∈ dom ∧ )
10	1, 2, 3, 4, 5, 6, 9	lemeet2 18456	1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ≤ 𝑌)

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1536   ∈ wcel 2105  ⟨cop 4636   class class class wbr 5147  dom cdm 5688  ‘cfv 6562  (class class class)co 7430  Basecbs 17244  lecple 17304  joincjn 18368  meetcmee 18369  Latclat 18488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-glb 18404  df-meet 18406  df-lat 18489

This theorem is referenced by:  latmlem1  18526  latledi  18534  mod1ile  18550  oldmm1  39198  olm01  39217  cmtcomlemN  39229  cmtbr4N  39236  meetat  39277  cvrexchlem  39401  cvrat4  39425  2llnmj  39542  2lplnmj  39604  dalem25  39680  dalem54  39708  dalem57  39711  cdlema1N  39773  cdlemb  39776  llnexchb2lem  39850  llnexch2N  39852  dalawlem1  39853  dalawlem3  39855  pl42lem1N  39961  lhpelim  40019  lhpat3  40028  4atexlemunv  40048  4atexlemtlw  40049  4atexlemnclw  40052  4atexlemex2  40053  lautm  40076  trlle  40166  cdlemc2  40174  cdlemc5  40177  cdlemd2  40181  cdleme0b  40194  cdleme0c  40195  cdleme0fN  40200  cdleme01N  40203  cdleme0ex1N  40205  cdleme2  40210  cdleme3b  40211  cdleme3c  40212  cdleme3g  40216  cdleme3h  40217  cdleme7aa  40224  cdleme7c  40227  cdleme7d  40228  cdleme7e  40229  cdleme7ga  40230  cdleme11fN  40246  cdleme11k  40250  cdleme15d  40259  cdleme16f  40265  cdlemednpq  40281  cdleme19c  40287  cdleme20aN  40291  cdleme20c  40293  cdleme20j  40300  cdleme21c  40309  cdleme21ct  40311  cdleme22cN  40324  cdleme22f  40328  cdleme23a  40331  cdleme28a  40352  cdleme35d  40434  cdleme35f  40436  cdlemeg46frv  40507  cdlemeg46rgv  40510  cdlemeg46req  40511  cdlemg2fv2  40582  cdlemg2m  40586  cdlemg4  40599  cdlemg10bALTN  40618  cdlemg31b  40680  trlcolem  40708  cdlemk14  40836  dia2dimlem1  41046  docaclN  41106  doca2N  41108  djajN  41119  dihjustlem  41198  dihord1  41200  dihord2a  41201  dihord2b  41202  dihord2cN  41203  dihord11b  41204  dihord11c  41206  dihord2pre  41207  dihlsscpre  41216  dihvalcq2  41229  dihopelvalcpre  41230  dihord6apre  41238  dihord5b  41241  dihord5apre  41244  dihmeetlem1N  41272  dihglblem5apreN  41273  dihglblem3N  41277  dihmeetbclemN  41286  dihmeetlem4preN  41288  dihmeetlem7N  41292  dihmeetlem9N  41297  dihjatcclem4  41403