# 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}={\mathrm{Base}}_{{K}}$
cvrval5.l
cvrval5.j
cvrval5.m
cvrval5.c ${⊢}{C}={⋖}_{{K}}$
cvrval5.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
Assertion cvrval5

### Proof

Step Hyp Ref Expression
1 cvrval5.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 cvrval5.l
3 cvrval5.j
4 cvrval5.m
5 cvrval5.c ${⊢}{C}={⋖}_{{K}}$
6 cvrval5.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
7 simp1 ${⊢}\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {K}\in \mathrm{HL}$
8 hllat ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{Lat}$
9 1 4 latmcl
10 8 9 syl3an1
11 simp2 ${⊢}\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {X}\in {B}$
12 1 2 3 5 6 cvrval3
13 7 10 11 12 syl3anc
14 8 3ad2ant1 ${⊢}\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\to {K}\in \mathrm{Lat}$
17 1 6 atbase ${⊢}{p}\in {A}\to {p}\in {B}$
19 1 2 3 latlej2
20 15 16 18 19 syl3anc
21 simpr
22 20 21 breqtrd
23 22 biantrurd
24 simpll2
25 simpll3
26 1 2 4 latlem12
27 15 18 24 25 26 syl13anc
28 23 27 bitr2d
29 28 notbid
30 29 ex
31 30 pm5.32rd
32 14 adantr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {p}\in {A}\right)\to {K}\in \mathrm{Lat}$
34 17 adantl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\in {B}\wedge {Y}\in {B}\right)\wedge {p}\in {A}\right)\to {p}\in {B}$