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

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