Theorem latjle12 18177

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 29880 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 18165	. . 3 ⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset)
5	4	adantr 481	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Poset)
6		simpr1 1193	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑋 ∈ 𝐵)
7		simpr2 1194	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌 ∈ 𝐵)
8		simpr3 1195	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍 ∈ 𝐵)
9		eqid 2739	. . . 4 ⊢ (meet‘𝐾) = (meet‘𝐾)
10		simpl 483	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Lat)
11	1, 3, 9, 10, 6, 7	latcl2 18163	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (⟨𝑋, 𝑌⟩ ∈ dom ∨ ∧ ⟨𝑋, 𝑌⟩ ∈ dom (meet‘𝐾)))
12	11	simpld 495	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ⟨𝑋, 𝑌⟩ ∈ dom ∨ )
13	1, 2, 3, 5, 6, 7, 8, 12	joinle 18113	1 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑍 ∧ 𝑌 ≤ 𝑍) ↔ (𝑋 ∨ 𝑌) ≤ 𝑍))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107  ⟨cop 4568   class class class wbr 5075  dom cdm 5590  ‘cfv 6437  (class class class)co 7284  Basecbs 16921  lecple 16978  Posetcpo 18034  joincjn 18038  meetcmee 18039  Latclat 18158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-rep 5210  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-riota 7241  df-ov 7287  df-oprab 7288  df-poset 18040  df-lub 18073  df-join 18075  df-lat 18159

This theorem is referenced by:  latleeqj1  18178  latjlej1  18180  latjidm  18189  latledi  18204  latjass  18210  mod1ile  18220  lubun  18242  oldmm1  37238  olj01  37246  cvlexchb1  37351  cvlcvr1  37360  hlrelat  37423  hlrelat2  37424  exatleN  37425  hlrelat3  37433  cvrexchlem  37440  cvratlem  37442  cvrat  37443  atlelt  37459  ps-1  37498  hlatexch3N  37501  hlatexch4  37502  3atlem1  37504  3atlem2  37505  lplnexllnN  37585  2llnjaN  37587  4atlem3  37617  4atlem10  37627  4atlem11b  37629  4atlem11  37630  4atlem12b  37632  4atlem12  37633  2lplnja  37640  dalem1  37680  dalem3  37685  dalem8  37691  dalem16  37700  dalem17  37701  dalem21  37715  dalem25  37719  dalem39  37732  dalem54  37747  dalem60  37753  linepsubN  37773  pmapsub  37789  lneq2at  37799  2llnma3r  37809  cdlema1N  37812  cdlemblem  37814  paddasslem5  37845  paddasslem12  37852  paddasslem13  37853  llnexchb2  37890  dalawlem3  37894  dalawlem5  37896  dalawlem8  37899  dalawlem11  37902  dalawlem12  37903  lhp2lt  38022  lhpexle2lem  38030  lhpexle3lem  38032  4atexlemtlw  38088  4atexlemnclw  38091  lautj  38114  cdlemd3  38221  cdleme3g  38255  cdleme3h  38256  cdleme7d  38267  cdleme11c  38282  cdleme15d  38298  cdleme17b  38308  cdleme19a  38324  cdleme20j  38339  cdleme21c  38348  cdleme22b  38362  cdleme22d  38364  cdleme28a  38391  cdleme35a  38469  cdleme35fnpq  38470  cdleme35b  38471  cdleme35f  38475  cdleme42c  38493  cdleme42i  38504  cdlemf1  38582  cdlemg4c  38633  cdlemg6c  38641  cdlemg8b  38649  cdlemg10  38662  cdlemg11b  38663  cdlemg13a  38672  cdlemg17a  38682  cdlemg18b  38700  cdlemg27a  38713  cdlemg33b0  38722  cdlemg35  38734  cdlemg42  38750  cdlemg46  38756  trljco  38761  tendopltp  38801  cdlemk3  38854  cdlemk10  38864  cdlemk1u  38880  cdlemk39  38937  dialss  39067  dia2dimlem1  39085  dia2dimlem10  39094  dia2dimlem12  39096  cdlemm10N  39139  djajN  39158  diblss  39191  cdlemn2  39216  dihord2pre2  39247  dib2dim  39264  dih2dimb  39265  dih2dimbALTN  39266  dihmeetlem6  39330  dihjatcclem1  39439