Metamath Proof Explorer


Theorem sotri

Description: A strict order relation is a transitive relation. (Contributed by NM, 10-Feb-1996) (Revised by Mario Carneiro, 10-May-2013)

Ref Expression
Hypotheses soi.1 ROrS
soi.2 RS×S
Assertion sotri ARBBRCARC

Proof

Step Hyp Ref Expression
1 soi.1 ROrS
2 soi.2 RS×S
3 2 brel ARBASBS
4 3 simpld ARBAS
5 2 brel BRCBSCS
6 4 5 anim12i ARBBRCASBSCS
7 sotr ROrSASBSCSARBBRCARC
8 1 7 mpan ASBSCSARBBRCARC
9 8 3expb ASBSCSARBBRCARC
10 6 9 mpcom ARBBRCARC