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

Metamath Proof Explorer

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 ) )