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

Metamath Proof Explorer

Theorem latjidm

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

Ref Expression
Hypotheses latjidm.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
latjidm.j ⊢ ∨ = ( join ‘ 𝐾 )
Assertion latjidm ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑋 ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 latjidm.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 latjidm.j ⊢ ∨ = ( join ‘ 𝐾 )
3 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
4 simpl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) → 𝐾 ∈ Lat )
5 1 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑋 ) ∈ 𝐵 )
6 5 3anidm23 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑋 ) ∈ 𝐵 )
7 simpr ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
8 1 3 latref ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ( le ‘ 𝐾 ) 𝑋 )
9 1 3 2 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑋 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑋 ( le ‘ 𝐾 ) 𝑋 ) ↔ ( 𝑋 ∨ 𝑋 ) ( le ‘ 𝐾 ) 𝑋 ) )
10 4 7 7 7 9 syl13anc ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑋 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑋 ( le ‘ 𝐾 ) 𝑋 ) ↔ ( 𝑋 ∨ 𝑋 ) ( le ‘ 𝐾 ) 𝑋 ) )
11 8 8 10 mpbi2and ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑋 ) ( le ‘ 𝐾 ) 𝑋 )
12 1 3 2 latlej1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑋 ) )
13 12 3anidm23 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ( le ‘ 𝐾 ) ( 𝑋 ∨ 𝑋 ) )
14 1 3 4 6 7 11 13 latasymd ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑋 ) = 𝑋 )