Theorem latlem12 18511

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 18483	. . 3 ⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset)
5	4	adantr 480	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Poset)
6		simpr2 1196	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌 ∈ 𝐵)
7		simpr3 1197	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍 ∈ 𝐵)
8		simpr1 1195	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑋 ∈ 𝐵)
9		eqid 2737	. . . 4 ⊢ (join‘𝐾) = (join‘𝐾)
10		simpl 482	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Lat)
11	1, 9, 3, 10, 6, 7	latcl2 18481	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (⟨𝑌, 𝑍⟩ ∈ dom (join‘𝐾) ∧ ⟨𝑌, 𝑍⟩ ∈ dom ∧ ))
12	11	simprd 495	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ⟨𝑌, 𝑍⟩ ∈ dom ∧ )
13	1, 2, 3, 5, 6, 7, 8, 12	meetle 18445	1 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑌 ∧ 𝑋 ≤ 𝑍) ↔ 𝑋 ≤ (𝑌 ∧ 𝑍)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ 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  Posetcpo 18353  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-poset 18359  df-glb 18392  df-meet 18394  df-lat 18477

This theorem is referenced by:  latleeqm1  18512  latmlem1  18514  latmidm  18519  latledi  18522  mod1ile  18538  oldmm1  39218  olm01  39237  cmtbr4N  39256  atnle  39318  atlatmstc  39320  hlrelat2  39405  cvrval5  39417  cvrexchlem  39421  2atjm  39447  atbtwn  39448  ps-2b  39484  2atm  39529  2llnm4  39572  2llnmeqat  39573  dalemcea  39662  dalem21  39696  dalem54  39728  dalem55  39729  dalem57  39731  2atm2atN  39787  2llnma1b  39788  cdlemblem  39795  dalawlem2  39874  dalawlem3  39875  dalawlem6  39878  dalawlem11  39883  dalawlem12  39884  lhpocnle  40018  lhpmcvr4N  40028  lhpat3  40048  4atexlemcnd  40074  lautm  40096  trlval3  40189  cdlemc5  40197  cdleme3  40239  cdleme7ga  40250  cdleme7  40251  cdleme11k  40270  cdleme16e  40284  cdleme16f  40285  cdlemednpq  40301  cdleme22aa  40341  cdleme22b  40343  cdleme22cN  40344  cdleme23c  40353  cdlemeg46req  40531  cdlemf2  40564  cdlemg10c  40641  cdlemg12f  40650  cdlemg17dALTN  40666  cdlemg19a  40685  cdlemg27b  40698  cdlemi  40822  cdlemk15  40857  cdlemk50  40954  dia2dimlem1  41066  dihopelvalcpre  41250  dihord5b  41261  dihmeetlem1N  41292  dihglblem5apreN  41293  dihglblem2N  41296  dihmeetlem3N  41307