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 ⊢ R Or S
soi.2 ⊢ R ⊆ S × S
Assertion son2lpi ⊢ ¬ A R B ∧ B R A

Proof

Step Hyp Ref Expression
1 soi.1 ⊢ R Or S
2 soi.2 ⊢ R ⊆ S × S
3 1 2 soirri ⊢ ¬ A R A
4 1 2 sotri ⊢ A R B ∧ B R A → A R A
5 3 4 mto ⊢ ¬ A R B ∧ B R A