Theorem latjle12 18472

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 31668 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 18460	. . 3 ⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset)
5	4	adantr 484	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Poset)
6		simpr1 1207	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑋 ∈ 𝐵)
7		simpr2 1208	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌 ∈ 𝐵)
8		simpr3 1209	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍 ∈ 𝐵)
9		eqid 2761	. . . 4 ⊢ (meet‘𝐾) = (meet‘𝐾)
10		simpl 486	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Lat)
11	1, 3, 9, 10, 6, 7	latcl2 18458	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (⟨𝑋, 𝑌⟩ ∈ dom ∨ ∧ ⟨𝑋, 𝑌⟩ ∈ dom (meet‘𝐾)))
12	11	simpld 498	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ⟨𝑋, 𝑌⟩ ∈ dom ∨ )
13	1, 2, 3, 5, 6, 7, 8, 12	joinle 18406	1 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑍 ∧ 𝑌 ≤ 𝑍) ↔ (𝑋 ∨ 𝑌) ≤ 𝑍))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   ∧ w3a 1097   = wceq 1559   ∈ wcel 2141  ⟨cop 4585   class class class wbr 5097  dom cdm 5643  ‘cfv 6515  (class class class)co 7390  Basecbs 17235  lecple 17283  Posetcpo 18329  joincjn 18333  meetcmee 18334  Latclat 18453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-rep 5224  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7712

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-iota 6471  df-fun 6517  df-fn 6518  df-f 6519  df-f1 6520  df-fo 6521  df-f1o 6522  df-fv 6523  df-riota 7347  df-ov 7393  df-oprab 7394  df-poset 18335  df-lub 18366  df-join 18368  df-lat 18454

This theorem is referenced by:  latleeqj1  18473  latjlej1  18475  latjidm  18484  latledi  18499  latjass  18505  mod1ile  18515  lubun  18537  oldmm1  39801  olj01  39809  cvlexchb1  39914  cvlcvr1  39923  hlrelat  39986  hlrelat2  39987  exatleN  39988  hlrelat3  39996  cvrexchlem  40003  cvratlem  40005  cvrat  40006  atlelt  40022  ps-1  40061  hlatexch3N  40064  hlatexch4  40065  3atlem1  40067  3atlem2  40068  lplnexllnN  40148  2llnjaN  40150  4atlem3  40180  4atlem10  40190  4atlem11b  40192  4atlem11  40193  4atlem12b  40195  4atlem12  40196  2lplnja  40203  dalem1  40243  dalem3  40248  dalem8  40254  dalem16  40263  dalem17  40264  dalem21  40278  dalem25  40282  dalem39  40295  dalem54  40310  dalem60  40316  linepsubN  40336  pmapsub  40352  lneq2at  40362  2llnma3r  40372  cdlema1N  40375  cdlemblem  40377  paddasslem5  40408  paddasslem12  40415  paddasslem13  40416  llnexchb2  40453  dalawlem3  40457  dalawlem5  40459  dalawlem8  40462  dalawlem11  40465  dalawlem12  40466  lhp2lt  40585  lhpexle2lem  40593  lhpexle3lem  40595  4atexlemtlw  40651  4atexlemnclw  40654  lautj  40677  cdlemd3  40784  cdleme3g  40818  cdleme3h  40819  cdleme7d  40830  cdleme11c  40845  cdleme15d  40861  cdleme17b  40871  cdleme19a  40887  cdleme20j  40902  cdleme21c  40911  cdleme22b  40925  cdleme22d  40927  cdleme28a  40954  cdleme35a  41032  cdleme35fnpq  41033  cdleme35b  41034  cdleme35f  41038  cdleme42c  41056  cdleme42i  41067  cdlemf1  41145  cdlemg4c  41196  cdlemg6c  41204  cdlemg8b  41212  cdlemg10  41225  cdlemg11b  41226  cdlemg13a  41235  cdlemg17a  41245  cdlemg18b  41263  cdlemg27a  41276  cdlemg33b0  41285  cdlemg35  41297  cdlemg42  41313  cdlemg46  41319  trljco  41324  tendopltp  41364  cdlemk3  41417  cdlemk10  41427  cdlemk1u  41443  cdlemk39  41500  dialss  41630  dia2dimlem1  41648  dia2dimlem10  41657  dia2dimlem12  41659  cdlemm10N  41702  djajN  41721  diblss  41754  cdlemn2  41779  dihord2pre2  41810  dib2dim  41827  dih2dimb  41828  dih2dimbALTN  41829  dihmeetlem6  41893  dihjatcclem1  42002