Theorem latjle12 18373

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113  ⟨cop 4586   class class class wbr 5098  dom cdm 5624  ‘cfv 6492  (class class class)co 7358  Basecbs 17136  lecple 17184  Posetcpo 18230  joincjn 18234  meetcmee 18235  Latclat 18354

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-rep 5224  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rmo 3350  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7315  df-ov 7361  df-oprab 7362  df-poset 18236  df-lub 18267  df-join 18269  df-lat 18355

This theorem is referenced by:  latleeqj1  18374  latjlej1  18376  latjidm  18385  latledi  18400  latjass  18406  mod1ile  18416  lubun  18438  oldmm1  39477  olj01  39485  cvlexchb1  39590  cvlcvr1  39599  hlrelat  39662  hlrelat2  39663  exatleN  39664  hlrelat3  39672  cvrexchlem  39679  cvratlem  39681  cvrat  39682  atlelt  39698  ps-1  39737  hlatexch3N  39740  hlatexch4  39741  3atlem1  39743  3atlem2  39744  lplnexllnN  39824  2llnjaN  39826  4atlem3  39856  4atlem10  39866  4atlem11b  39868  4atlem11  39869  4atlem12b  39871  4atlem12  39872  2lplnja  39879  dalem1  39919  dalem3  39924  dalem8  39930  dalem16  39939  dalem17  39940  dalem21  39954  dalem25  39958  dalem39  39971  dalem54  39986  dalem60  39992  linepsubN  40012  pmapsub  40028  lneq2at  40038  2llnma3r  40048  cdlema1N  40051  cdlemblem  40053  paddasslem5  40084  paddasslem12  40091  paddasslem13  40092  llnexchb2  40129  dalawlem3  40133  dalawlem5  40135  dalawlem8  40138  dalawlem11  40141  dalawlem12  40142  lhp2lt  40261  lhpexle2lem  40269  lhpexle3lem  40271  4atexlemtlw  40327  4atexlemnclw  40330  lautj  40353  cdlemd3  40460  cdleme3g  40494  cdleme3h  40495  cdleme7d  40506  cdleme11c  40521  cdleme15d  40537  cdleme17b  40547  cdleme19a  40563  cdleme20j  40578  cdleme21c  40587  cdleme22b  40601  cdleme22d  40603  cdleme28a  40630  cdleme35a  40708  cdleme35fnpq  40709  cdleme35b  40710  cdleme35f  40714  cdleme42c  40732  cdleme42i  40743  cdlemf1  40821  cdlemg4c  40872  cdlemg6c  40880  cdlemg8b  40888  cdlemg10  40901  cdlemg11b  40902  cdlemg13a  40911  cdlemg17a  40921  cdlemg18b  40939  cdlemg27a  40952  cdlemg33b0  40961  cdlemg35  40973  cdlemg42  40989  cdlemg46  40995  trljco  41000  tendopltp  41040  cdlemk3  41093  cdlemk10  41103  cdlemk1u  41119  cdlemk39  41176  dialss  41306  dia2dimlem1  41324  dia2dimlem10  41333  dia2dimlem12  41335  cdlemm10N  41378  djajN  41397  diblss  41430  cdlemn2  41455  dihord2pre2  41486  dib2dim  41503  dih2dimb  41504  dih2dimbALTN  41505  dihmeetlem6  41569  dihjatcclem1  41678