Theorem latjle12 17263

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 28677 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 17251	. . 3 ⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset)
5	4	adantr 472	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Poset)
6		simpr1 1234	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑋 ∈ 𝐵)
7		simpr2 1236	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌 ∈ 𝐵)
8		simpr3 1238	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍 ∈ 𝐵)
9		eqid 2760	. . . 4 ⊢ (meet‘𝐾) = (meet‘𝐾)
10		simpl 474	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Lat)
11	1, 3, 9, 10, 6, 7	latcl2 17249	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (⟨𝑋, 𝑌⟩ ∈ dom ∨ ∧ ⟨𝑋, 𝑌⟩ ∈ dom (meet‘𝐾)))
12	11	simpld 477	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ⟨𝑋, 𝑌⟩ ∈ dom ∨ )
13	1, 2, 3, 5, 6, 7, 8, 12	joinle 17215	1 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑍 ∧ 𝑌 ≤ 𝑍) ↔ (𝑋 ∨ 𝑌) ≤ 𝑍))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1072   = wceq 1632   ∈ wcel 2139  ⟨cop 4327   class class class wbr 4804  dom cdm 5266  ‘cfv 6049  (class class class)co 6813  Basecbs 16059  lecple 16150  Posetcpo 17141  joincjn 17145  meetcmee 17146  Latclat 17246

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-reu 3057  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6774  df-ov 6816  df-oprab 6817  df-poset 17147  df-lub 17175  df-join 17177  df-lat 17247

This theorem is referenced by:  latleeqj1  17264  latjlej1  17266  latjidm  17275  latledi  17290  latjass  17296  mod1ile  17306  lubun  17324  oldmm1  35007  olj01  35015  cvlexchb1  35120  cvlcvr1  35129  hlrelat  35191  hlrelat2  35192  exatleN  35193  hlrelat3  35201  cvrexchlem  35208  cvratlem  35210  cvrat  35211  atlelt  35227  ps-1  35266  hlatexch3N  35269  hlatexch4  35270  3atlem1  35272  3atlem2  35273  lplnexllnN  35353  2llnjaN  35355  4atlem3  35385  4atlem10  35395  4atlem11b  35397  4atlem11  35398  4atlem12b  35400  4atlem12  35401  2lplnja  35408  dalem1  35448  dalem3  35453  dalem8  35459  dalem16  35468  dalem17  35469  dalem21  35483  dalem25  35487  dalem39  35500  dalem54  35515  dalem60  35521  linepsubN  35541  pmapsub  35557  lneq2at  35567  2llnma3r  35577  cdlema1N  35580  cdlemblem  35582  paddasslem5  35613  paddasslem12  35620  paddasslem13  35621  llnexchb2  35658  dalawlem3  35662  dalawlem5  35664  dalawlem8  35667  dalawlem11  35670  dalawlem12  35671  lhp2lt  35790  lhpexle2lem  35798  lhpexle3lem  35800  4atexlemtlw  35856  4atexlemnclw  35859  lautj  35882  cdlemd3  35990  cdleme3g  36024  cdleme3h  36025  cdleme7d  36036  cdleme11c  36051  cdleme15d  36067  cdleme17b  36077  cdleme19a  36093  cdleme20j  36108  cdleme21c  36117  cdleme22b  36131  cdleme22d  36133  cdleme28a  36160  cdleme35a  36238  cdleme35fnpq  36239  cdleme35b  36240  cdleme35f  36244  cdleme42c  36262  cdleme42i  36273  cdlemf1  36351  cdlemg4c  36402  cdlemg6c  36410  cdlemg8b  36418  cdlemg10  36431  cdlemg11b  36432  cdlemg13a  36441  cdlemg17a  36451  cdlemg18b  36469  cdlemg27a  36482  cdlemg33b0  36491  cdlemg35  36503  cdlemg42  36519  cdlemg46  36525  trljco  36530  tendopltp  36570  cdlemk3  36623  cdlemk10  36633  cdlemk1u  36649  cdlemk39  36706  dialss  36837  dia2dimlem1  36855  dia2dimlem10  36864  dia2dimlem12  36866  cdlemm10N  36909  djajN  36928  diblss  36961  cdlemn2  36986  dihord2pre2  37017  dib2dim  37034  dih2dimb  37035  dih2dimbALTN  37036  dihmeetlem6  37100  dihjatcclem1  37209