Theorem latjle12 18416

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 31580 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 18404	. . 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 2736	. . . 4 ⊢ (meet‘𝐾) = (meet‘𝐾)
10		simpl 482	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Lat)
11	1, 3, 9, 10, 6, 7	latcl2 18402	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (⟨𝑋, 𝑌⟩ ∈ dom ∨ ∧ ⟨𝑋, 𝑌⟩ ∈ dom (meet‘𝐾)))
12	11	simpld 494	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ⟨𝑋, 𝑌⟩ ∈ dom ∨ )
13	1, 2, 3, 5, 6, 7, 8, 12	joinle 18350	1 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑍 ∧ 𝑌 ≤ 𝑍) ↔ (𝑋 ∨ 𝑌) ≤ 𝑍))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ⟨cop 4573   class class class wbr 5085  dom cdm 5631  ‘cfv 6498  (class class class)co 7367  Basecbs 17179  lecple 17227  Posetcpo 18273  joincjn 18277  meetcmee 18278  Latclat 18397

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 2708  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rmo 3342  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-riota 7324  df-ov 7370  df-oprab 7371  df-poset 18279  df-lub 18310  df-join 18312  df-lat 18398

This theorem is referenced by:  latleeqj1  18417  latjlej1  18419  latjidm  18428  latledi  18443  latjass  18449  mod1ile  18459  lubun  18481  oldmm1  39663  olj01  39671  cvlexchb1  39776  cvlcvr1  39785  hlrelat  39848  hlrelat2  39849  exatleN  39850  hlrelat3  39858  cvrexchlem  39865  cvratlem  39867  cvrat  39868  atlelt  39884  ps-1  39923  hlatexch3N  39926  hlatexch4  39927  3atlem1  39929  3atlem2  39930  lplnexllnN  40010  2llnjaN  40012  4atlem3  40042  4atlem10  40052  4atlem11b  40054  4atlem11  40055  4atlem12b  40057  4atlem12  40058  2lplnja  40065  dalem1  40105  dalem3  40110  dalem8  40116  dalem16  40125  dalem17  40126  dalem21  40140  dalem25  40144  dalem39  40157  dalem54  40172  dalem60  40178  linepsubN  40198  pmapsub  40214  lneq2at  40224  2llnma3r  40234  cdlema1N  40237  cdlemblem  40239  paddasslem5  40270  paddasslem12  40277  paddasslem13  40278  llnexchb2  40315  dalawlem3  40319  dalawlem5  40321  dalawlem8  40324  dalawlem11  40327  dalawlem12  40328  lhp2lt  40447  lhpexle2lem  40455  lhpexle3lem  40457  4atexlemtlw  40513  4atexlemnclw  40516  lautj  40539  cdlemd3  40646  cdleme3g  40680  cdleme3h  40681  cdleme7d  40692  cdleme11c  40707  cdleme15d  40723  cdleme17b  40733  cdleme19a  40749  cdleme20j  40764  cdleme21c  40773  cdleme22b  40787  cdleme22d  40789  cdleme28a  40816  cdleme35a  40894  cdleme35fnpq  40895  cdleme35b  40896  cdleme35f  40900  cdleme42c  40918  cdleme42i  40929  cdlemf1  41007  cdlemg4c  41058  cdlemg6c  41066  cdlemg8b  41074  cdlemg10  41087  cdlemg11b  41088  cdlemg13a  41097  cdlemg17a  41107  cdlemg18b  41125  cdlemg27a  41138  cdlemg33b0  41147  cdlemg35  41159  cdlemg42  41175  cdlemg46  41181  trljco  41186  tendopltp  41226  cdlemk3  41279  cdlemk10  41289  cdlemk1u  41305  cdlemk39  41362  dialss  41492  dia2dimlem1  41510  dia2dimlem10  41519  dia2dimlem12  41521  cdlemm10N  41564  djajN  41583  diblss  41616  cdlemn2  41641  dihord2pre2  41672  dib2dim  41689  dih2dimb  41690  dih2dimbALTN  41691  dihmeetlem6  41755  dihjatcclem1  41864