Theorem latjle12 17675

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 29289 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 17663	. . 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 2824	. . . 4 ⊢ (meet‘𝐾) = (meet‘𝐾)
10		simpl 485	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Lat)
11	1, 3, 9, 10, 6, 7	latcl2 17661	. . 3 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (⟨𝑋, 𝑌⟩ ∈ dom ∨ ∧ ⟨𝑋, 𝑌⟩ ∈ dom (meet‘𝐾)))
12	11	simpld 497	. 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ⟨𝑋, 𝑌⟩ ∈ dom ∨ )
13	1, 2, 3, 5, 6, 7, 8, 12	joinle 17627	1 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑍 ∧ 𝑌 ≤ 𝑍) ↔ (𝑋 ∨ 𝑌) ≤ 𝑍))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083   = wceq 1536   ∈ wcel 2113  ⟨cop 4576   class class class wbr 5069  dom cdm 5558  ‘cfv 6358  (class class class)co 7159  Basecbs 16486  lecple 16575  Posetcpo 17553  joincjn 17557  meetcmee 17558  Latclat 17658

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-rep 5193  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333  ax-un 7464

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-ral 3146  df-rex 3147  df-reu 3148  df-rab 3150  df-v 3499  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-pw 4544  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-iun 4924  df-br 5070  df-opab 5132  df-mpt 5150  df-id 5463  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571  df-iota 6317  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-riota 7117  df-ov 7162  df-oprab 7163  df-poset 17559  df-lub 17587  df-join 17589  df-lat 17659

This theorem is referenced by:  latleeqj1  17676  latjlej1  17678  latjidm  17687  latledi  17702  latjass  17708  mod1ile  17718  lubun  17736  oldmm1  36357  olj01  36365  cvlexchb1  36470  cvlcvr1  36479  hlrelat  36542  hlrelat2  36543  exatleN  36544  hlrelat3  36552  cvrexchlem  36559  cvratlem  36561  cvrat  36562  atlelt  36578  ps-1  36617  hlatexch3N  36620  hlatexch4  36621  3atlem1  36623  3atlem2  36624  lplnexllnN  36704  2llnjaN  36706  4atlem3  36736  4atlem10  36746  4atlem11b  36748  4atlem11  36749  4atlem12b  36751  4atlem12  36752  2lplnja  36759  dalem1  36799  dalem3  36804  dalem8  36810  dalem16  36819  dalem17  36820  dalem21  36834  dalem25  36838  dalem39  36851  dalem54  36866  dalem60  36872  linepsubN  36892  pmapsub  36908  lneq2at  36918  2llnma3r  36928  cdlema1N  36931  cdlemblem  36933  paddasslem5  36964  paddasslem12  36971  paddasslem13  36972  llnexchb2  37009  dalawlem3  37013  dalawlem5  37015  dalawlem8  37018  dalawlem11  37021  dalawlem12  37022  lhp2lt  37141  lhpexle2lem  37149  lhpexle3lem  37151  4atexlemtlw  37207  4atexlemnclw  37210  lautj  37233  cdlemd3  37340  cdleme3g  37374  cdleme3h  37375  cdleme7d  37386  cdleme11c  37401  cdleme15d  37417  cdleme17b  37427  cdleme19a  37443  cdleme20j  37458  cdleme21c  37467  cdleme22b  37481  cdleme22d  37483  cdleme28a  37510  cdleme35a  37588  cdleme35fnpq  37589  cdleme35b  37590  cdleme35f  37594  cdleme42c  37612  cdleme42i  37623  cdlemf1  37701  cdlemg4c  37752  cdlemg6c  37760  cdlemg8b  37768  cdlemg10  37781  cdlemg11b  37782  cdlemg13a  37791  cdlemg17a  37801  cdlemg18b  37819  cdlemg27a  37832  cdlemg33b0  37841  cdlemg35  37853  cdlemg42  37869  cdlemg46  37875  trljco  37880  tendopltp  37920  cdlemk3  37973  cdlemk10  37983  cdlemk1u  37999  cdlemk39  38056  dialss  38186  dia2dimlem1  38204  dia2dimlem10  38213  dia2dimlem12  38215  cdlemm10N  38258  djajN  38277  diblss  38310  cdlemn2  38335  dihord2pre2  38366  dib2dim  38383  dih2dimb  38384  dih2dimbALTN  38385  dihmeetlem6  38449  dihjatcclem1  38558