Theorem latjle12 18409

Description: A join is less than or equal to a third value iff each argument is less than or equal to the third value. (chlub 31438 analog.) (Contributed by NM, 17-Sep-2011.)

Hypotheses

Ref	Expression
latlej.b	⊢ 𝐵 = (Base‘𝐾)
latlej.l	⊢ ≤ = (le‘𝐾)
latlej.j	⊢ ∨ = (join‘𝐾)

Assertion

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

Proof of Theorem latjle12

Step	Hyp	Ref	Expression
1		latlej.b	. 2 ⊢ 𝐵 = (Base‘𝐾)
2		latlej.l	. 2 ⊢ ≤ = (le‘𝐾)
3		latlej.j	. 2 ⊢ ∨ = (join‘𝐾)
4		latpos 18397	. . 3 ⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset)
5	4	adantr 480	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Poset)
6		simpr1 1195	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑋 ∈ 𝐵)
7		simpr2 1196	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌 ∈ 𝐵)
8		simpr3 1197	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍 ∈ 𝐵)
9		eqid 2729	. . . 4 ⊢ (meet‘𝐾) = (meet‘𝐾)
10		simpl 482	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Lat)
11	1, 3, 9, 10, 6, 7	latcl2 18395	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (⟨𝑋, 𝑌⟩ ∈ dom ∨ ∧ ⟨𝑋, 𝑌⟩ ∈ dom (meet‘𝐾)))
12	11	simpld 494	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ⟨𝑋, 𝑌⟩ ∈ dom ∨ )
13	1, 2, 3, 5, 6, 7, 8, 12	joinle 18345	1 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑍 ∧ 𝑌 ≤ 𝑍) ↔ (𝑋 ∨ 𝑌) ≤ 𝑍))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ⟨cop 4595   class class class wbr 5107  dom cdm 5638  ‘cfv 6511  (class class class)co 7387  Basecbs 17179  lecple 17227  Posetcpo 18268  joincjn 18272  meetcmee 18273  Latclat 18390

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 5234  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711

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 3354  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-poset 18274  df-lub 18305  df-join 18307  df-lat 18391

This theorem is referenced by:  latleeqj1  18410  latjlej1  18412  latjidm  18421  latledi  18436  latjass  18442  mod1ile  18452  lubun  18474  oldmm1  39210  olj01  39218  cvlexchb1  39323  cvlcvr1  39332  hlrelat  39396  hlrelat2  39397  exatleN  39398  hlrelat3  39406  cvrexchlem  39413  cvratlem  39415  cvrat  39416  atlelt  39432  ps-1  39471  hlatexch3N  39474  hlatexch4  39475  3atlem1  39477  3atlem2  39478  lplnexllnN  39558  2llnjaN  39560  4atlem3  39590  4atlem10  39600  4atlem11b  39602  4atlem11  39603  4atlem12b  39605  4atlem12  39606  2lplnja  39613  dalem1  39653  dalem3  39658  dalem8  39664  dalem16  39673  dalem17  39674  dalem21  39688  dalem25  39692  dalem39  39705  dalem54  39720  dalem60  39726  linepsubN  39746  pmapsub  39762  lneq2at  39772  2llnma3r  39782  cdlema1N  39785  cdlemblem  39787  paddasslem5  39818  paddasslem12  39825  paddasslem13  39826  llnexchb2  39863  dalawlem3  39867  dalawlem5  39869  dalawlem8  39872  dalawlem11  39875  dalawlem12  39876  lhp2lt  39995  lhpexle2lem  40003  lhpexle3lem  40005  4atexlemtlw  40061  4atexlemnclw  40064  lautj  40087  cdlemd3  40194  cdleme3g  40228  cdleme3h  40229  cdleme7d  40240  cdleme11c  40255  cdleme15d  40271  cdleme17b  40281  cdleme19a  40297  cdleme20j  40312  cdleme21c  40321  cdleme22b  40335  cdleme22d  40337  cdleme28a  40364  cdleme35a  40442  cdleme35fnpq  40443  cdleme35b  40444  cdleme35f  40448  cdleme42c  40466  cdleme42i  40477  cdlemf1  40555  cdlemg4c  40606  cdlemg6c  40614  cdlemg8b  40622  cdlemg10  40635  cdlemg11b  40636  cdlemg13a  40645  cdlemg17a  40655  cdlemg18b  40673  cdlemg27a  40686  cdlemg33b0  40695  cdlemg35  40707  cdlemg42  40723  cdlemg46  40729  trljco  40734  tendopltp  40774  cdlemk3  40827  cdlemk10  40837  cdlemk1u  40853  cdlemk39  40910  dialss  41040  dia2dimlem1  41058  dia2dimlem10  41067  dia2dimlem12  41069  cdlemm10N  41112  djajN  41131  diblss  41164  cdlemn2  41189  dihord2pre2  41220  dib2dim  41237  dih2dimb  41238  dih2dimbALTN  41239  dihmeetlem6  41303  dihjatcclem1  41412