Theorem latjle12 18656

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 32144 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 18644	. . 3 ⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset)
5	4	adantr 486	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Poset)
6		simpr1 1213	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑋 ∈ 𝐵)
7		simpr2 1214	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌 ∈ 𝐵)
8		simpr3 1215	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍 ∈ 𝐵)
9		eqid 2763	. . . 4 ⊢ (meet‘𝐾) = (meet‘𝐾)
10		simpl 488	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Lat)
11	1, 3, 9, 10, 6, 7	latcl2 18642	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (⟨𝑋, 𝑌⟩ ∈ dom ∨ ∧ ⟨𝑋, 𝑌⟩ ∈ dom (meet‘𝐾)))
12	11	simpld 500	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ⟨𝑋, 𝑌⟩ ∈ dom ∨ )
13	1, 2, 3, 5, 6, 7, 8, 12	joinle 18590	1 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑍 ∧ 𝑌 ≤ 𝑍) ↔ (𝑋 ∨ 𝑌) ≤ 𝑍))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147  ⟨cop 4838   class class class wbr 5106  dom cdm 5656  ‘cfv 6561  (class class class)co 7446  Basecbs 17419  lecple 17467  Posetcpo 18513  joincjn 18517  meetcmee 18518  Latclat 18637

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5236  ax-sep 5253  ax-nul 5264  ax-pow 5332  ax-pr 5396  ax-un 7778

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5172  df-mpt 5191  df-id 5551  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-iota 6515  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7403  df-ov 7449  df-oprab 7450  df-poset 18519  df-lub 18550  df-join 18552  df-lat 18638

This theorem is used by:  latleeqj1  18657  latjlej1  18659  latjidm  18668  latledi  18683  latjass  18689  mod1ile  18699  lubun  18721  oldmm1  40477  olj01  40485  cvlexchb1  40590  cvlcvr1  40599  hlrelat  40662  hlrelat2  40663  exatleN  40664  hlrelat3  40672  cvrexchlem  40679  cvratlem  40681  cvrat  40682  atlelt  40698  ps-1  40737  hlatexch3N  40740  hlatexch4  40741  3atlem1  40743  3atlem2  40744  lplnexllnN  40824  2llnjaN  40826  4atlem3  40856  4atlem10  40866  4atlem11b  40868  4atlem11  40869  4atlem12b  40871  4atlem12  40872  2lplnja  40879  dalem1  40919  dalem3  40924  dalem8  40930  dalem16  40939  dalem17  40940  dalem21  40954  dalem25  40958  dalem39  40971  dalem54  40986  dalem60  40992  linepsubN  41012  pmapsub  41028  lneq2at  41038  2llnma3r  41048  cdlema1N  41051  cdlemblem  41053  paddasslem5  41084  paddasslem12  41091  paddasslem13  41092  llnexchb2  41129  dalawlem3  41133  dalawlem5  41135  dalawlem8  41138  dalawlem11  41141  dalawlem12  41142  lhp2lt  41261  lhpexle2lem  41269  lhpexle3lem  41271  4atexlemtlw  41327  4atexlemnclw  41330  lautj  41353  cdlemd3  41460  cdleme3g  41494  cdleme3h  41495  cdleme7d  41506  cdleme11c  41521  cdleme15d  41537  cdleme17b  41547  cdleme19a  41563  cdleme20j  41578  cdleme21c  41587  cdleme22b  41601  cdleme22d  41603  cdleme28a  41630  cdleme35a  41708  cdleme35fnpq  41709  cdleme35b  41710  cdleme35f  41714  cdleme42c  41732  cdleme42i  41743  cdlemf1  41821  cdlemg4c  41872  cdlemg6c  41880  cdlemg8b  41888  cdlemg10  41901  cdlemg11b  41902  cdlemg13a  41911  cdlemg17a  41921  cdlemg18b  41939  cdlemg27a  41952  cdlemg33b0  41961  cdlemg35  41973  cdlemg42  41989  cdlemg46  41995  trljco  42000  tendopltp  42040  cdlemk3  42093  cdlemk10  42103  cdlemk1u  42119  cdlemk39  42176  dialss  42306  dia2dimlem1  42324  dia2dimlem10  42333  dia2dimlem12  42335  cdlemm10N  42378  djajN  42397  diblss  42430  cdlemn2  42455  dihord2pre2  42486  dib2dim  42503  dih2dimb  42504  dih2dimbALTN  42505  dihmeetlem6  42569  dihjatcclem1  42678