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 ∧ 𝑋𝐵 ) → ( 𝑋 𝑋 ) = 𝑋 )