Metamath Proof Explorer


Theorem meetle

Description: A meet 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) (Revised by NM, 12-Sep-2018)

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

Proof

Step Hyp Ref Expression
1 meetle.b
 |-  B = ( Base ` K )
2 meetle.l
 |-  .<_ = ( le ` K )
3 meetle.m
 |-  ./\ = ( meet ` K )
4 meetle.k
 |-  ( ph -> K e. Poset )
5 meetle.x
 |-  ( ph -> X e. B )
6 meetle.y
 |-  ( ph -> Y e. B )
7 meetle.z
 |-  ( ph -> Z e. B )
8 meetle.e
 |-  ( ph -> <. X , Y >. e. dom ./\ )
9 breq1
 |-  ( z = Z -> ( z .<_ X <-> Z .<_ X ) )
10 breq1
 |-  ( z = Z -> ( z .<_ Y <-> Z .<_ Y ) )
11 9 10 anbi12d
 |-  ( z = Z -> ( ( z .<_ X /\ z .<_ Y ) <-> ( Z .<_ X /\ Z .<_ Y ) ) )
12 breq1
 |-  ( z = Z -> ( z .<_ ( X ./\ Y ) <-> Z .<_ ( X ./\ Y ) ) )
13 11 12 imbi12d
 |-  ( z = Z -> ( ( ( z .<_ X /\ z .<_ Y ) -> z .<_ ( X ./\ Y ) ) <-> ( ( Z .<_ X /\ Z .<_ Y ) -> Z .<_ ( X ./\ Y ) ) ) )
14 1 2 3 4 5 6 8 meetlem
 |-  ( ph -> ( ( ( X ./\ Y ) .<_ X /\ ( X ./\ Y ) .<_ Y ) /\ A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ ( X ./\ Y ) ) ) )
15 14 simprd
 |-  ( ph -> A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ ( X ./\ Y ) ) )
16 13 15 7 rspcdva
 |-  ( ph -> ( ( Z .<_ X /\ Z .<_ Y ) -> Z .<_ ( X ./\ Y ) ) )
17 1 2 3 4 5 6 8 lemeet1
 |-  ( ph -> ( X ./\ Y ) .<_ X )
18 1 3 4 5 6 8 meetcl
 |-  ( ph -> ( X ./\ Y ) e. B )
19 1 2 postr
 |-  ( ( K e. Poset /\ ( Z e. B /\ ( X ./\ Y ) e. B /\ X e. B ) ) -> ( ( Z .<_ ( X ./\ Y ) /\ ( X ./\ Y ) .<_ X ) -> Z .<_ X ) )
20 4 7 18 5 19 syl13anc
 |-  ( ph -> ( ( Z .<_ ( X ./\ Y ) /\ ( X ./\ Y ) .<_ X ) -> Z .<_ X ) )
21 17 20 mpan2d
 |-  ( ph -> ( Z .<_ ( X ./\ Y ) -> Z .<_ X ) )
22 1 2 3 4 5 6 8 lemeet2
 |-  ( ph -> ( X ./\ Y ) .<_ Y )
23 1 2 postr
 |-  ( ( K e. Poset /\ ( Z e. B /\ ( X ./\ Y ) e. B /\ Y e. B ) ) -> ( ( Z .<_ ( X ./\ Y ) /\ ( X ./\ Y ) .<_ Y ) -> Z .<_ Y ) )
24 4 7 18 6 23 syl13anc
 |-  ( ph -> ( ( Z .<_ ( X ./\ Y ) /\ ( X ./\ Y ) .<_ Y ) -> Z .<_ Y ) )
25 22 24 mpan2d
 |-  ( ph -> ( Z .<_ ( X ./\ Y ) -> Z .<_ Y ) )
26 21 25 jcad
 |-  ( ph -> ( Z .<_ ( X ./\ Y ) -> ( Z .<_ X /\ Z .<_ Y ) ) )
27 16 26 impbid
 |-  ( ph -> ( ( Z .<_ X /\ Z .<_ Y ) <-> Z .<_ ( X ./\ Y ) ) )