Metamath Proof Explorer

Theorem latjidm

Description: Lattice join is idempotent. Analogue of unidm . (Contributed by NM, 8-Oct-2011)

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

Proof

Step Hyp Ref Expression
1 latjidm.b ⊢ B = Base K
2 latjidm.j ⊢ ∨ ˙ = join ⁡ K
3 eqid ⊢ ≤ K = ≤ K
4 simpl ⊢ K ∈ Lat ∧ X ∈ B → K ∈ Lat
5 1 2 latjcl ⊢ K ∈ Lat ∧ X ∈ B ∧ X ∈ B → X ∨ ˙ X ∈ B
6 5 3anidm23 ⊢ K ∈ Lat ∧ X ∈ B → X ∨ ˙ X ∈ B
7 simpr ⊢ K ∈ Lat ∧ X ∈ B → X ∈ B
8 1 3 latref ⊢ K ∈ Lat ∧ X ∈ B → X ≤ K X
9 1 3 2 latjle12 ⊢ K ∈ Lat ∧ X ∈ B ∧ X ∈ B ∧ X ∈ B → X ≤ K X ∧ X ≤ K X ↔ X ∨ ˙ X ≤ K X
10 4 7 7 7 9 syl13anc ⊢ K ∈ Lat ∧ X ∈ B → X ≤ K X ∧ X ≤ K X ↔ X ∨ ˙ X ≤ K X
11 8 8 10 mpbi2and ⊢ K ∈ Lat ∧ X ∈ B → X ∨ ˙ X ≤ K X
12 1 3 2 latlej1 ⊢ K ∈ Lat ∧ X ∈ B ∧ X ∈ B → X ≤ K X ∨ ˙ X
13 12 3anidm23 ⊢ K ∈ Lat ∧ X ∈ B → X ≤ K X ∨ ˙ X
14 1 3 4 6 7 11 13 latasymd ⊢ K ∈ Lat ∧ X ∈ B → X ∨ ˙ X = X