Step |
Hyp |
Ref |
Expression |
1 |
|
pltletr.b |
|- B = ( Base ` K ) |
2 |
|
pltletr.l |
|- .<_ = ( le ` K ) |
3 |
|
pltletr.s |
|- .< = ( lt ` K ) |
4 |
1 2 3
|
pleval2 |
|- ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> ( X .< Y \/ X = Y ) ) ) |
5 |
4
|
3adant3r3 |
|- ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .<_ Y <-> ( X .< Y \/ X = Y ) ) ) |
6 |
1 3
|
plttr |
|- ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .< Y /\ Y .< Z ) -> X .< Z ) ) |
7 |
6
|
expd |
|- ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .< Y -> ( Y .< Z -> X .< Z ) ) ) |
8 |
|
breq1 |
|- ( X = Y -> ( X .< Z <-> Y .< Z ) ) |
9 |
8
|
biimprd |
|- ( X = Y -> ( Y .< Z -> X .< Z ) ) |
10 |
9
|
a1i |
|- ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X = Y -> ( Y .< Z -> X .< Z ) ) ) |
11 |
7 10
|
jaod |
|- ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .< Y \/ X = Y ) -> ( Y .< Z -> X .< Z ) ) ) |
12 |
5 11
|
sylbid |
|- ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .<_ Y -> ( Y .< Z -> X .< Z ) ) ) |
13 |
12
|
impd |
|- ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X .<_ Y /\ Y .< Z ) -> X .< Z ) ) |