Metamath Proof Explorer


Theorem po2nr

Description: A partial order has no 2-cycle loops. (Contributed by NM, 27-Mar-1997)

Ref Expression
Assertion po2nr ( ( 𝑅 Po 𝐴 ∧ ( 𝐵𝐴𝐶𝐴 ) ) → ¬ ( 𝐵 𝑅 𝐶𝐶 𝑅 𝐵 ) )

Proof

Step Hyp Ref Expression
1 poirr ( ( 𝑅 Po 𝐴𝐵𝐴 ) → ¬ 𝐵 𝑅 𝐵 )
2 1 adantrr ( ( 𝑅 Po 𝐴 ∧ ( 𝐵𝐴𝐶𝐴 ) ) → ¬ 𝐵 𝑅 𝐵 )
3 potr ( ( 𝑅 Po 𝐴 ∧ ( 𝐵𝐴𝐶𝐴𝐵𝐴 ) ) → ( ( 𝐵 𝑅 𝐶𝐶 𝑅 𝐵 ) → 𝐵 𝑅 𝐵 ) )
4 3 3exp2 ( 𝑅 Po 𝐴 → ( 𝐵𝐴 → ( 𝐶𝐴 → ( 𝐵𝐴 → ( ( 𝐵 𝑅 𝐶𝐶 𝑅 𝐵 ) → 𝐵 𝑅 𝐵 ) ) ) ) )
5 4 com34 ( 𝑅 Po 𝐴 → ( 𝐵𝐴 → ( 𝐵𝐴 → ( 𝐶𝐴 → ( ( 𝐵 𝑅 𝐶𝐶 𝑅 𝐵 ) → 𝐵 𝑅 𝐵 ) ) ) ) )
6 5 pm2.43d ( 𝑅 Po 𝐴 → ( 𝐵𝐴 → ( 𝐶𝐴 → ( ( 𝐵 𝑅 𝐶𝐶 𝑅 𝐵 ) → 𝐵 𝑅 𝐵 ) ) ) )
7 6 imp32 ( ( 𝑅 Po 𝐴 ∧ ( 𝐵𝐴𝐶𝐴 ) ) → ( ( 𝐵 𝑅 𝐶𝐶 𝑅 𝐵 ) → 𝐵 𝑅 𝐵 ) )
8 2 7 mtod ( ( 𝑅 Po 𝐴 ∧ ( 𝐵𝐴𝐶𝐴 ) ) → ¬ ( 𝐵 𝑅 𝐶𝐶 𝑅 𝐵 ) )