Theorem latjle12 17524

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 29061 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 17512	. . 3 ⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset)
5	4	adantr 473	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Poset)
6		simpr1 1174	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑋 ∈ 𝐵)
7		simpr2 1175	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌 ∈ 𝐵)
8		simpr3 1176	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍 ∈ 𝐵)
9		eqid 2775	. . . 4 ⊢ (meet‘𝐾) = (meet‘𝐾)
10		simpl 475	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Lat)
11	1, 3, 9, 10, 6, 7	latcl2 17510	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (⟨𝑋, 𝑌⟩ ∈ dom ∨ ∧ ⟨𝑋, 𝑌⟩ ∈ dom (meet‘𝐾)))
12	11	simpld 487	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ⟨𝑋, 𝑌⟩ ∈ dom ∨ )
13	1, 2, 3, 5, 6, 7, 8, 12	joinle 17476	1 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑍 ∧ 𝑌 ≤ 𝑍) ↔ (𝑋 ∨ 𝑌) ≤ 𝑍))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   ∧ w3a 1068   = wceq 1507   ∈ wcel 2048  ⟨cop 4445   class class class wbr 4927  dom cdm 5404  ‘cfv 6186  (class class class)co 6974  Basecbs 16333  lecple 16422  Posetcpo 17402  joincjn 17406  meetcmee 17407  Latclat 17507

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2747  ax-rep 5047  ax-sep 5058  ax-nul 5065  ax-pow 5117  ax-pr 5184  ax-un 7277

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2756  df-cleq 2768  df-clel 2843  df-nfc 2915  df-ne 2965  df-ral 3090  df-rex 3091  df-reu 3092  df-rab 3094  df-v 3414  df-sbc 3681  df-csb 3786  df-dif 3831  df-un 3833  df-in 3835  df-ss 3842  df-nul 4178  df-if 4349  df-pw 4422  df-sn 4440  df-pr 4442  df-op 4446  df-uni 4711  df-iun 4792  df-br 4928  df-opab 4990  df-mpt 5007  df-id 5309  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-fv 6194  df-riota 6935  df-ov 6977  df-oprab 6978  df-poset 17408  df-lub 17436  df-join 17438  df-lat 17508

This theorem is referenced by:  latleeqj1  17525  latjlej1  17527  latjidm  17536  latledi  17551  latjass  17557  mod1ile  17567  lubun  17585  oldmm1  35776  olj01  35784  cvlexchb1  35889  cvlcvr1  35898  hlrelat  35961  hlrelat2  35962  exatleN  35963  hlrelat3  35971  cvrexchlem  35978  cvratlem  35980  cvrat  35981  atlelt  35997  ps-1  36036  hlatexch3N  36039  hlatexch4  36040  3atlem1  36042  3atlem2  36043  lplnexllnN  36123  2llnjaN  36125  4atlem3  36155  4atlem10  36165  4atlem11b  36167  4atlem11  36168  4atlem12b  36170  4atlem12  36171  2lplnja  36178  dalem1  36218  dalem3  36223  dalem8  36229  dalem16  36238  dalem17  36239  dalem21  36253  dalem25  36257  dalem39  36270  dalem54  36285  dalem60  36291  linepsubN  36311  pmapsub  36327  lneq2at  36337  2llnma3r  36347  cdlema1N  36350  cdlemblem  36352  paddasslem5  36383  paddasslem12  36390  paddasslem13  36391  llnexchb2  36428  dalawlem3  36432  dalawlem5  36434  dalawlem8  36437  dalawlem11  36440  dalawlem12  36441  lhp2lt  36560  lhpexle2lem  36568  lhpexle3lem  36570  4atexlemtlw  36626  4atexlemnclw  36629  lautj  36652  cdlemd3  36759  cdleme3g  36793  cdleme3h  36794  cdleme7d  36805  cdleme11c  36820  cdleme15d  36836  cdleme17b  36846  cdleme19a  36862  cdleme20j  36877  cdleme21c  36886  cdleme22b  36900  cdleme22d  36902  cdleme28a  36929  cdleme35a  37007  cdleme35fnpq  37008  cdleme35b  37009  cdleme35f  37013  cdleme42c  37031  cdleme42i  37042  cdlemf1  37120  cdlemg4c  37171  cdlemg6c  37179  cdlemg8b  37187  cdlemg10  37200  cdlemg11b  37201  cdlemg13a  37210  cdlemg17a  37220  cdlemg18b  37238  cdlemg27a  37251  cdlemg33b0  37260  cdlemg35  37272  cdlemg42  37288  cdlemg46  37294  trljco  37299  tendopltp  37339  cdlemk3  37392  cdlemk10  37402  cdlemk1u  37418  cdlemk39  37475  dialss  37605  dia2dimlem1  37623  dia2dimlem10  37632  dia2dimlem12  37634  cdlemm10N  37677  djajN  37696  diblss  37729  cdlemn2  37754  dihord2pre2  37785  dib2dim  37802  dih2dimb  37803  dih2dimbALTN  37804  dihmeetlem6  37868  dihjatcclem1  37977