Theorem latjle12 18360

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113  ⟨cop 4583   class class class wbr 5095  dom cdm 5621  ‘cfv 6488  (class class class)co 7354  Basecbs 17124  lecple 17172  Posetcpo 18217  joincjn 18221  meetcmee 18222  Latclat 18341

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-rep 5221  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7676

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-rmo 3347  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6444  df-fun 6490  df-fn 6491  df-f 6492  df-f1 6493  df-fo 6494  df-f1o 6495  df-fv 6496  df-riota 7311  df-ov 7357  df-oprab 7358  df-poset 18223  df-lub 18254  df-join 18256  df-lat 18342

This theorem is referenced by:  latleeqj1  18361  latjlej1  18363  latjidm  18372  latledi  18387  latjass  18393  mod1ile  18403  lubun  18425  oldmm1  39339  olj01  39347  cvlexchb1  39452  cvlcvr1  39461  hlrelat  39524  hlrelat2  39525  exatleN  39526  hlrelat3  39534  cvrexchlem  39541  cvratlem  39543  cvrat  39544  atlelt  39560  ps-1  39599  hlatexch3N  39602  hlatexch4  39603  3atlem1  39605  3atlem2  39606  lplnexllnN  39686  2llnjaN  39688  4atlem3  39718  4atlem10  39728  4atlem11b  39730  4atlem11  39731  4atlem12b  39733  4atlem12  39734  2lplnja  39741  dalem1  39781  dalem3  39786  dalem8  39792  dalem16  39801  dalem17  39802  dalem21  39816  dalem25  39820  dalem39  39833  dalem54  39848  dalem60  39854  linepsubN  39874  pmapsub  39890  lneq2at  39900  2llnma3r  39910  cdlema1N  39913  cdlemblem  39915  paddasslem5  39946  paddasslem12  39953  paddasslem13  39954  llnexchb2  39991  dalawlem3  39995  dalawlem5  39997  dalawlem8  40000  dalawlem11  40003  dalawlem12  40004  lhp2lt  40123  lhpexle2lem  40131  lhpexle3lem  40133  4atexlemtlw  40189  4atexlemnclw  40192  lautj  40215  cdlemd3  40322  cdleme3g  40356  cdleme3h  40357  cdleme7d  40368  cdleme11c  40383  cdleme15d  40399  cdleme17b  40409  cdleme19a  40425  cdleme20j  40440  cdleme21c  40449  cdleme22b  40463  cdleme22d  40465  cdleme28a  40492  cdleme35a  40570  cdleme35fnpq  40571  cdleme35b  40572  cdleme35f  40576  cdleme42c  40594  cdleme42i  40605  cdlemf1  40683  cdlemg4c  40734  cdlemg6c  40742  cdlemg8b  40750  cdlemg10  40763  cdlemg11b  40764  cdlemg13a  40773  cdlemg17a  40783  cdlemg18b  40801  cdlemg27a  40814  cdlemg33b0  40823  cdlemg35  40835  cdlemg42  40851  cdlemg46  40857  trljco  40862  tendopltp  40902  cdlemk3  40955  cdlemk10  40965  cdlemk1u  40981  cdlemk39  41038  dialss  41168  dia2dimlem1  41186  dia2dimlem10  41195  dia2dimlem12  41197  cdlemm10N  41240  djajN  41259  diblss  41292  cdlemn2  41317  dihord2pre2  41348  dib2dim  41365  dih2dimb  41366  dih2dimbALTN  41367  dihmeetlem6  41431  dihjatcclem1  41540