Metamath Proof Explorer


Theorem so2nr

Description: A strict order relation has no 2-cycle loops. (Contributed by NM, 21-Jan-1996)

Ref Expression
Assertion so2nr ( ( 𝑅 Or 𝐴 ∧ ( 𝐵𝐴𝐶𝐴 ) ) → ¬ ( 𝐵 𝑅 𝐶𝐶 𝑅 𝐵 ) )

Proof

Step Hyp Ref Expression
1 sopo ( 𝑅 Or 𝐴𝑅 Po 𝐴 )
2 po2nr ( ( 𝑅 Po 𝐴 ∧ ( 𝐵𝐴𝐶𝐴 ) ) → ¬ ( 𝐵 𝑅 𝐶𝐶 𝑅 𝐵 ) )
3 1 2 sylan ( ( 𝑅 Or 𝐴 ∧ ( 𝐵𝐴𝐶𝐴 ) ) → ¬ ( 𝐵 𝑅 𝐶𝐶 𝑅 𝐵 ) )