![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > latjcom | Structured version Visualization version GIF version |
Description: The join of a lattice commutes. (chjcom 30737 analog.) (Contributed by NM, 16-Sep-2011.) |
Ref | Expression |
---|---|
latjcom.b | ⊢ 𝐵 = (Base‘𝐾) |
latjcom.j | ⊢ ∨ = (join‘𝐾) |
Ref | Expression |
---|---|
latjcom | ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opelxpi 5712 | . . . . 5 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 〈𝑋, 𝑌〉 ∈ (𝐵 × 𝐵)) | |
2 | 1 | 3adant1 1131 | . . . 4 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 〈𝑋, 𝑌〉 ∈ (𝐵 × 𝐵)) |
3 | latjcom.b | . . . . . . 7 ⊢ 𝐵 = (Base‘𝐾) | |
4 | latjcom.j | . . . . . . 7 ⊢ ∨ = (join‘𝐾) | |
5 | eqid 2733 | . . . . . . 7 ⊢ (meet‘𝐾) = (meet‘𝐾) | |
6 | 3, 4, 5 | islat 18382 | . . . . . 6 ⊢ (𝐾 ∈ Lat ↔ (𝐾 ∈ Poset ∧ (dom ∨ = (𝐵 × 𝐵) ∧ dom (meet‘𝐾) = (𝐵 × 𝐵)))) |
7 | simprl 770 | . . . . . 6 ⊢ ((𝐾 ∈ Poset ∧ (dom ∨ = (𝐵 × 𝐵) ∧ dom (meet‘𝐾) = (𝐵 × 𝐵))) → dom ∨ = (𝐵 × 𝐵)) | |
8 | 6, 7 | sylbi 216 | . . . . 5 ⊢ (𝐾 ∈ Lat → dom ∨ = (𝐵 × 𝐵)) |
9 | 8 | 3ad2ant1 1134 | . . . 4 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → dom ∨ = (𝐵 × 𝐵)) |
10 | 2, 9 | eleqtrrd 2837 | . . 3 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 〈𝑋, 𝑌〉 ∈ dom ∨ ) |
11 | opelxpi 5712 | . . . . . 6 ⊢ ((𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → 〈𝑌, 𝑋〉 ∈ (𝐵 × 𝐵)) | |
12 | 11 | ancoms 460 | . . . . 5 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 〈𝑌, 𝑋〉 ∈ (𝐵 × 𝐵)) |
13 | 12 | 3adant1 1131 | . . . 4 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 〈𝑌, 𝑋〉 ∈ (𝐵 × 𝐵)) |
14 | 13, 9 | eleqtrrd 2837 | . . 3 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 〈𝑌, 𝑋〉 ∈ dom ∨ ) |
15 | 10, 14 | jca 513 | . 2 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (〈𝑋, 𝑌〉 ∈ dom ∨ ∧ 〈𝑌, 𝑋〉 ∈ dom ∨ )) |
16 | latpos 18387 | . . 3 ⊢ (𝐾 ∈ Lat → 𝐾 ∈ Poset) | |
17 | 3, 4 | joincom 18351 | . . 3 ⊢ (((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (〈𝑋, 𝑌〉 ∈ dom ∨ ∧ 〈𝑌, 𝑋〉 ∈ dom ∨ )) → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋)) |
18 | 16, 17 | syl3anl1 1413 | . 2 ⊢ (((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (〈𝑋, 𝑌〉 ∈ dom ∨ ∧ 〈𝑌, 𝑋〉 ∈ dom ∨ )) → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋)) |
19 | 15, 18 | mpdan 686 | 1 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∧ w3a 1088 = wceq 1542 ∈ wcel 2107 〈cop 4633 × cxp 5673 dom cdm 5675 ‘cfv 6540 (class class class)co 7404 Basecbs 17140 Posetcpo 18256 joincjn 18260 meetcmee 18261 Latclat 18380 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7720 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5573 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7360 df-ov 7407 df-oprab 7408 df-lub 18295 df-join 18297 df-lat 18381 |
This theorem is referenced by: latleeqj2 18401 latjlej2 18403 latnle 18422 latmlej12 18428 latj12 18433 latj32 18434 latj13 18435 latj31 18436 latj4rot 18439 mod2ile 18443 latdisdlem 18445 olj02 38034 omllaw4 38054 cmt2N 38058 cmtbr3N 38062 cvlexch2 38137 cvlexchb2 38139 cvlatexchb2 38143 cvlatexch2 38145 cvlatexch3 38146 cvlatcvr2 38150 cvlsupr2 38151 cvlsupr7 38156 cvlsupr8 38157 hlatjcom 38176 hlrelat5N 38210 cvrval5 38224 cvrexch 38229 cvratlem 38230 cvrat 38231 2atlt 38248 cvrat3 38251 cvrat4 38252 cvrat42 38253 4noncolr3 38262 1cvrat 38285 3atlem1 38292 4atlem4d 38411 4atlem12 38421 paddcom 38622 paddasslem2 38630 pmapjat2 38663 atmod2i1 38670 atmod2i2 38671 llnmod2i2 38672 atmod4i1 38675 atmod4i2 38676 dalawlem4 38683 dalawlem9 38688 dalawlem12 38691 lhpjat2 38830 lhple 38851 trljat1 38975 trljat2 38976 cdlemc1 39000 cdlemc6 39005 cdlemd1 39007 cdleme5 39049 cdleme9 39062 cdleme10 39063 cdleme19e 39116 trlcolem 39535 trljco2 39550 cdlemk7 39657 cdlemk7u 39679 cdlemkid1 39731 dih1 40095 dihjatc2N 40121 |
Copyright terms: Public domain | W3C validator |