Metamath Proof Explorer


Theorem cvrletrN

Description: Property of an element above a covering. (Contributed by NM, 7-Dec-2012) (New usage is discouraged.)

Ref Expression
Hypotheses cvrletr.b B = Base K
cvrletr.l ˙ = K
cvrletr.s < ˙ = < K
cvrletr.c C = K
Assertion cvrletrN K Poset X B Y B Z B X C Y Y ˙ Z X < ˙ Z

Proof

Step Hyp Ref Expression
1 cvrletr.b B = Base K
2 cvrletr.l ˙ = K
3 cvrletr.s < ˙ = < K
4 cvrletr.c C = K
5 simpll K Poset X B Y B Z B X C Y K Poset
6 simplr1 K Poset X B Y B Z B X C Y X B
7 simplr2 K Poset X B Y B Z B X C Y Y B
8 simpr K Poset X B Y B Z B X C Y X C Y
9 1 3 4 cvrlt K Poset X B Y B X C Y X < ˙ Y
10 5 6 7 8 9 syl31anc K Poset X B Y B Z B X C Y X < ˙ Y
11 1 2 3 pltletr K Poset X B Y B Z B X < ˙ Y Y ˙ Z X < ˙ Z
12 11 adantr K Poset X B Y B Z B X C Y X < ˙ Y Y ˙ Z X < ˙ Z
13 10 12 mpand K Poset X B Y B Z B X C Y Y ˙ Z X < ˙ Z
14 13 expimpd K Poset X B Y B Z B X C Y Y ˙ Z X < ˙ Z