Theorem latjle12 18083

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 29772 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 18071	. . 3 ⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset)
5	4	adantr 480	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Poset)
6		simpr1 1192	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑋 ∈ 𝐵)
7		simpr2 1193	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌 ∈ 𝐵)
8		simpr3 1194	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍 ∈ 𝐵)
9		eqid 2738	. . . 4 ⊢ (meet‘𝐾) = (meet‘𝐾)
10		simpl 482	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Lat)
11	1, 3, 9, 10, 6, 7	latcl2 18069	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (⟨𝑋, 𝑌⟩ ∈ dom ∨ ∧ ⟨𝑋, 𝑌⟩ ∈ dom (meet‘𝐾)))
12	11	simpld 494	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ⟨𝑋, 𝑌⟩ ∈ dom ∨ )
13	1, 2, 3, 5, 6, 7, 8, 12	joinle 18019	1 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑍 ∧ 𝑌 ≤ 𝑍) ↔ (𝑋 ∨ 𝑌) ≤ 𝑍))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108  ⟨cop 4564   class class class wbr 5070  dom cdm 5580  ‘cfv 6418  (class class class)co 7255  Basecbs 16840  lecple 16895  Posetcpo 17940  joincjn 17944  meetcmee 17945  Latclat 18064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-poset 17946  df-lub 17979  df-join 17981  df-lat 18065

This theorem is referenced by:  latleeqj1  18084  latjlej1  18086  latjidm  18095  latledi  18110  latjass  18116  mod1ile  18126  lubun  18148  oldmm1  37158  olj01  37166  cvlexchb1  37271  cvlcvr1  37280  hlrelat  37343  hlrelat2  37344  exatleN  37345  hlrelat3  37353  cvrexchlem  37360  cvratlem  37362  cvrat  37363  atlelt  37379  ps-1  37418  hlatexch3N  37421  hlatexch4  37422  3atlem1  37424  3atlem2  37425  lplnexllnN  37505  2llnjaN  37507  4atlem3  37537  4atlem10  37547  4atlem11b  37549  4atlem11  37550  4atlem12b  37552  4atlem12  37553  2lplnja  37560  dalem1  37600  dalem3  37605  dalem8  37611  dalem16  37620  dalem17  37621  dalem21  37635  dalem25  37639  dalem39  37652  dalem54  37667  dalem60  37673  linepsubN  37693  pmapsub  37709  lneq2at  37719  2llnma3r  37729  cdlema1N  37732  cdlemblem  37734  paddasslem5  37765  paddasslem12  37772  paddasslem13  37773  llnexchb2  37810  dalawlem3  37814  dalawlem5  37816  dalawlem8  37819  dalawlem11  37822  dalawlem12  37823  lhp2lt  37942  lhpexle2lem  37950  lhpexle3lem  37952  4atexlemtlw  38008  4atexlemnclw  38011  lautj  38034  cdlemd3  38141  cdleme3g  38175  cdleme3h  38176  cdleme7d  38187  cdleme11c  38202  cdleme15d  38218  cdleme17b  38228  cdleme19a  38244  cdleme20j  38259  cdleme21c  38268  cdleme22b  38282  cdleme22d  38284  cdleme28a  38311  cdleme35a  38389  cdleme35fnpq  38390  cdleme35b  38391  cdleme35f  38395  cdleme42c  38413  cdleme42i  38424  cdlemf1  38502  cdlemg4c  38553  cdlemg6c  38561  cdlemg8b  38569  cdlemg10  38582  cdlemg11b  38583  cdlemg13a  38592  cdlemg17a  38602  cdlemg18b  38620  cdlemg27a  38633  cdlemg33b0  38642  cdlemg35  38654  cdlemg42  38670  cdlemg46  38676  trljco  38681  tendopltp  38721  cdlemk3  38774  cdlemk10  38784  cdlemk1u  38800  cdlemk39  38857  dialss  38987  dia2dimlem1  39005  dia2dimlem10  39014  dia2dimlem12  39016  cdlemm10N  39059  djajN  39078  diblss  39111  cdlemn2  39136  dihord2pre2  39167  dib2dim  39184  dih2dimb  39185  dih2dimbALTN  39186  dihmeetlem6  39250  dihjatcclem1  39359