# Metamath Proof Explorer

## Theorem cvrval3

Description: Binary relation expressing Y covers X . (Contributed by NM, 16-Jun-2012)

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

### Proof

Step Hyp Ref Expression
1 cvrval3.b
` |-  B = ( Base ` K )`
2 cvrval3.l
` |-  .<_ = ( le ` K )`
3 cvrval3.j
` |-  .\/ = ( join ` K )`
4 cvrval3.c
` |-  C = ( `
5 cvrval3.a
` |-  A = ( Atoms ` K )`
6 eqid
` |-  ( lt ` K ) = ( lt ` K )`
7 1 6 4 cvrlt
` |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) -> X ( lt ` K ) Y )`
8 1 2 6 3 4 5 hlrelat3
` |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X ( lt ` K ) Y ) -> E. p e. A ( X C ( X .\/ p ) /\ ( X .\/ p ) .<_ Y ) )`
9 7 8 syldan
` |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) -> E. p e. A ( X C ( X .\/ p ) /\ ( X .\/ p ) .<_ Y ) )`
10 simp3l
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ p e. A /\ ( X C ( X .\/ p ) /\ ( X .\/ p ) .<_ Y ) ) -> X C ( X .\/ p ) )`
11 simp1l1
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ p e. A /\ ( X C ( X .\/ p ) /\ ( X .\/ p ) .<_ Y ) ) -> K e. HL )`
12 simp1l2
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ p e. A /\ ( X C ( X .\/ p ) /\ ( X .\/ p ) .<_ Y ) ) -> X e. B )`
13 simp2
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ p e. A /\ ( X C ( X .\/ p ) /\ ( X .\/ p ) .<_ Y ) ) -> p e. A )`
14 1 2 3 4 5 cvr1
` |-  ( ( K e. HL /\ X e. B /\ p e. A ) -> ( -. p .<_ X <-> X C ( X .\/ p ) ) )`
15 11 12 13 14 syl3anc
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ p e. A /\ ( X C ( X .\/ p ) /\ ( X .\/ p ) .<_ Y ) ) -> ( -. p .<_ X <-> X C ( X .\/ p ) ) )`
16 10 15 mpbird
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ p e. A /\ ( X C ( X .\/ p ) /\ ( X .\/ p ) .<_ Y ) ) -> -. p .<_ X )`
17 11 hllatd
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ p e. A /\ ( X C ( X .\/ p ) /\ ( X .\/ p ) .<_ Y ) ) -> K e. Lat )`
18 1 5 atbase
` |-  ( p e. A -> p e. B )`
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ p e. A /\ ( X C ( X .\/ p ) /\ ( X .\/ p ) .<_ Y ) ) -> p e. B )`
20 1 3 latjcl
` |-  ( ( K e. Lat /\ X e. B /\ p e. B ) -> ( X .\/ p ) e. B )`
21 17 12 19 20 syl3anc
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ p e. A /\ ( X C ( X .\/ p ) /\ ( X .\/ p ) .<_ Y ) ) -> ( X .\/ p ) e. B )`
22 1 6 4 cvrlt
` |-  ( ( ( K e. HL /\ X e. B /\ ( X .\/ p ) e. B ) /\ X C ( X .\/ p ) ) -> X ( lt ` K ) ( X .\/ p ) )`
23 11 12 21 10 22 syl31anc
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ p e. A /\ ( X C ( X .\/ p ) /\ ( X .\/ p ) .<_ Y ) ) -> X ( lt ` K ) ( X .\/ p ) )`
24 simp3r
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ p e. A /\ ( X C ( X .\/ p ) /\ ( X .\/ p ) .<_ Y ) ) -> ( X .\/ p ) .<_ Y )`
25 hlpos
` |-  ( K e. HL -> K e. Poset )`
26 11 25 syl
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ p e. A /\ ( X C ( X .\/ p ) /\ ( X .\/ p ) .<_ Y ) ) -> K e. Poset )`
27 simp1l3
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ p e. A /\ ( X C ( X .\/ p ) /\ ( X .\/ p ) .<_ Y ) ) -> Y e. B )`
28 simp1r
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ p e. A /\ ( X C ( X .\/ p ) /\ ( X .\/ p ) .<_ Y ) ) -> X C Y )`
29 1 2 6 4 cvrnbtwn2
` |-  ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ ( X .\/ p ) e. B ) /\ X C Y ) -> ( ( X ( lt ` K ) ( X .\/ p ) /\ ( X .\/ p ) .<_ Y ) <-> ( X .\/ p ) = Y ) )`
30 26 12 27 21 28 29 syl131anc
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ p e. A /\ ( X C ( X .\/ p ) /\ ( X .\/ p ) .<_ Y ) ) -> ( ( X ( lt ` K ) ( X .\/ p ) /\ ( X .\/ p ) .<_ Y ) <-> ( X .\/ p ) = Y ) )`
31 23 24 30 mpbi2and
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ p e. A /\ ( X C ( X .\/ p ) /\ ( X .\/ p ) .<_ Y ) ) -> ( X .\/ p ) = Y )`
32 16 31 jca
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) /\ p e. A /\ ( X C ( X .\/ p ) /\ ( X .\/ p ) .<_ Y ) ) -> ( -. p .<_ X /\ ( X .\/ p ) = Y ) )`
33 32 3exp
` |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) -> ( p e. A -> ( ( X C ( X .\/ p ) /\ ( X .\/ p ) .<_ Y ) -> ( -. p .<_ X /\ ( X .\/ p ) = Y ) ) ) )`
34 33 reximdvai
` |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) -> ( E. p e. A ( X C ( X .\/ p ) /\ ( X .\/ p ) .<_ Y ) -> E. p e. A ( -. p .<_ X /\ ( X .\/ p ) = Y ) ) )`
35 9 34 mpd
` |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) -> E. p e. A ( -. p .<_ X /\ ( X .\/ p ) = Y ) )`
36 35 ex
` |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( X C Y -> E. p e. A ( -. p .<_ X /\ ( X .\/ p ) = Y ) ) )`
37 simp3l
` |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A /\ ( -. p .<_ X /\ ( X .\/ p ) = Y ) ) -> -. p .<_ X )`
38 simp11
` |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A /\ ( -. p .<_ X /\ ( X .\/ p ) = Y ) ) -> K e. HL )`
39 simp12
` |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A /\ ( -. p .<_ X /\ ( X .\/ p ) = Y ) ) -> X e. B )`
40 simp2
` |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A /\ ( -. p .<_ X /\ ( X .\/ p ) = Y ) ) -> p e. A )`
41 38 39 40 14 syl3anc
` |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A /\ ( -. p .<_ X /\ ( X .\/ p ) = Y ) ) -> ( -. p .<_ X <-> X C ( X .\/ p ) ) )`
42 37 41 mpbid
` |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A /\ ( -. p .<_ X /\ ( X .\/ p ) = Y ) ) -> X C ( X .\/ p ) )`
43 simp3r
` |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A /\ ( -. p .<_ X /\ ( X .\/ p ) = Y ) ) -> ( X .\/ p ) = Y )`
44 42 43 breqtrd
` |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ p e. A /\ ( -. p .<_ X /\ ( X .\/ p ) = Y ) ) -> X C Y )`
45 44 rexlimdv3a
` |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( E. p e. A ( -. p .<_ X /\ ( X .\/ p ) = Y ) -> X C Y ) )`
46 36 45 impbid
` |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( X C Y <-> E. p e. A ( -. p .<_ X /\ ( X .\/ p ) = Y ) ) )`