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 31445 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 1195	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑋 ∈ 𝐵)
7		simpr2 1196	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌 ∈ 𝐵)
8		simpr3 1197	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍 ∈ 𝐵)
9		eqid 2730	. . . 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 18352	1 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑍 ∧ 𝑌 ≤ 𝑍) ↔ (𝑋 ∨ 𝑌) ≤ 𝑍))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ⟨cop 4598   class class class wbr 5110  dom cdm 5641  ‘cfv 6514  (class class class)co 7390  Basecbs 17186  lecple 17234  Posetcpo 18275  joincjn 18279  meetcmee 18280  Latclat 18397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-riota 7347  df-ov 7393  df-oprab 7394  df-poset 18281  df-lub 18312  df-join 18314  df-lat 18398

This theorem is referenced by:  latleeqj1  18417  latjlej1  18419  latjidm  18428  latledi  18443  latjass  18449  mod1ile  18459  lubun  18481  oldmm1  39217  olj01  39225  cvlexchb1  39330  cvlcvr1  39339  hlrelat  39403  hlrelat2  39404  exatleN  39405  hlrelat3  39413  cvrexchlem  39420  cvratlem  39422  cvrat  39423  atlelt  39439  ps-1  39478  hlatexch3N  39481  hlatexch4  39482  3atlem1  39484  3atlem2  39485  lplnexllnN  39565  2llnjaN  39567  4atlem3  39597  4atlem10  39607  4atlem11b  39609  4atlem11  39610  4atlem12b  39612  4atlem12  39613  2lplnja  39620  dalem1  39660  dalem3  39665  dalem8  39671  dalem16  39680  dalem17  39681  dalem21  39695  dalem25  39699  dalem39  39712  dalem54  39727  dalem60  39733  linepsubN  39753  pmapsub  39769  lneq2at  39779  2llnma3r  39789  cdlema1N  39792  cdlemblem  39794  paddasslem5  39825  paddasslem12  39832  paddasslem13  39833  llnexchb2  39870  dalawlem3  39874  dalawlem5  39876  dalawlem8  39879  dalawlem11  39882  dalawlem12  39883  lhp2lt  40002  lhpexle2lem  40010  lhpexle3lem  40012  4atexlemtlw  40068  4atexlemnclw  40071  lautj  40094  cdlemd3  40201  cdleme3g  40235  cdleme3h  40236  cdleme7d  40247  cdleme11c  40262  cdleme15d  40278  cdleme17b  40288  cdleme19a  40304  cdleme20j  40319  cdleme21c  40328  cdleme22b  40342  cdleme22d  40344  cdleme28a  40371  cdleme35a  40449  cdleme35fnpq  40450  cdleme35b  40451  cdleme35f  40455  cdleme42c  40473  cdleme42i  40484  cdlemf1  40562  cdlemg4c  40613  cdlemg6c  40621  cdlemg8b  40629  cdlemg10  40642  cdlemg11b  40643  cdlemg13a  40652  cdlemg17a  40662  cdlemg18b  40680  cdlemg27a  40693  cdlemg33b0  40702  cdlemg35  40714  cdlemg42  40730  cdlemg46  40736  trljco  40741  tendopltp  40781  cdlemk3  40834  cdlemk10  40844  cdlemk1u  40860  cdlemk39  40917  dialss  41047  dia2dimlem1  41065  dia2dimlem10  41074  dia2dimlem12  41076  cdlemm10N  41119  djajN  41138  diblss  41171  cdlemn2  41196  dihord2pre2  41227  dib2dim  41244  dih2dimb  41245  dih2dimbALTN  41246  dihmeetlem6  41310  dihjatcclem1  41419