Theorem sotric 2148

Description: A strict order relation satisfies strict trichotomy.

Assertion

Ref	Expression
sotric	|- ((R Or A /\ (B e. A /\ C e. A)) -> (BRC <-> -. (B = C \/ CRB)))

Proof of Theorem sotric

Step	Hyp	Ref	Expression
1		breq2 2066	. . . . . . . 8 |- (B = C -> (BRB <-> BRC))
2	1	negbid 463	. . . . . . 7 |- (B = C -> (-. BRB <-> -. BRC))
3		sonr 2143	. . . . . . 7 |- ((R Or A /\ B e. A) -> -. BRB)
4	2, 3	syl5bi 183	. . . . . 6 |- (B = C -> ((R Or A /\ B e. A) -> -. BRC))
5	4	com12 13	. . . . 5 |- ((R Or A /\ B e. A) -> (B = C -> -. BRC))
6	5	adantrr 312	. . . 4 |- ((R Or A /\ (B e. A /\ C e. A)) -> (B = C -> -. BRC))
7		so2nr 2146	. . . . . 6 |- ((R Or A /\ (B e. A /\ C e. A)) -> -. (BRC /\ CRB))
8		imnan 207	. . . . . 6 |- ((BRC -> -. CRB) <-> -. (BRC /\ CRB))
9	7, 8	sylibr 175	. . . . 5 |- ((R Or A /\ (B e. A /\ C e. A)) -> (BRC -> -. CRB))
10	9	con2d 83	. . . 4 |- ((R Or A /\ (B e. A /\ C e. A)) -> (CRB -> -. BRC))
11	6, 10	jaod 329	. . 3 |- ((R Or A /\ (B e. A /\ C e. A)) -> ((B = C \/ CRB) -> -. BRC))
12		solin 2145	. . . 4 |- ((R Or A /\ (B e. A /\ C e. A)) -> (BRC \/ B = C \/ CRB))
13		3orass 584	. . . . 5 |- ((BRC \/ B = C \/ CRB) <-> (BRC \/ (B = C \/ CRB)))
14		df-or 197	. . . . 5 |- ((BRC \/ (B = C \/ CRB)) <-> (-. BRC -> (B = C \/ CRB)))
15	13, 14	bitr 151	. . . 4 |- ((BRC \/ B = C \/ CRB) <-> (-. BRC -> (B = C \/ CRB)))
16	12, 15	sylib 173	. . 3 |- ((R Or A /\ (B e. A /\ C e. A)) -> (-. BRC -> (B = C \/ CRB)))
17	11, 16	impbid 397	. 2 |- ((R Or A /\ (B e. A /\ C e. A)) -> ((B = C \/ CRB) <-> -. BRC))
18	17	bicon2d 404	1 |- ((R Or A /\ (B e. A /\ C e. A)) -> (BRC <-> -. (B = C \/ CRB)))

Syntax hints:  -. wn 1   -> wi 2   <-> wb 127   \/ wo 195   /\ wa 196   \/ w3o 580   = wceq 1091   e. wcel 1092   class class class wbr 2054   Or wor 2059

This theorem is referenced by:  sotrieq 2149  indpi 3828  ltsopq 3869  ltrpq 3879  prub 3892  prlem934b 3932  ltapr 3945  suplem2pr 3956  ltsosr 3997  suppsr2 4017  suppsr3 4018  ltsor 4055  axlttri 4083

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3or 582  df-3an 583  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-v 1349  df-un 1490  df-sn 1811  df-pr 1812  df-op 1815  df-br 2063  df-po 2128  df-so 2138

metamath.org