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

Metamath Proof Explorer

Theorem son2lpi

Description: A strict order relation has no 2-cycle loops. (Contributed by NM, 10-Feb-1996) (Revised by Mario Carneiro, 10-May-2013)

Ref Expression
Hypotheses soi.1 ⊢ 𝑅 Or 𝑆
soi.2 ⊢ 𝑅 ⊆ ( 𝑆 × 𝑆 )
Assertion son2lpi ¬ ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐴 )

Proof

Step Hyp Ref Expression
1 soi.1 ⊢ 𝑅 Or 𝑆
2 soi.2 ⊢ 𝑅 ⊆ ( 𝑆 × 𝑆 )
3 1 2 soirri ⊢ ¬ 𝐴 𝑅 𝐴
4 1 2 sotri ⊢ ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐴 ) → 𝐴 𝑅 𝐴 )
5 3 4 mto ⊢ ¬ ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐴 )