Metamath Proof Explorer

Theorem latnlej2

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

Ref Expression
Hypotheses latlej.b ⊢ B = Base K
latlej.l ⊢ ≤ ˙ = ≤ K
latlej.j ⊢ ∨ ˙ = join ⁡ K
Assertion latnlej2 ⊢ 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 simpl ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → K ∈ Lat
7 simpr1 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∈ B
8 simpr2 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → Y ∈ B
9 1 3 latjcl ⊢ K ∈ Lat ∧ Y ∈ B ∧ Z ∈ B → Y ∨ ˙ Z ∈ B
10 9 3adant3r1 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → Y ∨ ˙ Z ∈ B
11 1 2 lattr ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Y ∨ ˙ Z ∈ B → X ≤ ˙ Y ∧ Y ≤ ˙ Y ∨ ˙ Z → X ≤ ˙ Y ∨ ˙ Z
12 6 7 8 10 11 syl13anc ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ≤ ˙ Y ∧ Y ≤ ˙ Y ∨ ˙ Z → X ≤ ˙ Y ∨ ˙ Z
13 5 12 mpan2d ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ≤ ˙ Y → X ≤ ˙ Y ∨ ˙ Z
14 13 con3d ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → ¬ X ≤ ˙ Y ∨ ˙ Z → ¬ X ≤ ˙ Y
15 1 2 3 latlej2 ⊢ K ∈ Lat ∧ Y ∈ B ∧ Z ∈ B → Z ≤ ˙ Y ∨ ˙ Z
16 15 3adant3r1 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → Z ≤ ˙ Y ∨ ˙ Z
17 simpr3 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → Z ∈ B
18 1 2 lattr ⊢ K ∈ Lat ∧ X ∈ B ∧ Z ∈ B ∧ Y ∨ ˙ Z ∈ B → X ≤ ˙ Z ∧ Z ≤ ˙ Y ∨ ˙ Z → X ≤ ˙ Y ∨ ˙ Z
19 6 7 17 10 18 syl13anc ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ≤ ˙ Z ∧ Z ≤ ˙ Y ∨ ˙ Z → X ≤ ˙ Y ∨ ˙ Z
20 16 19 mpan2d ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ≤ ˙ Z → X ≤ ˙ Y ∨ ˙ Z
21 20 con3d ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → ¬ X ≤ ˙ Y ∨ ˙ Z → ¬ X ≤ ˙ Z
22 14 21 jcad ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → ¬ X ≤ ˙ Y ∨ ˙ Z → ¬ X ≤ ˙ Y ∧ ¬ X ≤ ˙ Z
23 22 3impia ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ ¬ X ≤ ˙ Y ∨ ˙ Z → ¬ X ≤ ˙ Y ∧ ¬ X ≤ ˙ Z