| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > latnlej1l | Structured version Visualization version GIF version | ||
| Description: An idiom to express that a lattice element differs from two others. (Contributed by NM, 19-Jul-2012.) |
| Ref | Expression |
|---|---|
| latlej.b | ⊢ 𝐵 = (Base‘𝐾) |
| latlej.l | ⊢ ≤ = (le‘𝐾) |
| latlej.j | ⊢ ∨ = (join‘𝐾) |
| Ref | Expression |
|---|---|
| latnlej1l | ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ ¬ 𝑋 ≤ (𝑌 ∨ 𝑍)) → 𝑋 ≠ 𝑌) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | latlej.b | . . 3 ⊢ 𝐵 = (Base‘𝐾) | |
| 2 | latlej.l | . . 3 ⊢ ≤ = (le‘𝐾) | |
| 3 | latlej.j | . . 3 ⊢ ∨ = (join‘𝐾) | |
| 4 | 1, 2, 3 | latnlej 18411 | . 2 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ ¬ 𝑋 ≤ (𝑌 ∨ 𝑍)) → (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍)) |
| 5 | 4 | simpld 494 | 1 ⊢ ((𝐾 ∈ Lat ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ ¬ 𝑋 ≤ (𝑌 ∨ 𝑍)) → 𝑋 ≠ 𝑌) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 class class class wbr 5086 ‘cfv 6490 (class class class)co 7358 Basecbs 17168 lecple 17216 joincjn 18266 Latclat 18386 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5300 ax-pr 5368 ax-un 7680 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-id 5517 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-rn 5633 df-res 5634 df-ima 5635 df-iota 6446 df-fun 6492 df-fn 6493 df-f 6494 df-f1 6495 df-fo 6496 df-f1o 6497 df-fv 6498 df-riota 7315 df-ov 7361 df-oprab 7362 df-lub 18299 df-join 18301 df-lat 18387 |
| This theorem is referenced by: atnlej1 39836 3atlem4 39943 3atlem6 39945 dalemcnes 40107 lhpexle3lem 40468 cdlemd4 40658 cdlemd7 40661 cdleme0e 40674 cdleme3e 40689 cdleme9 40710 cdleme17c 40745 |
| Copyright terms: Public domain | W3C validator |