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 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ¬ ( 𝐵 𝑅 𝐶 ∧ 𝐶 𝑅 𝐵 ) )