Theorem latjidm

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

	Ref	Expression
Hypotheses	latidm.b	|- B = ( Base ` K )
	latidm.j	|- .\/ = ( join ` K )
Assertion	latjidm	|- ( ( K e. Lat /\ X e. B ) -> ( X .\/ X ) = X )

Proof

Step	Hyp	Ref	Expression
1		latidm.b	|- B = ( Base ` K )
2		latidm.j	|- .\/ = ( join ` K )
3		eqid	|- ( le ` K ) = ( le ` K )
4		simpl	|- ( ( K e. Lat /\ X e. B ) -> K e. Lat )
5	1 2	latjcl	|- ( ( K e. Lat /\ X e. B /\ X e. B ) -> ( X .\/ X ) e. B )
6	5	3anidm23	|- ( ( K e. Lat /\ X e. B ) -> ( X .\/ X ) e. B )
7		simpr	|- ( ( K e. Lat /\ X e. B ) -> X e. B )
8	1 3	latref	|- ( ( K e. Lat /\ X e. B ) -> X ( le ` K ) X )
9	1 3 2	latjle12	|- ( ( K e. Lat /\ ( X e. B /\ X e. B /\ X e. B ) ) -> ( ( X ( le ` K ) X /\ X ( le ` K ) X ) <-> ( X .\/ X ) ( le ` K ) X ) )
10	4 7 7 7 9	syl13anc	|- ( ( K e. Lat /\ X e. B ) -> ( ( X ( le ` K ) X /\ X ( le ` K ) X ) <-> ( X .\/ X ) ( le ` K ) X ) )
11	8 8 10	mpbi2and	|- ( ( K e. Lat /\ X e. B ) -> ( X .\/ X ) ( le ` K ) X )
12	1 3 2	latlej1	|- ( ( K e. Lat /\ X e. B /\ X e. B ) -> X ( le ` K ) ( X .\/ X ) )
13	12	3anidm23	|- ( ( K e. Lat /\ X e. B ) -> X ( le ` K ) ( X .\/ X ) )
14	1 3 4 6 7 11 13	latasymd	|- ( ( K e. Lat /\ X e. B ) -> ( X .\/ X ) = X )