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

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