# Metamath Proof Explorer

## Theorem cvrval4N

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

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

### Proof

Step Hyp Ref Expression
1 cvrval4.b
` |-  B = ( Base ` K )`
2 cvrval4.s
` |-  .< = ( lt ` K )`
3 cvrval4.j
` |-  .\/ = ( join ` K )`
4 cvrval4.c
` |-  C = ( `
5 cvrval4.a
` |-  A = ( Atoms ` K )`
6 1 2 4 cvrlt
` |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) -> X .< Y )`
7 eqid
` |-  ( le ` K ) = ( le ` K )`
8 1 7 3 4 5 cvrval3
` |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( X C Y <-> E. p e. A ( -. p ( le ` K ) X /\ ( X .\/ p ) = Y ) ) )`
9 simpr
` |-  ( ( -. p ( le ` K ) X /\ ( X .\/ p ) = Y ) -> ( X .\/ p ) = Y )`
10 9 reximi
` |-  ( E. p e. A ( -. p ( le ` K ) X /\ ( X .\/ p ) = Y ) -> E. p e. A ( X .\/ p ) = Y )`
11 8 10 syl6bi
` |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( X C Y -> E. p e. A ( X .\/ p ) = Y ) )`
12 11 imp
` |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) -> E. p e. A ( X .\/ p ) = Y )`
13 6 12 jca
` |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X C Y ) -> ( X .< Y /\ E. p e. A ( X .\/ p ) = Y ) )`
14 13 ex
` |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( X C Y -> ( X .< Y /\ E. p e. A ( X .\/ p ) = Y ) ) )`
15 simp1r
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. A /\ ( X .\/ p ) = Y ) -> X .< Y )`
16 simp3
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. A /\ ( X .\/ p ) = Y ) -> ( X .\/ p ) = Y )`
17 15 16 breqtrrd
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. A /\ ( X .\/ p ) = Y ) -> X .< ( X .\/ p ) )`
18 simp1l1
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. A /\ ( X .\/ p ) = Y ) -> K e. HL )`
19 simp1l2
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. A /\ ( X .\/ p ) = Y ) -> X e. B )`
20 simp2
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. A /\ ( X .\/ p ) = Y ) -> p e. A )`
21 1 7 3 4 5 cvr1
` |-  ( ( K e. HL /\ X e. B /\ p e. A ) -> ( -. p ( le ` K ) X <-> X C ( X .\/ p ) ) )`
22 18 19 20 21 syl3anc
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. A /\ ( X .\/ p ) = Y ) -> ( -. p ( le ` K ) X <-> X C ( X .\/ p ) ) )`
23 1 2 3 4 5 cvr2N
` |-  ( ( K e. HL /\ X e. B /\ p e. A ) -> ( X .< ( X .\/ p ) <-> X C ( X .\/ p ) ) )`
24 18 19 20 23 syl3anc
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. A /\ ( X .\/ p ) = Y ) -> ( X .< ( X .\/ p ) <-> X C ( X .\/ p ) ) )`
25 22 24 bitr4d
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. A /\ ( X .\/ p ) = Y ) -> ( -. p ( le ` K ) X <-> X .< ( X .\/ p ) ) )`
26 17 25 mpbird
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. A /\ ( X .\/ p ) = Y ) -> -. p ( le ` K ) X )`
27 26 16 jca
` |-  ( ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) /\ p e. A /\ ( X .\/ p ) = Y ) -> ( -. p ( le ` K ) X /\ ( X .\/ p ) = Y ) )`
28 27 3exp
` |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) -> ( p e. A -> ( ( X .\/ p ) = Y -> ( -. p ( le ` K ) X /\ ( X .\/ p ) = Y ) ) ) )`
29 28 reximdvai
` |-  ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) -> ( E. p e. A ( X .\/ p ) = Y -> E. p e. A ( -. p ( le ` K ) X /\ ( X .\/ p ) = Y ) ) )`
30 29 expimpd
` |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( ( X .< Y /\ E. p e. A ( X .\/ p ) = Y ) -> E. p e. A ( -. p ( le ` K ) X /\ ( X .\/ p ) = Y ) ) )`
31 30 8 sylibrd
` |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( ( X .< Y /\ E. p e. A ( X .\/ p ) = Y ) -> X C Y ) )`
32 14 31 impbid
` |-  ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( X C Y <-> ( X .< Y /\ E. p e. A ( X .\/ p ) = Y ) ) )`