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

Syntax hints:   → wi 4   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119  ⟨cop 4561   class class class wbr 5072  dom cdm 5618  ‘cfv 6485  (class class class)co 7356  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 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-rep 5199  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rmo 3344  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-oprab 7360  df-glb 18302  df-meet 18304  df-lat 18389

This theorem is referenced by:  latmlem1  18426  latledi  18434  mod1ile  18450  oldmm1  39709  olm01  39728  cmtcomlemN  39740  cmtbr4N  39747  meetat  39788  cvrexchlem  39911  cvrat4  39935  2llnmj  40052  2lplnmj  40114  dalem25  40190  dalem54  40218  dalem57  40221  cdlema1N  40283  cdlemb  40286  llnexchb2lem  40360  llnexch2N  40362  dalawlem1  40363  dalawlem3  40365  pl42lem1N  40471  lhpelim  40529  lhpat3  40538  4atexlemunv  40558  4atexlemtlw  40559  4atexlemnclw  40562  4atexlemex2  40563  lautm  40586  trlle  40676  cdlemc2  40684  cdlemc5  40687  cdlemd2  40691  cdleme0b  40704  cdleme0c  40705  cdleme0fN  40710  cdleme01N  40713  cdleme0ex1N  40715  cdleme2  40720  cdleme3b  40721  cdleme3c  40722  cdleme3g  40726  cdleme3h  40727  cdleme7aa  40734  cdleme7c  40737  cdleme7d  40738  cdleme7e  40739  cdleme7ga  40740  cdleme11fN  40756  cdleme11k  40760  cdleme15d  40769  cdleme16f  40775  cdlemednpq  40791  cdleme19c  40797  cdleme20aN  40801  cdleme20c  40803  cdleme20j  40810  cdleme21c  40819  cdleme21ct  40821  cdleme22cN  40834  cdleme22f  40838  cdleme23a  40841  cdleme28a  40862  cdleme35d  40944  cdleme35f  40946  cdlemeg46frv  41017  cdlemeg46rgv  41020  cdlemeg46req  41021  cdlemg2fv2  41092  cdlemg2m  41096  cdlemg4  41109  cdlemg10bALTN  41128  cdlemg31b  41190  trlcolem  41218  cdlemk14  41346  dia2dimlem1  41556  docaclN  41616  doca2N  41618  djajN  41629  dihjustlem  41708  dihord1  41710  dihord2a  41711  dihord2b  41712  dihord2cN  41713  dihord11b  41714  dihord11c  41716  dihord2pre  41717  dihlsscpre  41726  dihvalcq2  41739  dihopelvalcpre  41740  dihord6apre  41748  dihord5b  41751  dihord5apre  41754  dihmeetlem1N  41782  dihglblem5apreN  41783  dihglblem3N  41787  dihmeetbclemN  41796  dihmeetlem4preN  41798  dihmeetlem7N  41802  dihmeetlem9N  41807  dihjatcclem4  41913