Theorem latmle2 18400

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ⟨cop 4591   class class class wbr 5102  dom cdm 5631  ‘cfv 6499  (class class class)co 7369  Basecbs 17155  lecple 17203  joincjn 18248  meetcmee 18249  Latclat 18366

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 5229  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691

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 3351  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-riota 7326  df-ov 7372  df-oprab 7373  df-glb 18282  df-meet 18284  df-lat 18367

This theorem is referenced by:  latmlem1  18404  latledi  18412  mod1ile  18428  oldmm1  39183  olm01  39202  cmtcomlemN  39214  cmtbr4N  39221  meetat  39262  cvrexchlem  39386  cvrat4  39410  2llnmj  39527  2lplnmj  39589  dalem25  39665  dalem54  39693  dalem57  39696  cdlema1N  39758  cdlemb  39761  llnexchb2lem  39835  llnexch2N  39837  dalawlem1  39838  dalawlem3  39840  pl42lem1N  39946  lhpelim  40004  lhpat3  40013  4atexlemunv  40033  4atexlemtlw  40034  4atexlemnclw  40037  4atexlemex2  40038  lautm  40061  trlle  40151  cdlemc2  40159  cdlemc5  40162  cdlemd2  40166  cdleme0b  40179  cdleme0c  40180  cdleme0fN  40185  cdleme01N  40188  cdleme0ex1N  40190  cdleme2  40195  cdleme3b  40196  cdleme3c  40197  cdleme3g  40201  cdleme3h  40202  cdleme7aa  40209  cdleme7c  40212  cdleme7d  40213  cdleme7e  40214  cdleme7ga  40215  cdleme11fN  40231  cdleme11k  40235  cdleme15d  40244  cdleme16f  40250  cdlemednpq  40266  cdleme19c  40272  cdleme20aN  40276  cdleme20c  40278  cdleme20j  40285  cdleme21c  40294  cdleme21ct  40296  cdleme22cN  40309  cdleme22f  40313  cdleme23a  40316  cdleme28a  40337  cdleme35d  40419  cdleme35f  40421  cdlemeg46frv  40492  cdlemeg46rgv  40495  cdlemeg46req  40496  cdlemg2fv2  40567  cdlemg2m  40571  cdlemg4  40584  cdlemg10bALTN  40603  cdlemg31b  40665  trlcolem  40693  cdlemk14  40821  dia2dimlem1  41031  docaclN  41091  doca2N  41093  djajN  41104  dihjustlem  41183  dihord1  41185  dihord2a  41186  dihord2b  41187  dihord2cN  41188  dihord11b  41189  dihord11c  41191  dihord2pre  41192  dihlsscpre  41201  dihvalcq2  41214  dihopelvalcpre  41215  dihord6apre  41223  dihord5b  41226  dihord5apre  41229  dihmeetlem1N  41257  dihglblem5apreN  41258  dihglblem3N  41262  dihmeetbclemN  41271  dihmeetlem4preN  41273  dihmeetlem7N  41277  dihmeetlem9N  41282  dihjatcclem4  41388