Theorem latjle12 18385

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ⟨cop 4588   class class class wbr 5100  dom cdm 5632  ‘cfv 6500  (class class class)co 7368  Basecbs 17148  lecple 17196  Posetcpo 18242  joincjn 18246  meetcmee 18247  Latclat 18366

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 2709  ax-rep 5226  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7325  df-ov 7371  df-oprab 7372  df-poset 18248  df-lub 18279  df-join 18281  df-lat 18367

This theorem is referenced by:  latleeqj1  18386  latjlej1  18388  latjidm  18397  latledi  18412  latjass  18418  mod1ile  18428  lubun  18450  oldmm1  39590  olj01  39598  cvlexchb1  39703  cvlcvr1  39712  hlrelat  39775  hlrelat2  39776  exatleN  39777  hlrelat3  39785  cvrexchlem  39792  cvratlem  39794  cvrat  39795  atlelt  39811  ps-1  39850  hlatexch3N  39853  hlatexch4  39854  3atlem1  39856  3atlem2  39857  lplnexllnN  39937  2llnjaN  39939  4atlem3  39969  4atlem10  39979  4atlem11b  39981  4atlem11  39982  4atlem12b  39984  4atlem12  39985  2lplnja  39992  dalem1  40032  dalem3  40037  dalem8  40043  dalem16  40052  dalem17  40053  dalem21  40067  dalem25  40071  dalem39  40084  dalem54  40099  dalem60  40105  linepsubN  40125  pmapsub  40141  lneq2at  40151  2llnma3r  40161  cdlema1N  40164  cdlemblem  40166  paddasslem5  40197  paddasslem12  40204  paddasslem13  40205  llnexchb2  40242  dalawlem3  40246  dalawlem5  40248  dalawlem8  40251  dalawlem11  40254  dalawlem12  40255  lhp2lt  40374  lhpexle2lem  40382  lhpexle3lem  40384  4atexlemtlw  40440  4atexlemnclw  40443  lautj  40466  cdlemd3  40573  cdleme3g  40607  cdleme3h  40608  cdleme7d  40619  cdleme11c  40634  cdleme15d  40650  cdleme17b  40660  cdleme19a  40676  cdleme20j  40691  cdleme21c  40700  cdleme22b  40714  cdleme22d  40716  cdleme28a  40743  cdleme35a  40821  cdleme35fnpq  40822  cdleme35b  40823  cdleme35f  40827  cdleme42c  40845  cdleme42i  40856  cdlemf1  40934  cdlemg4c  40985  cdlemg6c  40993  cdlemg8b  41001  cdlemg10  41014  cdlemg11b  41015  cdlemg13a  41024  cdlemg17a  41034  cdlemg18b  41052  cdlemg27a  41065  cdlemg33b0  41074  cdlemg35  41086  cdlemg42  41102  cdlemg46  41108  trljco  41113  tendopltp  41153  cdlemk3  41206  cdlemk10  41216  cdlemk1u  41232  cdlemk39  41289  dialss  41419  dia2dimlem1  41437  dia2dimlem10  41446  dia2dimlem12  41448  cdlemm10N  41491  djajN  41510  diblss  41543  cdlemn2  41568  dihord2pre2  41599  dib2dim  41616  dih2dimb  41617  dih2dimbALTN  41618  dihmeetlem6  41682  dihjatcclem1  41791