Theorem latmle2 18510

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 1137	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ Lat)
5		simp2 1138	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∈ 𝐵)
6		simp3 1139	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝐵)
7		eqid 2737	. . . 4 ⊢ (join‘𝐾) = (join‘𝐾)
8	1, 7, 3, 4, 5, 6	latcl2 18481	. . 3 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (⟨𝑋, 𝑌⟩ ∈ dom (join‘𝐾) ∧ ⟨𝑋, 𝑌⟩ ∈ dom ∧ ))
9	8	simprd 495	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ⟨𝑋, 𝑌⟩ ∈ dom ∧ )
10	1, 2, 3, 4, 5, 6, 9	lemeet2 18444	1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ≤ 𝑌)

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1540   ∈ wcel 2108  ⟨cop 4632   class class class wbr 5143  dom cdm 5685  ‘cfv 6561  (class class class)co 7431  Basecbs 17247  lecple 17304  joincjn 18357  meetcmee 18358  Latclat 18476

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-glb 18392  df-meet 18394  df-lat 18477

This theorem is referenced by:  latmlem1  18514  latledi  18522  mod1ile  18538  oldmm1  39218  olm01  39237  cmtcomlemN  39249  cmtbr4N  39256  meetat  39297  cvrexchlem  39421  cvrat4  39445  2llnmj  39562  2lplnmj  39624  dalem25  39700  dalem54  39728  dalem57  39731  cdlema1N  39793  cdlemb  39796  llnexchb2lem  39870  llnexch2N  39872  dalawlem1  39873  dalawlem3  39875  pl42lem1N  39981  lhpelim  40039  lhpat3  40048  4atexlemunv  40068  4atexlemtlw  40069  4atexlemnclw  40072  4atexlemex2  40073  lautm  40096  trlle  40186  cdlemc2  40194  cdlemc5  40197  cdlemd2  40201  cdleme0b  40214  cdleme0c  40215  cdleme0fN  40220  cdleme01N  40223  cdleme0ex1N  40225  cdleme2  40230  cdleme3b  40231  cdleme3c  40232  cdleme3g  40236  cdleme3h  40237  cdleme7aa  40244  cdleme7c  40247  cdleme7d  40248  cdleme7e  40249  cdleme7ga  40250  cdleme11fN  40266  cdleme11k  40270  cdleme15d  40279  cdleme16f  40285  cdlemednpq  40301  cdleme19c  40307  cdleme20aN  40311  cdleme20c  40313  cdleme20j  40320  cdleme21c  40329  cdleme21ct  40331  cdleme22cN  40344  cdleme22f  40348  cdleme23a  40351  cdleme28a  40372  cdleme35d  40454  cdleme35f  40456  cdlemeg46frv  40527  cdlemeg46rgv  40530  cdlemeg46req  40531  cdlemg2fv2  40602  cdlemg2m  40606  cdlemg4  40619  cdlemg10bALTN  40638  cdlemg31b  40700  trlcolem  40728  cdlemk14  40856  dia2dimlem1  41066  docaclN  41126  doca2N  41128  djajN  41139  dihjustlem  41218  dihord1  41220  dihord2a  41221  dihord2b  41222  dihord2cN  41223  dihord11b  41224  dihord11c  41226  dihord2pre  41227  dihlsscpre  41236  dihvalcq2  41249  dihopelvalcpre  41250  dihord6apre  41258  dihord5b  41261  dihord5apre  41264  dihmeetlem1N  41292  dihglblem5apreN  41293  dihglblem3N  41297  dihmeetbclemN  41306  dihmeetlem4preN  41308  dihmeetlem7N  41312  dihmeetlem9N  41317  dihjatcclem4  41423