Theorem latjle12 18465

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107  ⟨cop 4612   class class class wbr 5123  dom cdm 5665  ‘cfv 6541  (class class class)co 7413  Basecbs 17230  lecple 17281  Posetcpo 18324  joincjn 18328  meetcmee 18329  Latclat 18446

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-rep 5259  ax-sep 5276  ax-nul 5286  ax-pow 5345  ax-pr 5412  ax-un 7737

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-iun 4973  df-br 5124  df-opab 5186  df-mpt 5206  df-id 5558  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-iota 6494  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7370  df-ov 7416  df-oprab 7417  df-poset 18330  df-lub 18361  df-join 18363  df-lat 18447

This theorem is referenced by:  latleeqj1  18466  latjlej1  18468  latjidm  18477  latledi  18492  latjass  18498  mod1ile  18508  lubun  18530  oldmm1  39193  olj01  39201  cvlexchb1  39306  cvlcvr1  39315  hlrelat  39379  hlrelat2  39380  exatleN  39381  hlrelat3  39389  cvrexchlem  39396  cvratlem  39398  cvrat  39399  atlelt  39415  ps-1  39454  hlatexch3N  39457  hlatexch4  39458  3atlem1  39460  3atlem2  39461  lplnexllnN  39541  2llnjaN  39543  4atlem3  39573  4atlem10  39583  4atlem11b  39585  4atlem11  39586  4atlem12b  39588  4atlem12  39589  2lplnja  39596  dalem1  39636  dalem3  39641  dalem8  39647  dalem16  39656  dalem17  39657  dalem21  39671  dalem25  39675  dalem39  39688  dalem54  39703  dalem60  39709  linepsubN  39729  pmapsub  39745  lneq2at  39755  2llnma3r  39765  cdlema1N  39768  cdlemblem  39770  paddasslem5  39801  paddasslem12  39808  paddasslem13  39809  llnexchb2  39846  dalawlem3  39850  dalawlem5  39852  dalawlem8  39855  dalawlem11  39858  dalawlem12  39859  lhp2lt  39978  lhpexle2lem  39986  lhpexle3lem  39988  4atexlemtlw  40044  4atexlemnclw  40047  lautj  40070  cdlemd3  40177  cdleme3g  40211  cdleme3h  40212  cdleme7d  40223  cdleme11c  40238  cdleme15d  40254  cdleme17b  40264  cdleme19a  40280  cdleme20j  40295  cdleme21c  40304  cdleme22b  40318  cdleme22d  40320  cdleme28a  40347  cdleme35a  40425  cdleme35fnpq  40426  cdleme35b  40427  cdleme35f  40431  cdleme42c  40449  cdleme42i  40460  cdlemf1  40538  cdlemg4c  40589  cdlemg6c  40597  cdlemg8b  40605  cdlemg10  40618  cdlemg11b  40619  cdlemg13a  40628  cdlemg17a  40638  cdlemg18b  40656  cdlemg27a  40669  cdlemg33b0  40678  cdlemg35  40690  cdlemg42  40706  cdlemg46  40712  trljco  40717  tendopltp  40757  cdlemk3  40810  cdlemk10  40820  cdlemk1u  40836  cdlemk39  40893  dialss  41023  dia2dimlem1  41041  dia2dimlem10  41050  dia2dimlem12  41052  cdlemm10N  41095  djajN  41114  diblss  41147  cdlemn2  41172  dihord2pre2  41203  dib2dim  41220  dih2dimb  41221  dih2dimbALTN  41222  dihmeetlem6  41286  dihjatcclem1  41395