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	⊢ ¬ ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐴 )