Theorem latmle2 17278

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 1131	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ Lat)
5		simp2 1132	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∈ 𝐵)
6		simp3 1133	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝐵)
7		eqid 2760	. . . 4 ⊢ (join‘𝐾) = (join‘𝐾)
8	1, 7, 3, 4, 5, 6	latcl2 17249	. . 3 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (⟨𝑋, 𝑌⟩ ∈ dom (join‘𝐾) ∧ ⟨𝑋, 𝑌⟩ ∈ dom ∧ ))
9	8	simprd 482	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ⟨𝑋, 𝑌⟩ ∈ dom ∧ )
10	1, 2, 3, 4, 5, 6, 9	lemeet2 17228	1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ≤ 𝑌)

Syntax hints:   → wi 4   ∧ w3a 1072   = wceq 1632   ∈ wcel 2139  ⟨cop 4327   class class class wbr 4804  dom cdm 5266  ‘cfv 6049  (class class class)co 6813  Basecbs 16059  lecple 16150  joincjn 17145  meetcmee 17146  Latclat 17246

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-reu 3057  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6774  df-ov 6816  df-oprab 6817  df-glb 17176  df-meet 17178  df-lat 17247

This theorem is referenced by:  latmlem1  17282  latledi  17290  mod1ile  17306  oldmm1  35007  olm01  35026  cmtcomlemN  35038  cmtbr4N  35045  meetat  35086  cvrexchlem  35208  cvrat4  35232  2llnmj  35349  2lplnmj  35411  dalem25  35487  dalem54  35515  dalem57  35518  cdlema1N  35580  cdlemb  35583  llnexchb2lem  35657  llnexch2N  35659  dalawlem1  35660  dalawlem3  35662  pl42lem1N  35768  lhpelim  35826  lhpat3  35835  4atexlemunv  35855  4atexlemtlw  35856  4atexlemnclw  35859  4atexlemex2  35860  lautm  35883  trlle  35974  cdlemc2  35982  cdlemc5  35985  cdlemd2  35989  cdleme0b  36002  cdleme0c  36003  cdleme0fN  36008  cdleme01N  36011  cdleme0ex1N  36013  cdleme2  36018  cdleme3b  36019  cdleme3c  36020  cdleme3g  36024  cdleme3h  36025  cdleme7aa  36032  cdleme7c  36035  cdleme7d  36036  cdleme7e  36037  cdleme7ga  36038  cdleme11fN  36054  cdleme11k  36058  cdleme15d  36067  cdleme16f  36073  cdlemednpq  36089  cdleme19c  36095  cdleme20aN  36099  cdleme20c  36101  cdleme20j  36108  cdleme21c  36117  cdleme21ct  36119  cdleme22cN  36132  cdleme22f  36136  cdleme23a  36139  cdleme28a  36160  cdleme35d  36242  cdleme35f  36244  cdlemeg46frv  36315  cdlemeg46rgv  36318  cdlemeg46req  36319  cdlemg2fv2  36390  cdlemg2m  36394  cdlemg4  36407  cdlemg10bALTN  36426  cdlemg31b  36488  trlcolem  36516  cdlemk14  36644  dia2dimlem1  36855  docaclN  36915  doca2N  36917  djajN  36928  dihjustlem  37007  dihord1  37009  dihord2a  37010  dihord2b  37011  dihord2cN  37012  dihord11b  37013  dihord11c  37015  dihord2pre  37016  dihlsscpre  37025  dihvalcq2  37038  dihopelvalcpre  37039  dihord6apre  37047  dihord5b  37050  dihord5apre  37053  dihmeetlem1N  37081  dihglblem5apreN  37082  dihglblem3N  37086  dihmeetbclemN  37095  dihmeetlem4preN  37097  dihmeetlem7N  37101  dihmeetlem9N  37106  dihjatcclem4  37212