Theorem latmle2 18424

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ⟨cop 4595   class class class wbr 5107  dom cdm 5638  ‘cfv 6511  (class class class)co 7387  Basecbs 17179  lecple 17227  joincjn 18272  meetcmee 18273  Latclat 18390

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 5234  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711

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 3354  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-glb 18306  df-meet 18308  df-lat 18391

This theorem is referenced by:  latmlem1  18428  latledi  18436  mod1ile  18452  oldmm1  39210  olm01  39229  cmtcomlemN  39241  cmtbr4N  39248  meetat  39289  cvrexchlem  39413  cvrat4  39437  2llnmj  39554  2lplnmj  39616  dalem25  39692  dalem54  39720  dalem57  39723  cdlema1N  39785  cdlemb  39788  llnexchb2lem  39862  llnexch2N  39864  dalawlem1  39865  dalawlem3  39867  pl42lem1N  39973  lhpelim  40031  lhpat3  40040  4atexlemunv  40060  4atexlemtlw  40061  4atexlemnclw  40064  4atexlemex2  40065  lautm  40088  trlle  40178  cdlemc2  40186  cdlemc5  40189  cdlemd2  40193  cdleme0b  40206  cdleme0c  40207  cdleme0fN  40212  cdleme01N  40215  cdleme0ex1N  40217  cdleme2  40222  cdleme3b  40223  cdleme3c  40224  cdleme3g  40228  cdleme3h  40229  cdleme7aa  40236  cdleme7c  40239  cdleme7d  40240  cdleme7e  40241  cdleme7ga  40242  cdleme11fN  40258  cdleme11k  40262  cdleme15d  40271  cdleme16f  40277  cdlemednpq  40293  cdleme19c  40299  cdleme20aN  40303  cdleme20c  40305  cdleme20j  40312  cdleme21c  40321  cdleme21ct  40323  cdleme22cN  40336  cdleme22f  40340  cdleme23a  40343  cdleme28a  40364  cdleme35d  40446  cdleme35f  40448  cdlemeg46frv  40519  cdlemeg46rgv  40522  cdlemeg46req  40523  cdlemg2fv2  40594  cdlemg2m  40598  cdlemg4  40611  cdlemg10bALTN  40630  cdlemg31b  40692  trlcolem  40720  cdlemk14  40848  dia2dimlem1  41058  docaclN  41118  doca2N  41120  djajN  41131  dihjustlem  41210  dihord1  41212  dihord2a  41213  dihord2b  41214  dihord2cN  41215  dihord11b  41216  dihord11c  41218  dihord2pre  41219  dihlsscpre  41228  dihvalcq2  41241  dihopelvalcpre  41242  dihord6apre  41250  dihord5b  41253  dihord5apre  41256  dihmeetlem1N  41284  dihglblem5apreN  41285  dihglblem3N  41289  dihmeetbclemN  41298  dihmeetlem4preN  41300  dihmeetlem7N  41304  dihmeetlem9N  41309  dihjatcclem4  41415