Theorem latmle2 18431

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 2730	. . . 4 ⊢ (join‘𝐾) = (join‘𝐾)
8	1, 7, 3, 4, 5, 6	latcl2 18402	. . 3 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (⟨𝑋, 𝑌⟩ ∈ dom (join‘𝐾) ∧ ⟨𝑋, 𝑌⟩ ∈ dom ∧ ))
9	8	simprd 495	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ⟨𝑋, 𝑌⟩ ∈ dom ∧ )
10	1, 2, 3, 4, 5, 6, 9	lemeet2 18365	1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ≤ 𝑌)

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ⟨cop 4598   class class class wbr 5110  dom cdm 5641  ‘cfv 6514  (class class class)co 7390  Basecbs 17186  lecple 17234  joincjn 18279  meetcmee 18280  Latclat 18397

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 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-glb 18313  df-meet 18315  df-lat 18398

This theorem is referenced by:  latmlem1  18435  latledi  18443  mod1ile  18459  oldmm1  39217  olm01  39236  cmtcomlemN  39248  cmtbr4N  39255  meetat  39296  cvrexchlem  39420  cvrat4  39444  2llnmj  39561  2lplnmj  39623  dalem25  39699  dalem54  39727  dalem57  39730  cdlema1N  39792  cdlemb  39795  llnexchb2lem  39869  llnexch2N  39871  dalawlem1  39872  dalawlem3  39874  pl42lem1N  39980  lhpelim  40038  lhpat3  40047  4atexlemunv  40067  4atexlemtlw  40068  4atexlemnclw  40071  4atexlemex2  40072  lautm  40095  trlle  40185  cdlemc2  40193  cdlemc5  40196  cdlemd2  40200  cdleme0b  40213  cdleme0c  40214  cdleme0fN  40219  cdleme01N  40222  cdleme0ex1N  40224  cdleme2  40229  cdleme3b  40230  cdleme3c  40231  cdleme3g  40235  cdleme3h  40236  cdleme7aa  40243  cdleme7c  40246  cdleme7d  40247  cdleme7e  40248  cdleme7ga  40249  cdleme11fN  40265  cdleme11k  40269  cdleme15d  40278  cdleme16f  40284  cdlemednpq  40300  cdleme19c  40306  cdleme20aN  40310  cdleme20c  40312  cdleme20j  40319  cdleme21c  40328  cdleme21ct  40330  cdleme22cN  40343  cdleme22f  40347  cdleme23a  40350  cdleme28a  40371  cdleme35d  40453  cdleme35f  40455  cdlemeg46frv  40526  cdlemeg46rgv  40529  cdlemeg46req  40530  cdlemg2fv2  40601  cdlemg2m  40605  cdlemg4  40618  cdlemg10bALTN  40637  cdlemg31b  40699  trlcolem  40727  cdlemk14  40855  dia2dimlem1  41065  docaclN  41125  doca2N  41127  djajN  41138  dihjustlem  41217  dihord1  41219  dihord2a  41220  dihord2b  41221  dihord2cN  41222  dihord11b  41223  dihord11c  41225  dihord2pre  41226  dihlsscpre  41235  dihvalcq2  41248  dihopelvalcpre  41249  dihord6apre  41257  dihord5b  41260  dihord5apre  41263  dihmeetlem1N  41291  dihglblem5apreN  41292  dihglblem3N  41296  dihmeetbclemN  41305  dihmeetlem4preN  41307  dihmeetlem7N  41311  dihmeetlem9N  41316  dihjatcclem4  41422