Theorem latjle12 17672

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 29286 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 17660	. . 3 ⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset)
5	4	adantr 483	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Poset)
6		simpr1 1190	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑋 ∈ 𝐵)
7		simpr2 1191	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌 ∈ 𝐵)
8		simpr3 1192	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍 ∈ 𝐵)
9		eqid 2821	. . . 4 ⊢ (meet‘𝐾) = (meet‘𝐾)
10		simpl 485	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Lat)
11	1, 3, 9, 10, 6, 7	latcl2 17658	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (⟨𝑋, 𝑌⟩ ∈ dom ∨ ∧ ⟨𝑋, 𝑌⟩ ∈ dom (meet‘𝐾)))
12	11	simpld 497	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ⟨𝑋, 𝑌⟩ ∈ dom ∨ )
13	1, 2, 3, 5, 6, 7, 8, 12	joinle 17624	1 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑍 ∧ 𝑌 ≤ 𝑍) ↔ (𝑋 ∨ 𝑌) ≤ 𝑍))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114  ⟨cop 4573   class class class wbr 5066  dom cdm 5555  ‘cfv 6355  (class class class)co 7156  Basecbs 16483  lecple 16572  Posetcpo 17550  joincjn 17554  meetcmee 17555  Latclat 17655

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-rep 5190  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-riota 7114  df-ov 7159  df-oprab 7160  df-poset 17556  df-lub 17584  df-join 17586  df-lat 17656

This theorem is referenced by:  latleeqj1  17673  latjlej1  17675  latjidm  17684  latledi  17699  latjass  17705  mod1ile  17715  lubun  17733  oldmm1  36368  olj01  36376  cvlexchb1  36481  cvlcvr1  36490  hlrelat  36553  hlrelat2  36554  exatleN  36555  hlrelat3  36563  cvrexchlem  36570  cvratlem  36572  cvrat  36573  atlelt  36589  ps-1  36628  hlatexch3N  36631  hlatexch4  36632  3atlem1  36634  3atlem2  36635  lplnexllnN  36715  2llnjaN  36717  4atlem3  36747  4atlem10  36757  4atlem11b  36759  4atlem11  36760  4atlem12b  36762  4atlem12  36763  2lplnja  36770  dalem1  36810  dalem3  36815  dalem8  36821  dalem16  36830  dalem17  36831  dalem21  36845  dalem25  36849  dalem39  36862  dalem54  36877  dalem60  36883  linepsubN  36903  pmapsub  36919  lneq2at  36929  2llnma3r  36939  cdlema1N  36942  cdlemblem  36944  paddasslem5  36975  paddasslem12  36982  paddasslem13  36983  llnexchb2  37020  dalawlem3  37024  dalawlem5  37026  dalawlem8  37029  dalawlem11  37032  dalawlem12  37033  lhp2lt  37152  lhpexle2lem  37160  lhpexle3lem  37162  4atexlemtlw  37218  4atexlemnclw  37221  lautj  37244  cdlemd3  37351  cdleme3g  37385  cdleme3h  37386  cdleme7d  37397  cdleme11c  37412  cdleme15d  37428  cdleme17b  37438  cdleme19a  37454  cdleme20j  37469  cdleme21c  37478  cdleme22b  37492  cdleme22d  37494  cdleme28a  37521  cdleme35a  37599  cdleme35fnpq  37600  cdleme35b  37601  cdleme35f  37605  cdleme42c  37623  cdleme42i  37634  cdlemf1  37712  cdlemg4c  37763  cdlemg6c  37771  cdlemg8b  37779  cdlemg10  37792  cdlemg11b  37793  cdlemg13a  37802  cdlemg17a  37812  cdlemg18b  37830  cdlemg27a  37843  cdlemg33b0  37852  cdlemg35  37864  cdlemg42  37880  cdlemg46  37886  trljco  37891  tendopltp  37931  cdlemk3  37984  cdlemk10  37994  cdlemk1u  38010  cdlemk39  38067  dialss  38197  dia2dimlem1  38215  dia2dimlem10  38224  dia2dimlem12  38226  cdlemm10N  38269  djajN  38288  diblss  38321  cdlemn2  38346  dihord2pre2  38377  dib2dim  38394  dih2dimb  38395  dih2dimbALTN  38396  dihmeetlem6  38460  dihjatcclem1  38569