Metamath Proof Explorer

Theorem poltletr

Description: Transitive law for general strict orders. (Contributed by Stefan O'Rear, 17-Jan-2015)

Ref Expression
Assertion poltletr ⊢ R Po X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A R B ∧ B R ∪ I C → A R C

Proof

Step Hyp Ref Expression
1 poleloe ⊢ C ∈ X → B R ∪ I C ↔ B R C ∨ B = C
2 1 3ad2ant3 ⊢ A ∈ X ∧ B ∈ X ∧ C ∈ X → B R ∪ I C ↔ B R C ∨ B = C
3 2 adantl ⊢ R Po X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → B R ∪ I C ↔ B R C ∨ B = C
4 3 anbi2d ⊢ R Po X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A R B ∧ B R ∪ I C ↔ A R B ∧ B R C ∨ B = C
5 potr ⊢ R Po X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A R B ∧ B R C → A R C
6 5 com12 ⊢ A R B ∧ B R C → R Po X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A R C
7 breq2 ⊢ B = C → A R B ↔ A R C
8 7 biimpac ⊢ A R B ∧ B = C → A R C
9 8 a1d ⊢ A R B ∧ B = C → R Po X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A R C
10 6 9 jaodan ⊢ A R B ∧ B R C ∨ B = C → R Po X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A R C
11 10 com12 ⊢ R Po X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A R B ∧ B R C ∨ B = C → A R C
12 4 11 sylbid ⊢ R Po X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A R B ∧ B R ∪ I C → A R C