Theorem latjle12 18407

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ⟨cop 4574   class class class wbr 5086  dom cdm 5624  ‘cfv 6492  (class class class)co 7360  Basecbs 17170  lecple 17218  Posetcpo 18264  joincjn 18268  meetcmee 18269  Latclat 18388

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  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 7317  df-ov 7363  df-oprab 7364  df-poset 18270  df-lub 18301  df-join 18303  df-lat 18389

This theorem is referenced by:  latleeqj1  18408  latjlej1  18410  latjidm  18419  latledi  18434  latjass  18440  mod1ile  18450  lubun  18472  oldmm1  39677  olj01  39685  cvlexchb1  39790  cvlcvr1  39799  hlrelat  39862  hlrelat2  39863  exatleN  39864  hlrelat3  39872  cvrexchlem  39879  cvratlem  39881  cvrat  39882  atlelt  39898  ps-1  39937  hlatexch3N  39940  hlatexch4  39941  3atlem1  39943  3atlem2  39944  lplnexllnN  40024  2llnjaN  40026  4atlem3  40056  4atlem10  40066  4atlem11b  40068  4atlem11  40069  4atlem12b  40071  4atlem12  40072  2lplnja  40079  dalem1  40119  dalem3  40124  dalem8  40130  dalem16  40139  dalem17  40140  dalem21  40154  dalem25  40158  dalem39  40171  dalem54  40186  dalem60  40192  linepsubN  40212  pmapsub  40228  lneq2at  40238  2llnma3r  40248  cdlema1N  40251  cdlemblem  40253  paddasslem5  40284  paddasslem12  40291  paddasslem13  40292  llnexchb2  40329  dalawlem3  40333  dalawlem5  40335  dalawlem8  40338  dalawlem11  40341  dalawlem12  40342  lhp2lt  40461  lhpexle2lem  40469  lhpexle3lem  40471  4atexlemtlw  40527  4atexlemnclw  40530  lautj  40553  cdlemd3  40660  cdleme3g  40694  cdleme3h  40695  cdleme7d  40706  cdleme11c  40721  cdleme15d  40737  cdleme17b  40747  cdleme19a  40763  cdleme20j  40778  cdleme21c  40787  cdleme22b  40801  cdleme22d  40803  cdleme28a  40830  cdleme35a  40908  cdleme35fnpq  40909  cdleme35b  40910  cdleme35f  40914  cdleme42c  40932  cdleme42i  40943  cdlemf1  41021  cdlemg4c  41072  cdlemg6c  41080  cdlemg8b  41088  cdlemg10  41101  cdlemg11b  41102  cdlemg13a  41111  cdlemg17a  41121  cdlemg18b  41139  cdlemg27a  41152  cdlemg33b0  41161  cdlemg35  41173  cdlemg42  41189  cdlemg46  41195  trljco  41200  tendopltp  41240  cdlemk3  41293  cdlemk10  41303  cdlemk1u  41319  cdlemk39  41376  dialss  41506  dia2dimlem1  41524  dia2dimlem10  41533  dia2dimlem12  41535  cdlemm10N  41578  djajN  41597  diblss  41630  cdlemn2  41655  dihord2pre2  41686  dib2dim  41703  dih2dimb  41704  dih2dimbALTN  41705  dihmeetlem6  41769  dihjatcclem1  41878