Theorem poltletr

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

	Ref	Expression
Assertion	poltletr	⊢ ( ( 𝑅 Po 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 ( 𝑅 ∪ I ) 𝐶 ) → 𝐴 𝑅 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		poleloe	⊢ ( 𝐶 ∈ 𝑋 → ( 𝐵 ( 𝑅 ∪ I ) 𝐶 ↔ ( 𝐵 𝑅 𝐶 ∨ 𝐵 = 𝐶 ) ) )
2	1	3ad2ant3	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐵 ( 𝑅 ∪ I ) 𝐶 ↔ ( 𝐵 𝑅 𝐶 ∨ 𝐵 = 𝐶 ) ) )
3	2	adantl	⊢ ( ( 𝑅 Po 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐵 ( 𝑅 ∪ I ) 𝐶 ↔ ( 𝐵 𝑅 𝐶 ∨ 𝐵 = 𝐶 ) ) )
4	3	anbi2d	⊢ ( ( 𝑅 Po 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 ( 𝑅 ∪ I ) 𝐶 ) ↔ ( 𝐴 𝑅 𝐵 ∧ ( 𝐵 𝑅 𝐶 ∨ 𝐵 = 𝐶 ) ) ) )
5		potr	⊢ ( ( 𝑅 Po 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 ) )
6	5	com12	⊢ ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → ( ( 𝑅 Po 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐴 𝑅 𝐶 ) )
7		breq2	⊢ ( 𝐵 = 𝐶 → ( 𝐴 𝑅 𝐵 ↔ 𝐴 𝑅 𝐶 ) )
8	7	biimpac	⊢ ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 = 𝐶 ) → 𝐴 𝑅 𝐶 )
9	8	a1d	⊢ ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 = 𝐶 ) → ( ( 𝑅 Po 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐴 𝑅 𝐶 ) )
10	6 9	jaodan	⊢ ( ( 𝐴 𝑅 𝐵 ∧ ( 𝐵 𝑅 𝐶 ∨ 𝐵 = 𝐶 ) ) → ( ( 𝑅 Po 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → 𝐴 𝑅 𝐶 ) )
11	10	com12	⊢ ( ( 𝑅 Po 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝑅 𝐵 ∧ ( 𝐵 𝑅 𝐶 ∨ 𝐵 = 𝐶 ) ) → 𝐴 𝑅 𝐶 ) )
12	4 11	sylbid	⊢ ( ( 𝑅 Po 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 ( 𝑅 ∪ I ) 𝐶 ) → 𝐴 𝑅 𝐶 ) )