Theorem sotri3 5233

Description: A transitivity relation. (Read A < B and B <_ C implies A < C.) (Contributed by Mario Carneiro, 10-May-2013.)

Hypotheses

Ref	Expression
soi.1	|- R Or S
soi.2	|- R C_ ( S X. S )

Assertion

Ref	Expression
sotri3	|- ( ( C e. S /\ A R B /\ -. C R B ) -> A R C )

Proof of Theorem sotri3

Step	Hyp	Ref	Expression
1		soi.2	. . . . . 6 |- R C_ ( S X. S )
2	1	brel 4886	. . . . 5 |- ( A R B -> ( A e. S /\ B e. S ) )
3	2	simprd 465	. . . 4 |- ( A R B -> B e. S )
4		soi.1	. . . . . . . 8 |- R Or S
5		sotric 4784	. . . . . . . 8 |- ( ( R Or S /\ ( C e. S /\ B e. S ) ) -> ( C R B <-> -. ( C = B \/ B R C ) ) )
6	4, 5	mpan 677	. . . . . . 7 |- ( ( C e. S /\ B e. S ) -> ( C R B <-> -. ( C = B \/ B R C ) ) )
7	6	con2bid 331	. . . . . 6 |- ( ( C e. S /\ B e. S ) -> ( ( C = B \/ B R C ) <-> -. C R B ) )
8		breq2 4409	. . . . . . . 8 |- ( C = B -> ( A R C <-> A R B ) )
9	8	biimprd 227	. . . . . . 7 |- ( C = B -> ( A R B -> A R C ) )
10	4, 1	sotri 5230	. . . . . . . 8 |- ( ( A R B /\ B R C ) -> A R C )
11	10	expcom 437	. . . . . . 7 |- ( B R C -> ( A R B -> A R C ) )
12	9, 11	jaoi 381	. . . . . 6 |- ( ( C = B \/ B R C ) -> ( A R B -> A R C ) )
13	7, 12	syl6bir 233	. . . . 5 |- ( ( C e. S /\ B e. S ) -> ( -. C R B -> ( A R B -> A R C ) ) )
14	13	com3r 82	. . . 4 |- ( A R B -> ( ( C e. S /\ B e. S ) -> ( -. C R B -> A R C ) ) )
15	3, 14	mpan2d 681	. . 3 |- ( A R B -> ( C e. S -> ( -. C R B -> A R C ) ) )
16	15	com12 32	. 2 |- ( C e. S -> ( A R B -> ( -. C R B -> A R C ) ) )
17	16	3imp 1203	1 |- ( ( C e. S /\ A R B /\ -. C R B ) -> A R C )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 188   \/ wo 370   /\ wa 371   /\ w3a 986   = wceq 1446   e. wcel 1889   C_ wss 3406   class class class wbr 4405   Or wor 4757   X. cxp 4835

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-nul 4537  ax-pr 4642

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 987  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-rab 2748  df-v 3049  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-sn 3971  df-pr 3973  df-op 3977  df-br 4406  df-opab 4465  df-po 4758  df-so 4759  df-xp 4843

This theorem is referenced by:  archnq  9410