Step |
Hyp |
Ref |
Expression |
1 |
|
cvrletr.b |
|- B = ( Base ` K ) |
2 |
|
cvrletr.l |
|- .<_ = ( le ` K ) |
3 |
|
cvrletr.s |
|- .< = ( lt ` K ) |
4 |
|
cvrletr.c |
|- C = ( |
5 |
|
simpll |
|- ( ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ X C Y ) -> K e. Poset ) |
6 |
|
simplr1 |
|- ( ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ X C Y ) -> X e. B ) |
7 |
|
simplr2 |
|- ( ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ X C Y ) -> Y e. B ) |
8 |
|
simpr |
|- ( ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ X C Y ) -> X C Y ) |
9 |
1 3 4
|
cvrlt |
|- ( ( ( K e. Poset /\ X e. B /\ Y e. B ) /\ X C Y ) -> X .< Y ) |
10 |
5 6 7 8 9
|
syl31anc |
|- ( ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ X C Y ) -> X .< Y ) |
11 |
1 2 3
|
pltletr |
|- ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .< Y /\ Y .<_ Z ) -> X .< Z ) ) |
12 |
11
|
adantr |
|- ( ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ X C Y ) -> ( ( X .< Y /\ Y .<_ Z ) -> X .< Z ) ) |
13 |
10 12
|
mpand |
|- ( ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) /\ X C Y ) -> ( Y .<_ Z -> X .< Z ) ) |
14 |
13
|
expimpd |
|- ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X C Y /\ Y .<_ Z ) -> X .< Z ) ) |