Metamath Proof Explorer

Theorem latnlej

Description: An idiom to express that a lattice element differs from two others. (Contributed by NM, 28-May-2012)

Ref Expression
Hypotheses latlej.b ⊢ B = Base K
latlej.l ⊢ ≤ ˙ = ≤ K
latlej.j ⊢ ∨ ˙ = join ⁡ K
Assertion latnlej ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ ¬ X ≤ ˙ Y ∨ ˙ Z → X ≠ Y ∧ X ≠ Z

Proof

Step Hyp Ref Expression
1 latlej.b ⊢ B = Base K
2 latlej.l ⊢ ≤ ˙ = ≤ K
3 latlej.j ⊢ ∨ ˙ = join ⁡ K
4 1 2 3 latlej1 ⊢ K ∈ Lat ∧ Y ∈ B ∧ Z ∈ B → Y ≤ ˙ Y ∨ ˙ Z
5 4 3adant3r1 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → Y ≤ ˙ Y ∨ ˙ Z
6 breq1 ⊢ X = Y → X ≤ ˙ Y ∨ ˙ Z ↔ Y ≤ ˙ Y ∨ ˙ Z
7 5 6 syl5ibrcom ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X = Y → X ≤ ˙ Y ∨ ˙ Z
8 7 necon3bd ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → ¬ X ≤ ˙ Y ∨ ˙ Z → X ≠ Y
9 1 2 3 latlej2 ⊢ K ∈ Lat ∧ Y ∈ B ∧ Z ∈ B → Z ≤ ˙ Y ∨ ˙ Z
10 9 3adant3r1 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → Z ≤ ˙ Y ∨ ˙ Z
11 breq1 ⊢ X = Z → X ≤ ˙ Y ∨ ˙ Z ↔ Z ≤ ˙ Y ∨ ˙ Z
12 10 11 syl5ibrcom ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X = Z → X ≤ ˙ Y ∨ ˙ Z
13 12 necon3bd ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → ¬ X ≤ ˙ Y ∨ ˙ Z → X ≠ Z
14 8 13 jcad ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → ¬ X ≤ ˙ Y ∨ ˙ Z → X ≠ Y ∧ X ≠ Z
15 14 3impia ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ ¬ X ≤ ˙ Y ∨ ˙ Z → X ≠ Y ∧ X ≠ Z