Theorem latmle2 18422

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ⟨cop 4574   class class class wbr 5086  dom cdm 5624  ‘cfv 6492  (class class class)co 7360  Basecbs 17170  lecple 17218  joincjn 18268  meetcmee 18269  Latclat 18388

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7317  df-ov 7363  df-oprab 7364  df-glb 18302  df-meet 18304  df-lat 18389

This theorem is referenced by:  latmlem1  18426  latledi  18434  mod1ile  18450  oldmm1  39677  olm01  39696  cmtcomlemN  39708  cmtbr4N  39715  meetat  39756  cvrexchlem  39879  cvrat4  39903  2llnmj  40020  2lplnmj  40082  dalem25  40158  dalem54  40186  dalem57  40189  cdlema1N  40251  cdlemb  40254  llnexchb2lem  40328  llnexch2N  40330  dalawlem1  40331  dalawlem3  40333  pl42lem1N  40439  lhpelim  40497  lhpat3  40506  4atexlemunv  40526  4atexlemtlw  40527  4atexlemnclw  40530  4atexlemex2  40531  lautm  40554  trlle  40644  cdlemc2  40652  cdlemc5  40655  cdlemd2  40659  cdleme0b  40672  cdleme0c  40673  cdleme0fN  40678  cdleme01N  40681  cdleme0ex1N  40683  cdleme2  40688  cdleme3b  40689  cdleme3c  40690  cdleme3g  40694  cdleme3h  40695  cdleme7aa  40702  cdleme7c  40705  cdleme7d  40706  cdleme7e  40707  cdleme7ga  40708  cdleme11fN  40724  cdleme11k  40728  cdleme15d  40737  cdleme16f  40743  cdlemednpq  40759  cdleme19c  40765  cdleme20aN  40769  cdleme20c  40771  cdleme20j  40778  cdleme21c  40787  cdleme21ct  40789  cdleme22cN  40802  cdleme22f  40806  cdleme23a  40809  cdleme28a  40830  cdleme35d  40912  cdleme35f  40914  cdlemeg46frv  40985  cdlemeg46rgv  40988  cdlemeg46req  40989  cdlemg2fv2  41060  cdlemg2m  41064  cdlemg4  41077  cdlemg10bALTN  41096  cdlemg31b  41158  trlcolem  41186  cdlemk14  41314  dia2dimlem1  41524  docaclN  41584  doca2N  41586  djajN  41597  dihjustlem  41676  dihord1  41678  dihord2a  41679  dihord2b  41680  dihord2cN  41681  dihord11b  41682  dihord11c  41684  dihord2pre  41685  dihlsscpre  41694  dihvalcq2  41707  dihopelvalcpre  41708  dihord6apre  41716  dihord5b  41719  dihord5apre  41722  dihmeetlem1N  41750  dihglblem5apreN  41751  dihglblem3N  41755  dihmeetbclemN  41764  dihmeetlem4preN  41766  dihmeetlem7N  41770  dihmeetlem9N  41775  dihjatcclem4  41881