sotric - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > sotric		Structured version Visualization version GIF version

Theorem sotric 5465

Description: A strict order relation satisfies strict trichotomy. (Contributed by NM, 19-Feb-1996.)

**Assertion**
Ref	Expression
sotric	⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵𝑅𝐶 ↔ ¬ (𝐵 = 𝐶 ∨ 𝐶𝑅𝐵)))

**Proof of Theorem sotric**
Step	Hyp	Ref	Expression
1		sonr 5460	. . . . . 6 ⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵)
2		breq2 5034	. . . . . . 7 ⊢ (𝐵 = 𝐶 → (𝐵𝑅𝐵 ↔ 𝐵𝑅𝐶))
3	2	notbid 321	. . . . . 6 ⊢ (𝐵 = 𝐶 → (¬ 𝐵𝑅𝐵 ↔ ¬ 𝐵𝑅𝐶))
4	1, 3	syl5ibcom 248	. . . . 5 ⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐵 = 𝐶 → ¬ 𝐵𝑅𝐶))
5	4	adantrr 716	. . . 4 ⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵 = 𝐶 → ¬ 𝐵𝑅𝐶))
6		so2nr 5463	. . . . . 6 ⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐵))
7		imnan 403	. . . . . 6 ⊢ ((𝐵𝑅𝐶 → ¬ 𝐶𝑅𝐵) ↔ ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐵))
8	6, 7	sylibr 237	. . . . 5 ⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵𝑅𝐶 → ¬ 𝐶𝑅𝐵))
9	8	con2d 136	. . . 4 ⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐶𝑅𝐵 → ¬ 𝐵𝑅𝐶))
10	5, 9	jaod 856	. . 3 ⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ((𝐵 = 𝐶 ∨ 𝐶𝑅𝐵) → ¬ 𝐵𝑅𝐶))
11		solin 5462	. . . . 5 ⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵))
12		3orass 1087	. . . . 5 ⊢ ((𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵) ↔ (𝐵𝑅𝐶 ∨ (𝐵 = 𝐶 ∨ 𝐶𝑅𝐵)))
13	11, 12	sylib 221	. . . 4 ⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵𝑅𝐶 ∨ (𝐵 = 𝐶 ∨ 𝐶𝑅𝐵)))
14	13	ord 861	. . 3 ⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (¬ 𝐵𝑅𝐶 → (𝐵 = 𝐶 ∨ 𝐶𝑅𝐵)))
15	10, 14	impbid 215	. 2 ⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ((𝐵 = 𝐶 ∨ 𝐶𝑅𝐵) ↔ ¬ 𝐵𝑅𝐶))
16	15	con2bid 358	1 ⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵𝑅𝐶 ↔ ¬ (𝐵 = 𝐶 ∨ 𝐶𝑅𝐵)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 ∨ wo 844 ∨ w3o 1083 = wceq 1538 ∈ wcel 2111 class class class wbr 5030 Or wor 5437

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ral 3111 df-v 3443 df-un 3886 df-sn 4526 df-pr 4528 df-op 4532 df-br 5031 df-po 5438 df-so 5439

This theorem is referenced by: soasym 5468 sotr2 5469 sotri2 5956 sotri3 5957 somin1 5960 somincom 5961 soisores 7059 soisoi 7060 fimaxg 8749 suplub2 8909 supgtoreq 8918 fiming 8946 infsupprpr 8952 ordtypelem7 8972 fpwwe2 10054 indpi 10318 nqereu 10340 ltsonq 10380 prub 10405 ltapr 10456 suplem2pr 10464 ltsosr 10505 axpre-lttri 10576 sotr3 33115 noetalem3 33332 sleloe 33346 prproropf1olem4 44023

W3C validator