This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrid ⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ( ( 𝐵 𝑅 𝐶 ∧ 𝐶 𝑅 𝐷 ∧ 𝐷 𝑅 𝐵 ) → ( 𝐵 𝑅 𝐷 ∧ 𝐷 𝑅 𝐵 ) ) )
7 2 6 mtod ⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴 ) ) → ¬ ( 𝐵 𝑅 𝐶 ∧ 𝐶 𝑅 𝐷 ∧ 𝐷 𝑅 𝐵 ) )