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
cvrval3.j
cvrval3.c $⊢ C = ⋖ K$
cvrval3.a $⊢ A = Atoms ⁡ K$
Assertion cvrval3

Proof

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