Metamath Proof Explorer

Theorem joinle

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

Ref Expression
Hypotheses joinle.b 
|- B = ( Base ` K )
joinle.l 
|- .<_ = ( le ` K )
joinle.j 
|- .\/ = ( join ` K )
joinle.k 
|- ( ph -> K e. Poset )
joinle.x 
|- ( ph -> X e. B )
joinle.y 
|- ( ph -> Y e. B )
joinle.z 
|- ( ph -> Z e. B )
joinle.e 
|- ( ph -> <. X , Y >. e. dom .\/ )
Assertion joinle 
|- ( ph -> ( ( X .<_ Z /\ Y .<_ Z ) <-> ( X .\/ Y ) .<_ Z ) )

Proof

Step Hyp Ref Expression
1 joinle.b 
 |-  B = ( Base ` K )
2 joinle.l 
 |-  .<_ = ( le ` K )
3 joinle.j 
 |-  .\/ = ( join ` K )
4 joinle.k 
 |-  ( ph -> K e. Poset )
5 joinle.x 
 |-  ( ph -> X e. B )
6 joinle.y 
 |-  ( ph -> Y e. B )
7 joinle.z 
 |-  ( ph -> Z e. B )
8 joinle.e 
 |-  ( ph -> <. X , Y >. e. dom .\/ )
9 breq2 
 |-  ( z = Z -> ( X .<_ z <-> X .<_ Z ) )
10 breq2 
 |-  ( z = Z -> ( Y .<_ z <-> Y .<_ Z ) )
11 9 10 anbi12d 
 |-  ( z = Z -> ( ( X .<_ z /\ Y .<_ z ) <-> ( X .<_ Z /\ Y .<_ Z ) ) )
12 breq2 
 |-  ( z = Z -> ( ( X .\/ Y ) .<_ z <-> ( X .\/ Y ) .<_ Z ) )
13 11 12 imbi12d 
 |-  ( z = Z -> ( ( ( X .<_ z /\ Y .<_ z ) -> ( X .\/ Y ) .<_ z ) <-> ( ( X .<_ Z /\ Y .<_ Z ) -> ( X .\/ Y ) .<_ Z ) ) )
14 1 2 3 4 5 6 8 joinlem 
 |-  ( ph -> ( ( X .<_ ( X .\/ Y ) /\ Y .<_ ( X .\/ Y ) ) /\ A. z e. B ( ( X .<_ z /\ Y .<_ z ) -> ( X .\/ Y ) .<_ z ) ) )
15 14 simprd 
 |-  ( ph -> A. z e. B ( ( X .<_ z /\ Y .<_ z ) -> ( X .\/ Y ) .<_ z ) )
16 13 15 7 rspcdva 
 |-  ( ph -> ( ( X .<_ Z /\ Y .<_ Z ) -> ( X .\/ Y ) .<_ Z ) )
17 1 2 3 4 5 6 8 lejoin1 
 |-  ( ph -> X .<_ ( X .\/ Y ) )
18 1 3 4 5 6 8 joincl 
 |-  ( ph -> ( X .\/ Y ) e. B )
19 1 2 postr 
 |-  ( ( K e. Poset /\ ( X e. B /\ ( X .\/ Y ) e. B /\ Z e. B ) ) -> ( ( X .<_ ( X .\/ Y ) /\ ( X .\/ Y ) .<_ Z ) -> X .<_ Z ) )
20 4 5 18 7 19 syl13anc 
 |-  ( ph -> ( ( X .<_ ( X .\/ Y ) /\ ( X .\/ Y ) .<_ Z ) -> X .<_ Z ) )
21 17 20 mpand 
 |-  ( ph -> ( ( X .\/ Y ) .<_ Z -> X .<_ Z ) )
22 1 2 3 4 5 6 8 lejoin2 
 |-  ( ph -> Y .<_ ( X .\/ Y ) )
23 1 2 postr 
 |-  ( ( K e. Poset /\ ( Y e. B /\ ( X .\/ Y ) e. B /\ Z e. B ) ) -> ( ( Y .<_ ( X .\/ Y ) /\ ( X .\/ Y ) .<_ Z ) -> Y .<_ Z ) )
24 4 6 18 7 23 syl13anc 
 |-  ( ph -> ( ( Y .<_ ( X .\/ Y ) /\ ( X .\/ Y ) .<_ Z ) -> Y .<_ Z ) )
25 22 24 mpand 
 |-  ( ph -> ( ( X .\/ Y ) .<_ Z -> Y .<_ Z ) )
26 21 25 jcad 
 |-  ( ph -> ( ( X .\/ Y ) .<_ Z -> ( X .<_ Z /\ Y .<_ Z ) ) )
27 16 26 impbid 
 |-  ( ph -> ( ( X .<_ Z /\ Y .<_ Z ) <-> ( X .\/ Y ) .<_ Z ) )