# Metamath Proof Explorer

## Theorem cvrval5

Description: Binary relation expressing X covers X ./\ Y . (Contributed by NM, 7-Dec-2012)

Ref Expression
Hypotheses cvrval5.b
`|- B = ( Base ` K )`
cvrval5.l
`|- .<_ = ( le ` K )`
cvrval5.j
`|- .\/ = ( join ` K )`
cvrval5.m
`|- ./\ = ( meet ` K )`
cvrval5.c
`|- C = ( `
cvrval5.a
`|- A = ( Atoms ` K )`
Assertion cvrval5
`|- ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( ( X ./\ Y ) C X <-> E. p e. A ( -. p .<_ Y /\ ( p .\/ ( X ./\ Y ) ) = X ) ) )`

### Proof

Step Hyp Ref Expression
1 cvrval5.b
` |-  B = ( Base ` K )`
2 cvrval5.l
` |-  .<_ = ( le ` K )`
3 cvrval5.j
` |-  .\/ = ( join ` K )`
4 cvrval5.m
` |-  ./\ = ( meet ` K )`
5 cvrval5.c
` |-  C = ( `
6 cvrval5.a
` |-  A = ( Atoms ` K )`
7 simp1
` |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> K e. HL )`
8 hllat
` |-  ( K e. HL -> K e. Lat )`
9 1 4 latmcl
` |-  ( ( K e. Lat /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) e. B )`
10 8 9 syl3an1
` |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( X ./\ Y ) e. B )`
11 simp2
` |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> X e. B )`
12 1 2 3 5 6 cvrval3
` |-  ( ( K e. HL /\ ( X ./\ Y ) e. B /\ X e. B ) -> ( ( X ./\ Y ) C X <-> E. p e. A ( -. p .<_ ( X ./\ Y ) /\ ( ( X ./\ Y ) .\/ p ) = X ) ) )`
13 7 10 11 12 syl3anc
` |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( ( X ./\ Y ) C X <-> E. p e. A ( -. p .<_ ( X ./\ Y ) /\ ( ( X ./\ Y ) .\/ p ) = X ) ) )`
` |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> K e. Lat )`
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) /\ ( ( X ./\ Y ) .\/ p ) = X ) -> K e. Lat )`
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) /\ ( ( X ./\ Y ) .\/ p ) = X ) -> ( X ./\ Y ) e. B )`
17 1 6 atbase
` |-  ( p e. A -> p e. B )`
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) /\ ( ( X ./\ Y ) .\/ p ) = X ) -> p e. B )`
19 1 2 3 latlej2
` |-  ( ( K e. Lat /\ ( X ./\ Y ) e. B /\ p e. B ) -> p .<_ ( ( X ./\ Y ) .\/ p ) )`
20 15 16 18 19 syl3anc
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) /\ ( ( X ./\ Y ) .\/ p ) = X ) -> p .<_ ( ( X ./\ Y ) .\/ p ) )`
21 simpr
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) /\ ( ( X ./\ Y ) .\/ p ) = X ) -> ( ( X ./\ Y ) .\/ p ) = X )`
22 20 21 breqtrd
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) /\ ( ( X ./\ Y ) .\/ p ) = X ) -> p .<_ X )`
23 22 biantrurd
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) /\ ( ( X ./\ Y ) .\/ p ) = X ) -> ( p .<_ Y <-> ( p .<_ X /\ p .<_ Y ) ) )`
24 simpll2
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) /\ ( ( X ./\ Y ) .\/ p ) = X ) -> X e. B )`
25 simpll3
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) /\ ( ( X ./\ Y ) .\/ p ) = X ) -> Y e. B )`
26 1 2 4 latlem12
` |-  ( ( K e. Lat /\ ( p e. B /\ X e. B /\ Y e. B ) ) -> ( ( p .<_ X /\ p .<_ Y ) <-> p .<_ ( X ./\ Y ) ) )`
27 15 18 24 25 26 syl13anc
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) /\ ( ( X ./\ Y ) .\/ p ) = X ) -> ( ( p .<_ X /\ p .<_ Y ) <-> p .<_ ( X ./\ Y ) ) )`
28 23 27 bitr2d
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) /\ ( ( X ./\ Y ) .\/ p ) = X ) -> ( p .<_ ( X ./\ Y ) <-> p .<_ Y ) )`
29 28 notbid
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) /\ ( ( X ./\ Y ) .\/ p ) = X ) -> ( -. p .<_ ( X ./\ Y ) <-> -. p .<_ Y ) )`
30 29 ex
` |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) -> ( ( ( X ./\ Y ) .\/ p ) = X -> ( -. p .<_ ( X ./\ Y ) <-> -. p .<_ Y ) ) )`
31 30 pm5.32rd
` |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) -> ( ( -. p .<_ ( X ./\ Y ) /\ ( ( X ./\ Y ) .\/ p ) = X ) <-> ( -. p .<_ Y /\ ( ( X ./\ Y ) .\/ p ) = X ) ) )`
` |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) -> K e. Lat )`
` |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) -> ( X ./\ Y ) e. B )`
` |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) -> p e. B )`
35 1 3 latjcom
` |-  ( ( K e. Lat /\ ( X ./\ Y ) e. B /\ p e. B ) -> ( ( X ./\ Y ) .\/ p ) = ( p .\/ ( X ./\ Y ) ) )`
36 32 33 34 35 syl3anc
` |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) -> ( ( X ./\ Y ) .\/ p ) = ( p .\/ ( X ./\ Y ) ) )`
37 36 eqeq1d
` |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) -> ( ( ( X ./\ Y ) .\/ p ) = X <-> ( p .\/ ( X ./\ Y ) ) = X ) )`
38 37 anbi2d
` |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) -> ( ( -. p .<_ Y /\ ( ( X ./\ Y ) .\/ p ) = X ) <-> ( -. p .<_ Y /\ ( p .\/ ( X ./\ Y ) ) = X ) ) )`
39 31 38 bitrd
` |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A ) -> ( ( -. p .<_ ( X ./\ Y ) /\ ( ( X ./\ Y ) .\/ p ) = X ) <-> ( -. p .<_ Y /\ ( p .\/ ( X ./\ Y ) ) = X ) ) )`
40 39 rexbidva
` |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( E. p e. A ( -. p .<_ ( X ./\ Y ) /\ ( ( X ./\ Y ) .\/ p ) = X ) <-> E. p e. A ( -. p .<_ Y /\ ( p .\/ ( X ./\ Y ) ) = X ) ) )`
41 13 40 bitrd
` |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( ( X ./\ Y ) C X <-> E. p e. A ( -. p .<_ Y /\ ( p .\/ ( X ./\ Y ) ) = X ) ) )`