![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > latlej1 | Structured version Visualization version GIF version |
Description: A join's first argument is less than or equal to the join. (chub1 29055 analog.) (Contributed by NM, 17-Sep-2011.) |
Ref | Expression |
---|---|
latlej.b | ⊢ 𝐵 = (Base‘𝐾) |
latlej.l | ⊢ ≤ = (le‘𝐾) |
latlej.j | ⊢ ∨ = (join‘𝐾) |
Ref | Expression |
---|---|
latlej1 | ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ≤ (𝑋 ∨ 𝑌)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | latlej.b | . 2 ⊢ 𝐵 = (Base‘𝐾) | |
2 | latlej.l | . 2 ⊢ ≤ = (le‘𝐾) | |
3 | latlej.j | . 2 ⊢ ∨ = (join‘𝐾) | |
4 | simp1 1116 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝐾 ∈ Lat) | |
5 | simp2 1117 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ∈ 𝐵) | |
6 | simp3 1118 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌 ∈ 𝐵) | |
7 | eqid 2772 | . . . 4 ⊢ (meet‘𝐾) = (meet‘𝐾) | |
8 | 1, 3, 7, 4, 5, 6 | latcl2 17506 | . . 3 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (〈𝑋, 𝑌〉 ∈ dom ∨ ∧ 〈𝑋, 𝑌〉 ∈ dom (meet‘𝐾))) |
9 | 8 | simpld 487 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 〈𝑋, 𝑌〉 ∈ dom ∨ ) |
10 | 1, 2, 3, 4, 5, 6, 9 | lejoin1 17470 | 1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋 ≤ (𝑋 ∨ 𝑌)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1068 = wceq 1507 ∈ wcel 2048 〈cop 4441 class class class wbr 4923 dom cdm 5400 ‘cfv 6182 (class class class)co 6970 Basecbs 16329 lecple 16418 joincjn 17402 meetcmee 17403 Latclat 17503 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-13 2299 ax-ext 2745 ax-rep 5043 ax-sep 5054 ax-nul 5061 ax-pow 5113 ax-pr 5180 ax-un 7273 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2014 df-mo 2544 df-eu 2580 df-clab 2754 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ne 2962 df-ral 3087 df-rex 3088 df-reu 3089 df-rab 3091 df-v 3411 df-sbc 3678 df-csb 3783 df-dif 3828 df-un 3830 df-in 3832 df-ss 3839 df-nul 4174 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-op 4442 df-uni 4707 df-iun 4788 df-br 4924 df-opab 4986 df-mpt 5003 df-id 5305 df-xp 5406 df-rel 5407 df-cnv 5408 df-co 5409 df-dm 5410 df-rn 5411 df-res 5412 df-ima 5413 df-iota 6146 df-fun 6184 df-fn 6185 df-f 6186 df-f1 6187 df-fo 6188 df-f1o 6189 df-fv 6190 df-riota 6931 df-ov 6973 df-oprab 6974 df-lub 17432 df-join 17434 df-lat 17504 |
This theorem is referenced by: latjlej1 17523 latnlej 17526 latnlej2 17529 latjidm 17532 latnle 17543 latabs2 17546 latmlej11 17548 latjass 17553 mod1ile 17563 lubun 17581 oldmm1 35746 olj01 35754 omllaw5N 35776 cvlexchb1 35859 cvlsupr2 35872 cvlsupr7 35877 hlatlej1 35904 hlrelat5N 35930 2atjm 35974 2llnmj 36089 lplnexllnN 36093 2llnjaN 36095 2llnm2N 36097 4atlem3a 36126 2lplnja 36148 2lplnm2N 36150 2lplnmj 36151 dalemply 36183 dalemsly 36184 dalem10 36202 dalem13 36205 dalem21 36223 dalem55 36256 2llnma1b 36315 cdlema1N 36320 elpaddn0 36329 paddasslem12 36360 paddasslem13 36361 pmapjoin 36381 dalawlem2 36401 dalawlem7 36406 dalawlem11 36410 dalawlem12 36411 lhpmcvr3 36554 lhpmcvr5N 36556 lhpmcvr6N 36557 lautj 36622 trljat1 36695 cdlemc1 36720 cdlemc4 36723 cdleme1 36756 cdleme8 36779 cdleme11g 36794 cdleme22e 36873 cdleme22eALTN 36874 cdleme23b 36879 cdleme23c 36880 cdleme27N 36898 cdleme30a 36907 cdleme35fnpq 36978 cdleme35b 36979 cdleme35c 36980 cdleme42h 37011 cdleme42i 37012 cdleme48bw 37031 cdlemg2fv2 37129 cdlemg7fvbwN 37136 cdlemg8b 37157 cdlemg11b 37171 trlcolem 37255 trljco 37269 cdlemi1 37347 cdlemk48 37479 cdlemn2 37724 dihjustlem 37745 dihord1 37747 dihord5apre 37791 dihglbcpreN 37829 dihmeetlem3N 37834 dihmeetlem11N 37846 |
Copyright terms: Public domain | W3C validator |