Theorem latjle12 18544

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 31998 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 18532	. . 3 ⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset)
5	4	adantr 486	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Poset)
6		simpr1 1213	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑋 ∈ 𝐵)
7		simpr2 1214	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌 ∈ 𝐵)
8		simpr3 1215	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍 ∈ 𝐵)
9		eqid 2762	. . . 4 ⊢ (meet‘𝐾) = (meet‘𝐾)
10		simpl 488	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Lat)
11	1, 3, 9, 10, 6, 7	latcl2 18530	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (⟨𝑋, 𝑌⟩ ∈ dom ∨ ∧ ⟨𝑋, 𝑌⟩ ∈ dom (meet‘𝐾)))
12	11	simpld 500	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ⟨𝑋, 𝑌⟩ ∈ dom ∨ )
13	1, 2, 3, 5, 6, 7, 8, 12	joinle 18478	1 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑍 ∧ 𝑌 ≤ 𝑍) ↔ (𝑋 ∨ 𝑌) ≤ 𝑍))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ⟨cop 4593   class class class wbr 5107  dom cdm 5659  ‘cfv 6537  (class class class)co 7417  Basecbs 17307  lecple 17355  Posetcpo 18401  joincjn 18405  meetcmee 18406  Latclat 18525

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-rep 5236  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7374  df-ov 7420  df-oprab 7421  df-poset 18407  df-lub 18438  df-join 18440  df-lat 18526

This theorem is used by:  latleeqj1  18545  latjlej1  18547  latjidm  18556  latledi  18571  latjass  18577  mod1ile  18587  lubun  18609  oldmm1  40098  olj01  40106  cvlexchb1  40211  cvlcvr1  40220  hlrelat  40283  hlrelat2  40284  exatleN  40285  hlrelat3  40293  cvrexchlem  40300  cvratlem  40302  cvrat  40303  atlelt  40319  ps-1  40358  hlatexch3N  40361  hlatexch4  40362  3atlem1  40364  3atlem2  40365  lplnexllnN  40445  2llnjaN  40447  4atlem3  40477  4atlem10  40487  4atlem11b  40489  4atlem11  40490  4atlem12b  40492  4atlem12  40493  2lplnja  40500  dalem1  40540  dalem3  40545  dalem8  40551  dalem16  40560  dalem17  40561  dalem21  40575  dalem25  40579  dalem39  40592  dalem54  40607  dalem60  40613  linepsubN  40633  pmapsub  40649  lneq2at  40659  2llnma3r  40669  cdlema1N  40672  cdlemblem  40674  paddasslem5  40705  paddasslem12  40712  paddasslem13  40713  llnexchb2  40750  dalawlem3  40754  dalawlem5  40756  dalawlem8  40759  dalawlem11  40762  dalawlem12  40763  lhp2lt  40882  lhpexle2lem  40890  lhpexle3lem  40892  4atexlemtlw  40948  4atexlemnclw  40951  lautj  40974  cdlemd3  41081  cdleme3g  41115  cdleme3h  41116  cdleme7d  41127  cdleme11c  41142  cdleme15d  41158  cdleme17b  41168  cdleme19a  41184  cdleme20j  41199  cdleme21c  41208  cdleme22b  41222  cdleme22d  41224  cdleme28a  41251  cdleme35a  41329  cdleme35fnpq  41330  cdleme35b  41331  cdleme35f  41335  cdleme42c  41353  cdleme42i  41364  cdlemf1  41442  cdlemg4c  41493  cdlemg6c  41501  cdlemg8b  41509  cdlemg10  41522  cdlemg11b  41523  cdlemg13a  41532  cdlemg17a  41542  cdlemg18b  41560  cdlemg27a  41573  cdlemg33b0  41582  cdlemg35  41594  cdlemg42  41610  cdlemg46  41616  trljco  41621  tendopltp  41661  cdlemk3  41714  cdlemk10  41724  cdlemk1u  41740  cdlemk39  41797  dialss  41927  dia2dimlem1  41945  dia2dimlem10  41954  dia2dimlem12  41956  cdlemm10N  41999  djajN  42018  diblss  42051  cdlemn2  42076  dihord2pre2  42107  dib2dim  42124  dih2dimb  42125  dih2dimbALTN  42126  dihmeetlem6  42190  dihjatcclem1  42299