Theorem latjle12

Description: A join is less than or equal to a third value iff each argument is less than or equal to the third value. ( chlub analog.) (Contributed by NM, 17-Sep-2011)

	Ref	Expression
Hypotheses	latlej.b	|- B = ( Base ` K )
	latlej.l	|- .<_ = ( le ` K )
	latlej.j	|- .\/ = ( join ` K )
Assertion	latjle12	|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .<_ Z /\ Y .<_ Z ) <-> ( X .\/ Y ) .<_ Z ) )

Proof

Step	Hyp	Ref	Expression
1		latlej.b	|- B = ( Base ` K )
2		latlej.l	|- .<_ = ( le ` K )
3		latlej.j	|- .\/ = ( join ` K )
4		latpos	|- ( K e. Lat -> K e. Poset )
5	4	adantr	|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> K e. Poset )
6		simpr1	|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> X e. B )
7		simpr2	|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Y e. B )
8		simpr3	|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> Z e. B )
9		eqid	|- ( meet ` K ) = ( meet ` K )
10		simpl	|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> K e. Lat )
11	1 3 9 10 6 7	latcl2	|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( <. X , Y >. e. dom .\/ /\ <. X , Y >. e. dom ( meet ` K ) ) )
12	11	simpld	|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> <. X , Y >. e. dom .\/ )
13	1 2 3 5 6 7 8 12	joinle	|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .<_ Z /\ Y .<_ Z ) <-> ( X .\/ Y ) .<_ Z ) )