Theorem latmcl 18406

Description: Closure of meet operation in a lattice. (incom 4149 analog.) (Contributed by NM, 14-Sep-2011.)

Hypotheses

Ref	Expression
latmcl.b	⊢ 𝐵 = (Base‘𝐾)
latmcl.m	⊢ ∧ = (meet‘𝐾)

Assertion

Ref	Expression
latmcl	⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ∈ 𝐵)

Proof of Theorem latmcl

Step	Hyp	Ref	Expression
1		latmcl.b	. . 3 ⊢ 𝐵 = (Base‘𝐾)
2		eqid 2736	. . 3 ⊢ (join‘𝐾) = (join‘𝐾)
3		latmcl.m	. . 3 ⊢ ∧ = (meet‘𝐾)
4	1, 2, 3	latlem 18403	. 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋(join‘𝐾)𝑌) ∈ 𝐵 ∧ (𝑋 ∧ 𝑌) ∈ 𝐵))
5	4	simprd 495	1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∧ 𝑌) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ‘cfv 6498  (class class class)co 7367  Basecbs 17179  joincjn 18277  meetcmee 18278  Latclat 18397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rmo 3342  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  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 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-riota 7324  df-ov 7370  df-oprab 7371  df-lub 18310  df-glb 18311  df-join 18312  df-meet 18313  df-lat 18398

This theorem is referenced by:  latleeqm1  18433  latmlem1  18435  latmlem12  18437  latnlemlt  18438  latmidm  18440  latabs1  18441  latledi  18443  latmlej11  18444  mod1ile  18459  mod2ile  18460  latdisdlem  18462  oldmm1  39663  oldmj1  39667  latmrot  39678  latm4  39679  olm01  39682  omllaw4  39692  cmtcomlemN  39694  cmt2N  39696  cmtbr2N  39699  cmtbr3N  39700  cmtbr4N  39701  lecmtN  39702  omlfh1N  39704  omlfh3N  39705  meetat  39742  atnle  39763  atlatmstc  39765  hlrelat2  39849  cvrval5  39861  cvrexchlem  39865  cvrexch  39866  cvrat3  39888  cvrat4  39889  ps-2b  39928  2llnmat  39970  2atm  39973  llnmlplnN  39985  2lplnmN  40005  2llnmj  40006  2llnm2N  40014  2llnm4  40016  2lplnm2N  40067  2lplnmj  40068  dalemcea  40106  dalem16  40125  dalem21  40140  dalem54  40172  dalem55  40173  2lnat  40230  2atm2atN  40231  cdlema1N  40237  hlmod1i  40302  atmod1i1m  40304  atmod2i1  40307  atmod2i2  40308  llnmod2i2  40309  atmod4i1  40312  atmod4i2  40313  llnexchb2lem  40314  dalawlem1  40317  dalawlem2  40318  dalawlem3  40319  dalawlem4  40320  dalawlem5  40321  dalawlem6  40322  dalawlem7  40323  dalawlem8  40324  dalawlem9  40325  dalawlem11  40327  dalawlem12  40328  pmapj2N  40375  psubclinN  40394  poml4N  40399  pl42lem1N  40425  pl42lem2N  40426  pl42N  40429  lhpmcvr3  40471  lhpmcvr4N  40472  lhpmcvr5N  40473  lhpmcvr6N  40474  lhpelim  40483  lhpmod2i2  40484  lhpmod6i1  40485  lhprelat3N  40486  lautm  40540  trlval2  40609  trlcl  40610  trlval3  40633  cdlemc1  40637  cdlemc2  40638  cdlemc4  40640  cdlemc5  40641  cdlemc6  40642  cdlemd2  40645  cdleme0aa  40656  cdleme1b  40672  cdleme1  40673  cdleme2  40674  cdleme3b  40675  cdleme3h  40681  cdleme4a  40685  cdleme5  40686  cdleme7e  40693  cdleme7ga  40694  cdleme9b  40698  cdleme11g  40711  cdleme15d  40723  cdleme15  40724  cdleme16b  40725  cdleme16e  40728  cdleme16f  40729  cdleme22gb  40740  cdlemedb  40743  cdleme20j  40764  cdleme22cN  40788  cdleme22e  40790  cdleme22eALTN  40791  cdleme22f  40792  cdleme23a  40795  cdleme23b  40796  cdleme23c  40797  cdleme28a  40816  cdleme28b  40817  cdleme29ex  40820  cdleme30a  40824  cdlemefr29exN  40848  cdleme32c  40889  cdleme32e  40891  cdleme35b  40896  cdleme35c  40897  cdleme35d  40898  cdleme42c  40918  cdleme42h  40928  cdleme42i  40929  cdleme48bw  40948  cdlemg7fvbwN  41053  cdlemg10bALTN  41082  cdlemg10  41087  cdlemg11b  41088  cdlemg12f  41094  cdlemg12g  41095  cdlemg17a  41107  trlcolem  41172  cdlemkvcl  41288  cdlemk5u  41307  cdlemk37  41360  cdlemk52  41400  dia2dimlem2  41511  docaclN  41570  doca2N  41572  djajN  41583  cdlemn10  41652  dihjustlem  41662  dihord1  41664  dihord2a  41665  dihord2b  41666  dihord2cN  41667  dihord11b  41668  dihord11c  41670  dihord2pre  41671  dihord2pre2  41672  dihlsscpre  41680  dihvalcq2  41693  dihopelvalcpre  41694  dihord6apre  41702  dihord5b  41705  dihord5apre  41708  dihmeetlem1N  41736  dihglblem5apreN  41737  dihglblem2aN  41739  dihglblem2N  41740  dihmeetlem2N  41745  dihglbcpreN  41746  dihmeetbclemN  41750  dihmeetlem3N  41751  dihmeetlem4preN  41752  dihmeetlem6  41755  dihmeetlem7N  41756  dihjatc1  41757  dihjatc2N  41758  dihjatc3  41759  dihmeetlem9N  41761  dihmeetlem16N  41768  dihmeetlem19N  41771  dihmeetcl  41791  dihmeet2  41792  djhlj  41847  dihjatcclem1  41864  dihjatcclem2  41865  dihjatcclem4  41867