Theorem latjle12 18494

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 31766 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 18482	. . 3 ⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset)
5	4	adantr 485	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Poset)
6		simpr1 1211	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑋 ∈ 𝐵)
7		simpr2 1212	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌 ∈ 𝐵)
8		simpr3 1213	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍 ∈ 𝐵)
9		eqid 2765	. . . 4 ⊢ (meet‘𝐾) = (meet‘𝐾)
10		simpl 487	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Lat)
11	1, 3, 9, 10, 6, 7	latcl2 18480	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (⟨𝑋, 𝑌⟩ ∈ dom ∨ ∧ ⟨𝑋, 𝑌⟩ ∈ dom (meet‘𝐾)))
12	11	simpld 499	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ⟨𝑋, 𝑌⟩ ∈ dom ∨ )
13	1, 2, 3, 5, 6, 7, 8, 12	joinle 18428	1 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑍 ∧ 𝑌 ≤ 𝑍) ↔ (𝑋 ∨ 𝑌) ≤ 𝑍))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1101   = wceq 1563   ∈ wcel 2145  ⟨cop 4591   class class class wbr 5104  dom cdm 5651  ‘cfv 6525  (class class class)co 7400  Basecbs 17257  lecple 17305  Posetcpo 18351  joincjn 18355  meetcmee 18356  Latclat 18475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-rep 5231  ax-sep 5250  ax-nul 5260  ax-pow 5326  ax-pr 5394  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rmo 3370  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5105  df-opab 5167  df-mpt 5186  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-riota 7357  df-ov 7403  df-oprab 7404  df-poset 18357  df-lub 18388  df-join 18390  df-lat 18476

This theorem is referenced by:  latleeqj1  18495  latjlej1  18497  latjidm  18506  latledi  18521  latjass  18527  mod1ile  18537  lubun  18559  oldmm1  39848  olj01  39856  cvlexchb1  39961  cvlcvr1  39970  hlrelat  40033  hlrelat2  40034  exatleN  40035  hlrelat3  40043  cvrexchlem  40050  cvratlem  40052  cvrat  40053  atlelt  40069  ps-1  40108  hlatexch3N  40111  hlatexch4  40112  3atlem1  40114  3atlem2  40115  lplnexllnN  40195  2llnjaN  40197  4atlem3  40227  4atlem10  40237  4atlem11b  40239  4atlem11  40240  4atlem12b  40242  4atlem12  40243  2lplnja  40250  dalem1  40290  dalem3  40295  dalem8  40301  dalem16  40310  dalem17  40311  dalem21  40325  dalem25  40329  dalem39  40342  dalem54  40357  dalem60  40363  linepsubN  40383  pmapsub  40399  lneq2at  40409  2llnma3r  40419  cdlema1N  40422  cdlemblem  40424  paddasslem5  40455  paddasslem12  40462  paddasslem13  40463  llnexchb2  40500  dalawlem3  40504  dalawlem5  40506  dalawlem8  40509  dalawlem11  40512  dalawlem12  40513  lhp2lt  40632  lhpexle2lem  40640  lhpexle3lem  40642  4atexlemtlw  40698  4atexlemnclw  40701  lautj  40724  cdlemd3  40831  cdleme3g  40865  cdleme3h  40866  cdleme7d  40877  cdleme11c  40892  cdleme15d  40908  cdleme17b  40918  cdleme19a  40934  cdleme20j  40949  cdleme21c  40958  cdleme22b  40972  cdleme22d  40974  cdleme28a  41001  cdleme35a  41079  cdleme35fnpq  41080  cdleme35b  41081  cdleme35f  41085  cdleme42c  41103  cdleme42i  41114  cdlemf1  41192  cdlemg4c  41243  cdlemg6c  41251  cdlemg8b  41259  cdlemg10  41272  cdlemg11b  41273  cdlemg13a  41282  cdlemg17a  41292  cdlemg18b  41310  cdlemg27a  41323  cdlemg33b0  41332  cdlemg35  41344  cdlemg42  41360  cdlemg46  41366  trljco  41371  tendopltp  41411  cdlemk3  41464  cdlemk10  41474  cdlemk1u  41490  cdlemk39  41547  dialss  41677  dia2dimlem1  41695  dia2dimlem10  41704  dia2dimlem12  41706  cdlemm10N  41749  djajN  41768  diblss  41801  cdlemn2  41826  dihord2pre2  41857  dib2dim  41874  dih2dimb  41875  dih2dimbALTN  41876  dihmeetlem6  41940  dihjatcclem1  42049