Metamath Proof Explorer

Theorem latlem

Description: Lemma for lattice properties. (Contributed by NM, 14-Sep-2011)

Ref Expression
Hypotheses latlem.b ⊢ B = Base K
latlem.j ⊢ ∨ ˙ = join ⁡ K
latlem.m ⊢ ∧ ˙ = meet ⁡ K
Assertion latlem ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → X ∨ ˙ Y ∈ B ∧ X ∧ ˙ Y ∈ B

Proof

Step Hyp Ref Expression
1 latlem.b ⊢ B = Base K
2 latlem.j ⊢ ∨ ˙ = join ⁡ K
3 latlem.m ⊢ ∧ ˙ = meet ⁡ K
4 simp1 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → K ∈ Lat
5 simp2 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → X ∈ B
6 simp3 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → Y ∈ B
7 opelxpi ⊢ X ∈ B ∧ Y ∈ B → X Y ∈ B × B
8 7 3adant1 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → X Y ∈ B × B
9 1 2 3 islat ⊢ K ∈ Lat ↔ K ∈ Poset ∧ dom ⁡ ∨ ˙ = B × B ∧ dom ⁡ ∧ ˙ = B × B
10 simprl ⊢ K ∈ Poset ∧ dom ⁡ ∨ ˙ = B × B ∧ dom ⁡ ∧ ˙ = B × B → dom ⁡ ∨ ˙ = B × B
11 9 10 sylbi ⊢ K ∈ Lat → dom ⁡ ∨ ˙ = B × B
12 11 3ad2ant1 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → dom ⁡ ∨ ˙ = B × B
13 8 12 eleqtrrd ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → X Y ∈ dom ⁡ ∨ ˙
14 1 2 4 5 6 13 joincl ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → X ∨ ˙ Y ∈ B
15 simprr ⊢ K ∈ Poset ∧ dom ⁡ ∨ ˙ = B × B ∧ dom ⁡ ∧ ˙ = B × B → dom ⁡ ∧ ˙ = B × B
16 9 15 sylbi ⊢ K ∈ Lat → dom ⁡ ∧ ˙ = B × B
17 16 3ad2ant1 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → dom ⁡ ∧ ˙ = B × B
18 8 17 eleqtrrd ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → X Y ∈ dom ⁡ ∧ ˙
19 1 3 4 5 6 18 meetcl ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → X ∧ ˙ Y ∈ B
20 14 19 jca ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B → X ∨ ˙ Y ∈ B ∧ X ∧ ˙ Y ∈ B