Metamath Proof Explorer


Theorem plelttr

Description: Transitive law for chained "less than or equal to" and "less than". ( sspsstr analog.) (Contributed by NM, 2-May-2012)

Ref Expression
Hypotheses pltletr.b 𝐵 = ( Base ‘ 𝐾 )
pltletr.l = ( le ‘ 𝐾 )
pltletr.s < = ( lt ‘ 𝐾 )
Assertion plelttr ( ( 𝐾 ∈ Poset ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ) → ( ( 𝑋 𝑌𝑌 < 𝑍 ) → 𝑋 < 𝑍 ) )

Proof

Step Hyp Ref Expression
1 pltletr.b 𝐵 = ( Base ‘ 𝐾 )
2 pltletr.l = ( le ‘ 𝐾 )
3 pltletr.s < = ( lt ‘ 𝐾 )
4 1 2 3 pleval2 ( ( 𝐾 ∈ Poset ∧ 𝑋𝐵𝑌𝐵 ) → ( 𝑋 𝑌 ↔ ( 𝑋 < 𝑌𝑋 = 𝑌 ) ) )
5 4 3adant3r3 ( ( 𝐾 ∈ Poset ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ) → ( 𝑋 𝑌 ↔ ( 𝑋 < 𝑌𝑋 = 𝑌 ) ) )
6 1 3 plttr ( ( 𝐾 ∈ Poset ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ) → ( ( 𝑋 < 𝑌𝑌 < 𝑍 ) → 𝑋 < 𝑍 ) )
7 6 expd ( ( 𝐾 ∈ Poset ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ) → ( 𝑋 < 𝑌 → ( 𝑌 < 𝑍𝑋 < 𝑍 ) ) )
8 breq1 ( 𝑋 = 𝑌 → ( 𝑋 < 𝑍𝑌 < 𝑍 ) )
9 8 biimprd ( 𝑋 = 𝑌 → ( 𝑌 < 𝑍𝑋 < 𝑍 ) )
10 9 a1i ( ( 𝐾 ∈ Poset ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ) → ( 𝑋 = 𝑌 → ( 𝑌 < 𝑍𝑋 < 𝑍 ) ) )
11 7 10 jaod ( ( 𝐾 ∈ Poset ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ) → ( ( 𝑋 < 𝑌𝑋 = 𝑌 ) → ( 𝑌 < 𝑍𝑋 < 𝑍 ) ) )
12 5 11 sylbid ( ( 𝐾 ∈ Poset ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ) → ( 𝑋 𝑌 → ( 𝑌 < 𝑍𝑋 < 𝑍 ) ) )
13 12 impd ( ( 𝐾 ∈ Poset ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ) → ( ( 𝑋 𝑌𝑌 < 𝑍 ) → 𝑋 < 𝑍 ) )