Theorem latlem12 18517

Description: An element is less than or equal to a meet iff the element is less than or equal to each argument of the meet. (Contributed by NM, 21-Oct-2011.)

Hypotheses

Ref	Expression
latmle.b	⊢ 𝐵 = (Base‘𝐾)
latmle.l	⊢ ≤ = (le‘𝐾)
latmle.m	⊢ ∧ = (meet‘𝐾)

Assertion

Ref	Expression
latlem12	⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑋 ≤ 𝑍) ↔ 𝑋 ≤ (𝑌 ∧ 𝑍)))

Proof of Theorem latlem12

Step	Hyp	Ref	Expression
1		latmle.b	. 2 ⊢ 𝐵 = (Base‘𝐾)
2		latmle.l	. 2 ⊢ ≤ = (le‘𝐾)
3		latmle.m	. 2 ⊢ ∧ = (meet‘𝐾)
4		latpos 18489	. . 3 ⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset)
5	4	adantr 485	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Poset)
6		simpr2 1214	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌 ∈ 𝐵)
7		simpr3 1215	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍 ∈ 𝐵)
8		simpr1 1213	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑋 ∈ 𝐵)
9		eqid 2763	. . . 4 ⊢ (join‘𝐾) = (join‘𝐾)
10		simpl 487	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Lat)
11	1, 9, 3, 10, 6, 7	latcl2 18487	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (⟨𝑌, 𝑍⟩ ∈ dom (join‘𝐾) ∧ ⟨𝑌, 𝑍⟩ ∈ dom ∧ ))
12	11	simprd 500	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ⟨𝑌, 𝑍⟩ ∈ dom ∧ )
13	1, 2, 3, 5, 6, 7, 8, 12	meetle 18449	1 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑋 ≤ 𝑍) ↔ 𝑋 ≤ (𝑌 ∧ 𝑍)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1103   = wceq 1570   ∈ wcel 2143  ⟨cop 4595   class class class wbr 5109  dom cdm 5661  ‘cfv 6536  (class class class)co 7410  Basecbs 17264  lecple 17312  Posetcpo 18358  joincjn 18362  meetcmee 18363  Latclat 18482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5238  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-poset 18364  df-glb 18396  df-meet 18398  df-lat 18483

This theorem is referenced by:  latleeqm1  18518  latmlem1  18520  latmidm  18525  latledi  18528  mod1ile  18544  oldmm1  40011  olm01  40030  cmtbr4N  40049  atnle  40111  atlatmstc  40113  hlrelat2  40197  cvrval5  40209  cvrexchlem  40213  2atjm  40239  atbtwn  40240  ps-2b  40276  2atm  40321  2llnm4  40364  2llnmeqat  40365  dalemcea  40454  dalem21  40488  dalem54  40520  dalem55  40521  dalem57  40523  2atm2atN  40579  2llnma1b  40580  cdlemblem  40587  dalawlem2  40666  dalawlem3  40667  dalawlem6  40670  dalawlem11  40675  dalawlem12  40676  lhpocnle  40810  lhpmcvr4N  40820  lhpat3  40840  4atexlemcnd  40866  lautm  40888  trlval3  40981  cdlemc5  40989  cdleme3  41031  cdleme7ga  41042  cdleme7  41043  cdleme11k  41062  cdleme16e  41076  cdleme16f  41077  cdlemednpq  41093  cdleme22aa  41133  cdleme22b  41135  cdleme22cN  41136  cdleme23c  41145  cdlemeg46req  41323  cdlemf2  41356  cdlemg10c  41433  cdlemg12f  41442  cdlemg17dALTN  41458  cdlemg19a  41477  cdlemg27b  41490  cdlemi  41614  cdlemk15  41649  cdlemk50  41746  dia2dimlem1  41858  dihopelvalcpre  42042  dihord5b  42053  dihmeetlem1N  42084  dihglblem5apreN  42085  dihglblem2N  42088  dihmeetlem3N  42099