Proof of Theorem latjass
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | latjass.b | . 2
⊢ 𝐵 = (Base‘𝐾) | 
| 2 |  | eqid 2736 | . 2
⊢
(le‘𝐾) =
(le‘𝐾) | 
| 3 |  | simpl 482 | . 2
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝐾 ∈ Lat) | 
| 4 |  | latjass.j | . . . . 5
⊢  ∨ =
(join‘𝐾) | 
| 5 | 1, 4 | latjcl 18485 | . . . 4
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ 𝑌) ∈ 𝐵) | 
| 6 | 5 | 3adant3r3 1184 | . . 3
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∨ 𝑌) ∈ 𝐵) | 
| 7 |  | simpr3 1196 | . . 3
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍 ∈ 𝐵) | 
| 8 | 1, 4 | latjcl 18485 | . . 3
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∨ 𝑌) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 ∨ 𝑌) ∨ 𝑍) ∈ 𝐵) | 
| 9 | 3, 6, 7, 8 | syl3anc 1372 | . 2
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∨ 𝑌) ∨ 𝑍) ∈ 𝐵) | 
| 10 |  | simpr1 1194 | . . 3
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑋 ∈ 𝐵) | 
| 11 | 1, 4 | latjcl 18485 | . . . 4
⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑌 ∨ 𝑍) ∈ 𝐵) | 
| 12 | 11 | 3adant3r1 1182 | . . 3
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 ∨ 𝑍) ∈ 𝐵) | 
| 13 | 1, 4 | latjcl 18485 | . . 3
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ (𝑌 ∨ 𝑍) ∈ 𝐵) → (𝑋 ∨ (𝑌 ∨ 𝑍)) ∈ 𝐵) | 
| 14 | 3, 10, 12, 13 | syl3anc 1372 | . 2
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∨ (𝑌 ∨ 𝑍)) ∈ 𝐵) | 
| 15 | 1, 2, 4 | latlej1 18494 | . . . . 5
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ (𝑌 ∨ 𝑍) ∈ 𝐵) → 𝑋(le‘𝐾)(𝑋 ∨ (𝑌 ∨ 𝑍))) | 
| 16 | 3, 10, 12, 15 | syl3anc 1372 | . . . 4
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑋(le‘𝐾)(𝑋 ∨ (𝑌 ∨ 𝑍))) | 
| 17 |  | simpr2 1195 | . . . . 5
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌 ∈ 𝐵) | 
| 18 | 1, 2, 4 | latlej1 18494 | . . . . . 6
⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → 𝑌(le‘𝐾)(𝑌 ∨ 𝑍)) | 
| 19 | 18 | 3adant3r1 1182 | . . . . 5
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌(le‘𝐾)(𝑌 ∨ 𝑍)) | 
| 20 | 1, 2, 4 | latlej2 18495 | . . . . . 6
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ (𝑌 ∨ 𝑍) ∈ 𝐵) → (𝑌 ∨ 𝑍)(le‘𝐾)(𝑋 ∨ (𝑌 ∨ 𝑍))) | 
| 21 | 3, 10, 12, 20 | syl3anc 1372 | . . . . 5
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 ∨ 𝑍)(le‘𝐾)(𝑋 ∨ (𝑌 ∨ 𝑍))) | 
| 22 | 1, 2, 3, 17, 12, 14, 19, 21 | lattrd 18492 | . . . 4
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌(le‘𝐾)(𝑋 ∨ (𝑌 ∨ 𝑍))) | 
| 23 | 1, 2, 4 | latjle12 18496 | . . . . 5
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 ∨ (𝑌 ∨ 𝑍)) ∈ 𝐵)) → ((𝑋(le‘𝐾)(𝑋 ∨ (𝑌 ∨ 𝑍)) ∧ 𝑌(le‘𝐾)(𝑋 ∨ (𝑌 ∨ 𝑍))) ↔ (𝑋 ∨ 𝑌)(le‘𝐾)(𝑋 ∨ (𝑌 ∨ 𝑍)))) | 
| 24 | 3, 10, 17, 14, 23 | syl13anc 1373 | . . . 4
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋(le‘𝐾)(𝑋 ∨ (𝑌 ∨ 𝑍)) ∧ 𝑌(le‘𝐾)(𝑋 ∨ (𝑌 ∨ 𝑍))) ↔ (𝑋 ∨ 𝑌)(le‘𝐾)(𝑋 ∨ (𝑌 ∨ 𝑍)))) | 
| 25 | 16, 22, 24 | mpbi2and 712 | . . 3
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∨ 𝑌)(le‘𝐾)(𝑋 ∨ (𝑌 ∨ 𝑍))) | 
| 26 | 1, 2, 4 | latlej2 18495 | . . . . 5
⊢ ((𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → 𝑍(le‘𝐾)(𝑌 ∨ 𝑍)) | 
| 27 | 26 | 3adant3r1 1182 | . . . 4
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍(le‘𝐾)(𝑌 ∨ 𝑍)) | 
| 28 | 1, 2, 3, 7, 12, 14, 27, 21 | lattrd 18492 | . . 3
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍(le‘𝐾)(𝑋 ∨ (𝑌 ∨ 𝑍))) | 
| 29 | 1, 2, 4 | latjle12 18496 | . . . 4
⊢ ((𝐾 ∈ Lat ∧ ((𝑋 ∨ 𝑌) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ (𝑋 ∨ (𝑌 ∨ 𝑍)) ∈ 𝐵)) → (((𝑋 ∨ 𝑌)(le‘𝐾)(𝑋 ∨ (𝑌 ∨ 𝑍)) ∧ 𝑍(le‘𝐾)(𝑋 ∨ (𝑌 ∨ 𝑍))) ↔ ((𝑋 ∨ 𝑌) ∨ 𝑍)(le‘𝐾)(𝑋 ∨ (𝑌 ∨ 𝑍)))) | 
| 30 | 3, 6, 7, 14, 29 | syl13anc 1373 | . . 3
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (((𝑋 ∨ 𝑌)(le‘𝐾)(𝑋 ∨ (𝑌 ∨ 𝑍)) ∧ 𝑍(le‘𝐾)(𝑋 ∨ (𝑌 ∨ 𝑍))) ↔ ((𝑋 ∨ 𝑌) ∨ 𝑍)(le‘𝐾)(𝑋 ∨ (𝑌 ∨ 𝑍)))) | 
| 31 | 25, 28, 30 | mpbi2and 712 | . 2
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∨ 𝑌) ∨ 𝑍)(le‘𝐾)(𝑋 ∨ (𝑌 ∨ 𝑍))) | 
| 32 | 1, 2, 4 | latlej1 18494 | . . . . 5
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑋(le‘𝐾)(𝑋 ∨ 𝑌)) | 
| 33 | 32 | 3adant3r3 1184 | . . . 4
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑋(le‘𝐾)(𝑋 ∨ 𝑌)) | 
| 34 | 1, 2, 4 | latlej1 18494 | . . . . 5
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∨ 𝑌) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝑋 ∨ 𝑌)(le‘𝐾)((𝑋 ∨ 𝑌) ∨ 𝑍)) | 
| 35 | 3, 6, 7, 34 | syl3anc 1372 | . . . 4
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∨ 𝑌)(le‘𝐾)((𝑋 ∨ 𝑌) ∨ 𝑍)) | 
| 36 | 1, 2, 3, 10, 6, 9,
33, 35 | lattrd 18492 | . . 3
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑋(le‘𝐾)((𝑋 ∨ 𝑌) ∨ 𝑍)) | 
| 37 | 1, 2, 4 | latlej2 18495 | . . . . . 6
⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → 𝑌(le‘𝐾)(𝑋 ∨ 𝑌)) | 
| 38 | 37 | 3adant3r3 1184 | . . . . 5
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌(le‘𝐾)(𝑋 ∨ 𝑌)) | 
| 39 | 1, 2, 3, 17, 6, 9,
38, 35 | lattrd 18492 | . . . 4
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑌(le‘𝐾)((𝑋 ∨ 𝑌) ∨ 𝑍)) | 
| 40 | 1, 2, 4 | latlej2 18495 | . . . . 5
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∨ 𝑌) ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → 𝑍(le‘𝐾)((𝑋 ∨ 𝑌) ∨ 𝑍)) | 
| 41 | 3, 6, 7, 40 | syl3anc 1372 | . . . 4
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → 𝑍(le‘𝐾)((𝑋 ∨ 𝑌) ∨ 𝑍)) | 
| 42 | 1, 2, 4 | latjle12 18496 | . . . . 5
⊢ ((𝐾 ∈ Lat ∧ (𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ∧ ((𝑋 ∨ 𝑌) ∨ 𝑍) ∈ 𝐵)) → ((𝑌(le‘𝐾)((𝑋 ∨ 𝑌) ∨ 𝑍) ∧ 𝑍(le‘𝐾)((𝑋 ∨ 𝑌) ∨ 𝑍)) ↔ (𝑌 ∨ 𝑍)(le‘𝐾)((𝑋 ∨ 𝑌) ∨ 𝑍))) | 
| 43 | 3, 17, 7, 9, 42 | syl13anc 1373 | . . . 4
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑌(le‘𝐾)((𝑋 ∨ 𝑌) ∨ 𝑍) ∧ 𝑍(le‘𝐾)((𝑋 ∨ 𝑌) ∨ 𝑍)) ↔ (𝑌 ∨ 𝑍)(le‘𝐾)((𝑋 ∨ 𝑌) ∨ 𝑍))) | 
| 44 | 39, 41, 43 | mpbi2and 712 | . . 3
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑌 ∨ 𝑍)(le‘𝐾)((𝑋 ∨ 𝑌) ∨ 𝑍)) | 
| 45 | 1, 2, 4 | latjle12 18496 | . . . 4
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ (𝑌 ∨ 𝑍) ∈ 𝐵 ∧ ((𝑋 ∨ 𝑌) ∨ 𝑍) ∈ 𝐵)) → ((𝑋(le‘𝐾)((𝑋 ∨ 𝑌) ∨ 𝑍) ∧ (𝑌 ∨ 𝑍)(le‘𝐾)((𝑋 ∨ 𝑌) ∨ 𝑍)) ↔ (𝑋 ∨ (𝑌 ∨ 𝑍))(le‘𝐾)((𝑋 ∨ 𝑌) ∨ 𝑍))) | 
| 46 | 3, 10, 12, 9, 45 | syl13anc 1373 | . . 3
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋(le‘𝐾)((𝑋 ∨ 𝑌) ∨ 𝑍) ∧ (𝑌 ∨ 𝑍)(le‘𝐾)((𝑋 ∨ 𝑌) ∨ 𝑍)) ↔ (𝑋 ∨ (𝑌 ∨ 𝑍))(le‘𝐾)((𝑋 ∨ 𝑌) ∨ 𝑍))) | 
| 47 | 36, 44, 46 | mpbi2and 712 | . 2
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∨ (𝑌 ∨ 𝑍))(le‘𝐾)((𝑋 ∨ 𝑌) ∨ 𝑍)) | 
| 48 | 1, 2, 3, 9, 14, 31, 47 | latasymd 18491 | 1
⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∨ 𝑌) ∨ 𝑍) = (𝑋 ∨ (𝑌 ∨ 𝑍))) |