Theorem po3nr

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

	Ref	Expression
Assertion	po3nr	⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ¬ ( 𝐵 𝑅 𝐶 ∧ 𝐶 𝑅 𝐷 ∧ 𝐷 𝑅 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		po2nr	⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ¬ ( 𝐵 𝑅 𝐷 ∧ 𝐷 𝑅 𝐵 ) )
2	1	3adantr2	⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ¬ ( 𝐵 𝑅 𝐷 ∧ 𝐷 𝑅 𝐵 ) )
3		df-3an	⊢ ( ( 𝐵 𝑅 𝐶 ∧ 𝐶 𝑅 𝐷 ∧ 𝐷 𝑅 𝐵 ) ↔ ( ( 𝐵 𝑅 𝐶 ∧ 𝐶 𝑅 𝐷 ) ∧ 𝐷 𝑅 𝐵 ) )
4		potr	⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ( 𝐵 𝑅 𝐶 ∧ 𝐶 𝑅 𝐷 ) → 𝐵 𝑅 𝐷 ) )
5	4	anim1d	⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ( ( 𝐵 𝑅 𝐶 ∧ 𝐶 𝑅 𝐷 ) ∧ 𝐷 𝑅 𝐵 ) → ( 𝐵 𝑅 𝐷 ∧ 𝐷 𝑅 𝐵 ) ) )
6	3 5	syl5bi	⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ( 𝐵 𝑅 𝐶 ∧ 𝐶 𝑅 𝐷 ∧ 𝐷 𝑅 𝐵 ) → ( 𝐵 𝑅 𝐷 ∧ 𝐷 𝑅 𝐵 ) ) )
7	2 6	mtod	⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ¬ ( 𝐵 𝑅 𝐶 ∧ 𝐶 𝑅 𝐷 ∧ 𝐷 𝑅 𝐵 ) )