Metamath Proof Explorer

Theorem plttr

Description: The less-than relation is transitive. ( psstr analog.) (Contributed by NM, 2-Dec-2011)

Ref Expression
Hypotheses pltnlt.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
pltnlt.s ⊢ < = ( lt ‘ 𝐾 )
Assertion plttr ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 < 𝑌 ∧ 𝑌 < 𝑍 ) → 𝑋 < 𝑍 ) )

Proof

Step Hyp Ref Expression
1 pltnlt.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 pltnlt.s ⊢ < = ( lt ‘ 𝐾 )
3 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
4 3 2 pltle ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 < 𝑌 → 𝑋 ( le ‘ 𝐾 ) 𝑌 ) )
5 4 3adant3r3 ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 < 𝑌 → 𝑋 ( le ‘ 𝐾 ) 𝑌 ) )
6 3 2 pltle ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑌 < 𝑍 → 𝑌 ( le ‘ 𝐾 ) 𝑍 ) )
7 6 3adant3r1 ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑌 < 𝑍 → 𝑌 ( le ‘ 𝐾 ) 𝑍 ) )
8 1 3 postr ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ( le ‘ 𝐾 ) 𝑌 ∧ 𝑌 ( le ‘ 𝐾 ) 𝑍 ) → 𝑋 ( le ‘ 𝐾 ) 𝑍 ) )
9 5 7 8 syl2and ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 < 𝑌 ∧ 𝑌 < 𝑍 ) → 𝑋 ( le ‘ 𝐾 ) 𝑍 ) )
10 1 2 pltn2lp ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ¬ ( 𝑋 < 𝑌 ∧ 𝑌 < 𝑋 ) )
11 10 3adant3r3 ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ¬ ( 𝑋 < 𝑌 ∧ 𝑌 < 𝑋 ) )
12 breq2 ⊢ ( 𝑋 = 𝑍 → ( 𝑌 < 𝑋 ↔ 𝑌 < 𝑍 ) )
13 12 anbi2d ⊢ ( 𝑋 = 𝑍 → ( ( 𝑋 < 𝑌 ∧ 𝑌 < 𝑋 ) ↔ ( 𝑋 < 𝑌 ∧ 𝑌 < 𝑍 ) ) )
14 13 notbid ⊢ ( 𝑋 = 𝑍 → ( ¬ ( 𝑋 < 𝑌 ∧ 𝑌 < 𝑋 ) ↔ ¬ ( 𝑋 < 𝑌 ∧ 𝑌 < 𝑍 ) ) )
15 11 14 syl5ibcom ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 = 𝑍 → ¬ ( 𝑋 < 𝑌 ∧ 𝑌 < 𝑍 ) ) )
16 15 necon2ad ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 < 𝑌 ∧ 𝑌 < 𝑍 ) → 𝑋 ≠ 𝑍 ) )
17 9 16 jcad ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 < 𝑌 ∧ 𝑌 < 𝑍 ) → ( 𝑋 ( le ‘ 𝐾 ) 𝑍 ∧ 𝑋 ≠ 𝑍 ) ) )
18 3 2 pltval ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 < 𝑍 ↔ ( 𝑋 ( le ‘ 𝐾 ) 𝑍 ∧ 𝑋 ≠ 𝑍 ) ) )
19 18 3adant3r2 ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 < 𝑍 ↔ ( 𝑋 ( le ‘ 𝐾 ) 𝑍 ∧ 𝑋 ≠ 𝑍 ) ) )
20 17 19 sylibrd ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 < 𝑌 ∧ 𝑌 < 𝑍 ) → 𝑋 < 𝑍 ) )