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

Metamath Proof Explorer

Theorem latleeqm1

Description: "Less than or equal to" in terms of meet. (Contributed by NM, 7-Nov-2011)

Ref Expression
Hypotheses latmle.b 
|- B = ( Base ` K )
latmle.l 
|- .<_ = ( le ` K )
latmle.m 
|- ./\ = ( meet ` K )
Assertion latleeqm1 
|- ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> ( X ./\ Y ) = X ) )

Proof

Step Hyp Ref Expression
1 latmle.b 
 |-  B = ( Base ` K )
2 latmle.l 
 |-  .<_ = ( le ` K )
3 latmle.m 
 |-  ./\ = ( meet ` K )
4 1 2 latref 
 |-  ( ( K e. Lat /\ X e. B ) -> X .<_ X )
5 4 3adant3 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> X .<_ X )
6 5 biantrurd 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> ( X .<_ X /\ X .<_ Y ) ) )
7 simp1 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> K e. Lat )
8 simp2 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> X e. B )
9 simp3 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> Y e. B )
10 1 2 3 latlem12 
 |-  ( ( K e. Lat /\ ( X e. B /\ X e. B /\ Y e. B ) ) -> ( ( X .<_ X /\ X .<_ Y ) <-> X .<_ ( X ./\ Y ) ) )
11 7 8 8 9 10 syl13anc 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( ( X .<_ X /\ X .<_ Y ) <-> X .<_ ( X ./\ Y ) ) )
12 6 11 bitrd 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> X .<_ ( X ./\ Y ) ) )
13 1 2 3 latmle1 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) .<_ X )
14 13 biantrurd 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .<_ ( X ./\ Y ) <-> ( ( X ./\ Y ) .<_ X /\ X .<_ ( X ./\ Y ) ) ) )
15 12 14 bitrd 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> ( ( X ./\ Y ) .<_ X /\ X .<_ ( X ./\ Y ) ) ) )
16 latpos 
 |-  ( K e. Lat -> K e. Poset )
17 16 3ad2ant1 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> K e. Poset )
18 1 3 latmcl 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) e. B )
19 1 2 posasymb 
 |-  ( ( K e. Poset /\ ( X ./\ Y ) e. B /\ X e. B ) -> ( ( ( X ./\ Y ) .<_ X /\ X .<_ ( X ./\ Y ) ) <-> ( X ./\ Y ) = X ) )
20 17 18 8 19 syl3anc 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( ( ( X ./\ Y ) .<_ X /\ X .<_ ( X ./\ Y ) ) <-> ( X ./\ Y ) = X ) )
21 15 20 bitrd 
 |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> ( X ./\ Y ) = X ) )