Theorem latjle12 18414

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 31605 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 18402	. . 3 ⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset)
5	4	adantr 481	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Poset)
6		simpr1 1201	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑋 ∈ 𝐵)
7		simpr2 1202	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌 ∈ 𝐵)
8		simpr3 1203	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍 ∈ 𝐵)
9		eqid 2740	. . . 4 ⊢ (meet‘𝐾) = (meet‘𝐾)
10		simpl 483	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Lat)
11	1, 3, 9, 10, 6, 7	latcl2 18400	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (⟨𝑋, 𝑌⟩ ∈ dom ∨ ∧ ⟨𝑋, 𝑌⟩ ∈ dom (meet‘𝐾)))
12	11	simpld 495	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ⟨𝑋, 𝑌⟩ ∈ dom ∨ )
13	1, 2, 3, 5, 6, 7, 8, 12	joinle 18348	1 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑍 ∧ 𝑌 ≤ 𝑍) ↔ (𝑋 ∨ 𝑌) ≤ 𝑍))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119  ⟨cop 4568   class class class wbr 5079  dom cdm 5625  ‘cfv 6492  (class class class)co 7363  Basecbs 17177  lecple 17225  Posetcpo 18271  joincjn 18275  meetcmee 18276  Latclat 18395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-rep 5206  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rmo 3345  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-iun 4930  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  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 7320  df-ov 7366  df-oprab 7367  df-poset 18277  df-lub 18308  df-join 18310  df-lat 18396

This theorem is referenced by:  latleeqj1  18415  latjlej1  18417  latjidm  18426  latledi  18441  latjass  18447  mod1ile  18457  lubun  18479  oldmm1  39716  olj01  39724  cvlexchb1  39829  cvlcvr1  39838  hlrelat  39901  hlrelat2  39902  exatleN  39903  hlrelat3  39911  cvrexchlem  39918  cvratlem  39920  cvrat  39921  atlelt  39937  ps-1  39976  hlatexch3N  39979  hlatexch4  39980  3atlem1  39982  3atlem2  39983  lplnexllnN  40063  2llnjaN  40065  4atlem3  40095  4atlem10  40105  4atlem11b  40107  4atlem11  40108  4atlem12b  40110  4atlem12  40111  2lplnja  40118  dalem1  40158  dalem3  40163  dalem8  40169  dalem16  40178  dalem17  40179  dalem21  40193  dalem25  40197  dalem39  40210  dalem54  40225  dalem60  40231  linepsubN  40251  pmapsub  40267  lneq2at  40277  2llnma3r  40287  cdlema1N  40290  cdlemblem  40292  paddasslem5  40323  paddasslem12  40330  paddasslem13  40331  llnexchb2  40368  dalawlem3  40372  dalawlem5  40374  dalawlem8  40377  dalawlem11  40380  dalawlem12  40381  lhp2lt  40500  lhpexle2lem  40508  lhpexle3lem  40510  4atexlemtlw  40566  4atexlemnclw  40569  lautj  40592  cdlemd3  40699  cdleme3g  40733  cdleme3h  40734  cdleme7d  40745  cdleme11c  40760  cdleme15d  40776  cdleme17b  40786  cdleme19a  40802  cdleme20j  40817  cdleme21c  40826  cdleme22b  40840  cdleme22d  40842  cdleme28a  40869  cdleme35a  40947  cdleme35fnpq  40948  cdleme35b  40949  cdleme35f  40953  cdleme42c  40971  cdleme42i  40982  cdlemf1  41060  cdlemg4c  41111  cdlemg6c  41119  cdlemg8b  41127  cdlemg10  41140  cdlemg11b  41141  cdlemg13a  41150  cdlemg17a  41160  cdlemg18b  41178  cdlemg27a  41191  cdlemg33b0  41200  cdlemg35  41212  cdlemg42  41228  cdlemg46  41234  trljco  41239  tendopltp  41279  cdlemk3  41332  cdlemk10  41342  cdlemk1u  41358  cdlemk39  41415  dialss  41545  dia2dimlem1  41563  dia2dimlem10  41572  dia2dimlem12  41574  cdlemm10N  41617  djajN  41636  diblss  41669  cdlemn2  41694  dihord2pre2  41725  dib2dim  41742  dih2dimb  41743  dih2dimbALTN  41744  dihmeetlem6  41808  dihjatcclem1  41917