This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem latlem12

Description: An element is less than or equal to a meet iff the element is less than or equal to each argument of the meet. (Contributed by NM, 21-Oct-2011)

Ref Expression
Hypotheses latmle.b ⊢ B = Base K
latmle.l ⊢ ≤ ˙ = ≤ K
latmle.m ⊢ ∧ ˙ = meet ⁡ K
Assertion latlem12 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ≤ ˙ Y ∧ X ≤ ˙ Z ↔ X ≤ ˙ Y ∧ ˙ Z

Proof

Step Hyp Ref Expression
1 latmle.b ⊢ B = Base K
2 latmle.l ⊢ ≤ ˙ = ≤ K
3 latmle.m ⊢ ∧ ˙ = meet ⁡ K
4 latpos ⊢ K ∈ Lat → K ∈ Poset
5 4 adantr ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → K ∈ Poset
6 simpr2 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → Y ∈ B
7 simpr3 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → Z ∈ B
8 simpr1 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ∈ B
9 eqid ⊢ join ⁡ K = join ⁡ K
10 simpl ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → K ∈ Lat
11 1 9 3 10 6 7 latcl2 ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → Y Z ∈ dom ⁡ join ⁡ K ∧ Y Z ∈ dom ⁡ ∧ ˙
12 11 simprd ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → Y Z ∈ dom ⁡ ∧ ˙
13 1 2 3 5 6 7 8 12 meetle ⊢ K ∈ Lat ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X ≤ ˙ Y ∧ X ≤ ˙ Z ↔ X ≤ ˙ Y ∧ ˙ Z