Theorem latjle12 18531

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 31898 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 18519	. . 3 ⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset)
5	4	adantr 486	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Poset)
6		simpr1 1213	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑋 ∈ 𝐵)
7		simpr2 1214	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌 ∈ 𝐵)
8		simpr3 1215	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍 ∈ 𝐵)
9		eqid 2766	. . . 4 ⊢ (meet‘𝐾) = (meet‘𝐾)
10		simpl 488	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Lat)
11	1, 3, 9, 10, 6, 7	latcl2 18517	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (⟨𝑋, 𝑌⟩ ∈ dom ∨ ∧ ⟨𝑋, 𝑌⟩ ∈ dom (meet‘𝐾)))
12	11	simpld 500	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ⟨𝑋, 𝑌⟩ ∈ dom ∨ )
13	1, 2, 3, 5, 6, 7, 8, 12	joinle 18465	1 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑍 ∧ 𝑌 ≤ 𝑍) ↔ (𝑋 ∨ 𝑌) ≤ 𝑍))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146  ⟨cop 4600   class class class wbr 5114  dom cdm 5666  ‘cfv 6543  (class class class)co 7423  Basecbs 17294  lecple 17342  Posetcpo 18388  joincjn 18392  meetcmee 18393  Latclat 18512

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-rep 5243  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-rmo 3372  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7380  df-ov 7426  df-oprab 7427  df-poset 18394  df-lub 18425  df-join 18427  df-lat 18513

This theorem is used by:  latleeqj1  18532  latjlej1  18534  latjidm  18543  latledi  18558  latjass  18564  mod1ile  18574  lubun  18596  oldmm1  40032  olj01  40040  cvlexchb1  40145  cvlcvr1  40154  hlrelat  40217  hlrelat2  40218  exatleN  40219  hlrelat3  40227  cvrexchlem  40234  cvratlem  40236  cvrat  40237  atlelt  40253  ps-1  40292  hlatexch3N  40295  hlatexch4  40296  3atlem1  40298  3atlem2  40299  lplnexllnN  40379  2llnjaN  40381  4atlem3  40411  4atlem10  40421  4atlem11b  40423  4atlem11  40424  4atlem12b  40426  4atlem12  40427  2lplnja  40434  dalem1  40474  dalem3  40479  dalem8  40485  dalem16  40494  dalem17  40495  dalem21  40509  dalem25  40513  dalem39  40526  dalem54  40541  dalem60  40547  linepsubN  40567  pmapsub  40583  lneq2at  40593  2llnma3r  40603  cdlema1N  40606  cdlemblem  40608  paddasslem5  40639  paddasslem12  40646  paddasslem13  40647  llnexchb2  40684  dalawlem3  40688  dalawlem5  40690  dalawlem8  40693  dalawlem11  40696  dalawlem12  40697  lhp2lt  40816  lhpexle2lem  40824  lhpexle3lem  40826  4atexlemtlw  40882  4atexlemnclw  40885  lautj  40908  cdlemd3  41015  cdleme3g  41049  cdleme3h  41050  cdleme7d  41061  cdleme11c  41076  cdleme15d  41092  cdleme17b  41102  cdleme19a  41118  cdleme20j  41133  cdleme21c  41142  cdleme22b  41156  cdleme22d  41158  cdleme28a  41185  cdleme35a  41263  cdleme35fnpq  41264  cdleme35b  41265  cdleme35f  41269  cdleme42c  41287  cdleme42i  41298  cdlemf1  41376  cdlemg4c  41427  cdlemg6c  41435  cdlemg8b  41443  cdlemg10  41456  cdlemg11b  41457  cdlemg13a  41466  cdlemg17a  41476  cdlemg18b  41494  cdlemg27a  41507  cdlemg33b0  41516  cdlemg35  41528  cdlemg42  41544  cdlemg46  41550  trljco  41555  tendopltp  41595  cdlemk3  41648  cdlemk10  41658  cdlemk1u  41674  cdlemk39  41731  dialss  41861  dia2dimlem1  41879  dia2dimlem10  41888  dia2dimlem12  41890  cdlemm10N  41933  djajN  41952  diblss  41985  cdlemn2  42010  dihord2pre2  42041  dib2dim  42058  dih2dimb  42059  dih2dimbALTN  42060  dihmeetlem6  42124  dihjatcclem1  42233