Theorem latjle12 17270

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 28708 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 17258	. . 3 ⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset)
5	4	adantr 466	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Poset)
6		simpr1 1233	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑋 ∈ 𝐵)
7		simpr2 1235	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌 ∈ 𝐵)
8		simpr3 1237	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍 ∈ 𝐵)
9		eqid 2771	. . . 4 ⊢ (meet‘𝐾) = (meet‘𝐾)
10		simpl 468	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Lat)
11	1, 3, 9, 10, 6, 7	latcl2 17256	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (⟨𝑋, 𝑌⟩ ∈ dom ∨ ∧ ⟨𝑋, 𝑌⟩ ∈ dom (meet‘𝐾)))
12	11	simpld 482	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ⟨𝑋, 𝑌⟩ ∈ dom ∨ )
13	1, 2, 3, 5, 6, 7, 8, 12	joinle 17222	1 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑍 ∧ 𝑌 ≤ 𝑍) ↔ (𝑋 ∨ 𝑌) ≤ 𝑍))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 382   ∧ w3a 1071   = wceq 1631   ∈ wcel 2145  ⟨cop 4322   class class class wbr 4786  dom cdm 5249  ‘cfv 6031  (class class class)co 6793  Basecbs 16064  lecple 16156  Posetcpo 17148  joincjn 17152  meetcmee 17153  Latclat 17253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-riota 6754  df-ov 6796  df-oprab 6797  df-poset 17154  df-lub 17182  df-join 17184  df-lat 17254

This theorem is referenced by:  latleeqj1  17271  latjlej1  17273  latjidm  17282  latledi  17297  latjass  17303  mod1ile  17313  lubun  17331  oldmm1  35026  olj01  35034  cvlexchb1  35139  cvlcvr1  35148  hlrelat  35210  hlrelat2  35211  exatleN  35212  hlrelat3  35220  cvrexchlem  35227  cvratlem  35229  cvrat  35230  atlelt  35246  ps-1  35285  hlatexch3N  35288  hlatexch4  35289  3atlem1  35291  3atlem2  35292  lplnexllnN  35372  2llnjaN  35374  4atlem3  35404  4atlem10  35414  4atlem11b  35416  4atlem11  35417  4atlem12b  35419  4atlem12  35420  2lplnja  35427  dalem1  35467  dalem3  35472  dalem8  35478  dalem16  35487  dalem17  35488  dalem21  35502  dalem25  35506  dalem39  35519  dalem54  35534  dalem60  35540  linepsubN  35560  pmapsub  35576  lneq2at  35586  2llnma3r  35596  cdlema1N  35599  cdlemblem  35601  paddasslem5  35632  paddasslem12  35639  paddasslem13  35640  llnexchb2  35677  dalawlem3  35681  dalawlem5  35683  dalawlem8  35686  dalawlem11  35689  dalawlem12  35690  lhp2lt  35809  lhpexle2lem  35817  lhpexle3lem  35819  4atexlemtlw  35875  4atexlemnclw  35878  lautj  35901  cdlemd3  36009  cdleme3g  36043  cdleme3h  36044  cdleme7d  36055  cdleme11c  36070  cdleme15d  36086  cdleme17b  36096  cdleme19a  36112  cdleme20j  36127  cdleme21c  36136  cdleme22b  36150  cdleme22d  36152  cdleme28a  36179  cdleme35a  36257  cdleme35fnpq  36258  cdleme35b  36259  cdleme35f  36263  cdleme42c  36281  cdleme42i  36292  cdlemf1  36370  cdlemg4c  36421  cdlemg6c  36429  cdlemg8b  36437  cdlemg10  36450  cdlemg11b  36451  cdlemg13a  36460  cdlemg17a  36470  cdlemg18b  36488  cdlemg27a  36501  cdlemg33b0  36510  cdlemg35  36522  cdlemg42  36538  cdlemg46  36544  trljco  36549  tendopltp  36589  cdlemk3  36642  cdlemk10  36652  cdlemk1u  36668  cdlemk39  36725  dialss  36856  dia2dimlem1  36874  dia2dimlem10  36883  dia2dimlem12  36885  cdlemm10N  36928  djajN  36947  diblss  36980  cdlemn2  37005  dihord2pre2  37036  dib2dim  37053  dih2dimb  37054  dih2dimbALTN  37055  dihmeetlem6  37119  dihjatcclem1  37228