Theorem latjle12 18507

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 31842 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 18495	. . 3 ⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset)
5	4	adantr 485	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Poset)
6		simpr1 1213	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑋 ∈ 𝐵)
7		simpr2 1214	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌 ∈ 𝐵)
8		simpr3 1215	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍 ∈ 𝐵)
9		eqid 2763	. . . 4 ⊢ (meet‘𝐾) = (meet‘𝐾)
10		simpl 487	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Lat)
11	1, 3, 9, 10, 6, 7	latcl2 18493	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (⟨𝑋, 𝑌⟩ ∈ dom ∨ ∧ ⟨𝑋, 𝑌⟩ ∈ dom (meet‘𝐾)))
12	11	simpld 499	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ⟨𝑋, 𝑌⟩ ∈ dom ∨ )
13	1, 2, 3, 5, 6, 7, 8, 12	joinle 18441	1 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑍 ∧ 𝑌 ≤ 𝑍) ↔ (𝑋 ∨ 𝑌) ≤ 𝑍))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1103   = wceq 1570   ∈ wcel 2143  ⟨cop 4596   class class class wbr 5110  dom cdm 5663  ‘cfv 6538  (class class class)co 7412  Basecbs 17270  lecple 17318  Posetcpo 18364  joincjn 18368  meetcmee 18369  Latclat 18488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5239  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7369  df-ov 7415  df-oprab 7416  df-poset 18370  df-lub 18401  df-join 18403  df-lat 18489

This theorem is referenced by:  latleeqj1  18508  latjlej1  18510  latjidm  18519  latledi  18534  latjass  18540  mod1ile  18550  lubun  18572  oldmm1  39972  olj01  39980  cvlexchb1  40085  cvlcvr1  40094  hlrelat  40157  hlrelat2  40158  exatleN  40159  hlrelat3  40167  cvrexchlem  40174  cvratlem  40176  cvrat  40177  atlelt  40193  ps-1  40232  hlatexch3N  40235  hlatexch4  40236  3atlem1  40238  3atlem2  40239  lplnexllnN  40319  2llnjaN  40321  4atlem3  40351  4atlem10  40361  4atlem11b  40363  4atlem11  40364  4atlem12b  40366  4atlem12  40367  2lplnja  40374  dalem1  40414  dalem3  40419  dalem8  40425  dalem16  40434  dalem17  40435  dalem21  40449  dalem25  40453  dalem39  40466  dalem54  40481  dalem60  40487  linepsubN  40507  pmapsub  40523  lneq2at  40533  2llnma3r  40543  cdlema1N  40546  cdlemblem  40548  paddasslem5  40579  paddasslem12  40586  paddasslem13  40587  llnexchb2  40624  dalawlem3  40628  dalawlem5  40630  dalawlem8  40633  dalawlem11  40636  dalawlem12  40637  lhp2lt  40756  lhpexle2lem  40764  lhpexle3lem  40766  4atexlemtlw  40822  4atexlemnclw  40825  lautj  40848  cdlemd3  40955  cdleme3g  40989  cdleme3h  40990  cdleme7d  41001  cdleme11c  41016  cdleme15d  41032  cdleme17b  41042  cdleme19a  41058  cdleme20j  41073  cdleme21c  41082  cdleme22b  41096  cdleme22d  41098  cdleme28a  41125  cdleme35a  41203  cdleme35fnpq  41204  cdleme35b  41205  cdleme35f  41209  cdleme42c  41227  cdleme42i  41238  cdlemf1  41316  cdlemg4c  41367  cdlemg6c  41375  cdlemg8b  41383  cdlemg10  41396  cdlemg11b  41397  cdlemg13a  41406  cdlemg17a  41416  cdlemg18b  41434  cdlemg27a  41447  cdlemg33b0  41456  cdlemg35  41468  cdlemg42  41484  cdlemg46  41490  trljco  41495  tendopltp  41535  cdlemk3  41588  cdlemk10  41598  cdlemk1u  41614  cdlemk39  41671  dialss  41801  dia2dimlem1  41819  dia2dimlem10  41828  dia2dimlem12  41830  cdlemm10N  41873  djajN  41892  diblss  41925  cdlemn2  41950  dihord2pre2  41981  dib2dim  41998  dih2dimb  41999  dih2dimbALTN  42000  dihmeetlem6  42064  dihjatcclem1  42173