Theorem latmle2 18371

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 1136	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ Lat)
5		simp2 1137	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∈ 𝐵)
6		simp3 1138	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝐵)
7		eqid 2729	. . . 4 ⊢ (join‘𝐾) = (join‘𝐾)
8	1, 7, 3, 4, 5, 6	latcl2 18342	. . 3 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (⟨𝑋, 𝑌⟩ ∈ dom (join‘𝐾) ∧ ⟨𝑋, 𝑌⟩ ∈ dom ∧ ))
9	8	simprd 495	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ⟨𝑋, 𝑌⟩ ∈ dom ∧ )
10	1, 2, 3, 4, 5, 6, 9	lemeet2 18303	1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ≤ 𝑌)

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ⟨cop 4583   class class class wbr 5092  dom cdm 5619  ‘cfv 6482  (class class class)co 7349  Basecbs 17120  lecple 17168  joincjn 18217  meetcmee 18218  Latclat 18337

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5218  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rmo 3343  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-riota 7306  df-ov 7352  df-oprab 7353  df-glb 18251  df-meet 18253  df-lat 18338

This theorem is referenced by:  latmlem1  18375  latledi  18383  mod1ile  18399  oldmm1  39196  olm01  39215  cmtcomlemN  39227  cmtbr4N  39234  meetat  39275  cvrexchlem  39398  cvrat4  39422  2llnmj  39539  2lplnmj  39601  dalem25  39677  dalem54  39705  dalem57  39708  cdlema1N  39770  cdlemb  39773  llnexchb2lem  39847  llnexch2N  39849  dalawlem1  39850  dalawlem3  39852  pl42lem1N  39958  lhpelim  40016  lhpat3  40025  4atexlemunv  40045  4atexlemtlw  40046  4atexlemnclw  40049  4atexlemex2  40050  lautm  40073  trlle  40163  cdlemc2  40171  cdlemc5  40174  cdlemd2  40178  cdleme0b  40191  cdleme0c  40192  cdleme0fN  40197  cdleme01N  40200  cdleme0ex1N  40202  cdleme2  40207  cdleme3b  40208  cdleme3c  40209  cdleme3g  40213  cdleme3h  40214  cdleme7aa  40221  cdleme7c  40224  cdleme7d  40225  cdleme7e  40226  cdleme7ga  40227  cdleme11fN  40243  cdleme11k  40247  cdleme15d  40256  cdleme16f  40262  cdlemednpq  40278  cdleme19c  40284  cdleme20aN  40288  cdleme20c  40290  cdleme20j  40297  cdleme21c  40306  cdleme21ct  40308  cdleme22cN  40321  cdleme22f  40325  cdleme23a  40328  cdleme28a  40349  cdleme35d  40431  cdleme35f  40433  cdlemeg46frv  40504  cdlemeg46rgv  40507  cdlemeg46req  40508  cdlemg2fv2  40579  cdlemg2m  40583  cdlemg4  40596  cdlemg10bALTN  40615  cdlemg31b  40677  trlcolem  40705  cdlemk14  40833  dia2dimlem1  41043  docaclN  41103  doca2N  41105  djajN  41116  dihjustlem  41195  dihord1  41197  dihord2a  41198  dihord2b  41199  dihord2cN  41200  dihord11b  41201  dihord11c  41203  dihord2pre  41204  dihlsscpre  41213  dihvalcq2  41226  dihopelvalcpre  41227  dihord6apre  41235  dihord5b  41238  dihord5apre  41241  dihmeetlem1N  41269  dihglblem5apreN  41270  dihglblem3N  41274  dihmeetbclemN  41283  dihmeetlem4preN  41285  dihmeetlem7N  41289  dihmeetlem9N  41294  dihjatcclem4  41400