![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sotric | Structured version Visualization version GIF version |
Description: A strict order relation satisfies strict trichotomy. (Contributed by NM, 19-Feb-1996.) |
Ref | Expression |
---|---|
sotric | ⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵𝑅𝐶 ↔ ¬ (𝐵 = 𝐶 ∨ 𝐶𝑅𝐵))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sonr 5612 | . . . . . 6 ⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵) | |
2 | breq2 5153 | . . . . . . 7 ⊢ (𝐵 = 𝐶 → (𝐵𝑅𝐵 ↔ 𝐵𝑅𝐶)) | |
3 | 2 | notbid 318 | . . . . . 6 ⊢ (𝐵 = 𝐶 → (¬ 𝐵𝑅𝐵 ↔ ¬ 𝐵𝑅𝐶)) |
4 | 1, 3 | syl5ibcom 244 | . . . . 5 ⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐵 = 𝐶 → ¬ 𝐵𝑅𝐶)) |
5 | 4 | adantrr 716 | . . . 4 ⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵 = 𝐶 → ¬ 𝐵𝑅𝐶)) |
6 | so2nr 5615 | . . . . . 6 ⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐵)) | |
7 | imnan 401 | . . . . . 6 ⊢ ((𝐵𝑅𝐶 → ¬ 𝐶𝑅𝐵) ↔ ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐵)) | |
8 | 6, 7 | sylibr 233 | . . . . 5 ⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵𝑅𝐶 → ¬ 𝐶𝑅𝐵)) |
9 | 8 | con2d 134 | . . . 4 ⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐶𝑅𝐵 → ¬ 𝐵𝑅𝐶)) |
10 | 5, 9 | jaod 858 | . . 3 ⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ((𝐵 = 𝐶 ∨ 𝐶𝑅𝐵) → ¬ 𝐵𝑅𝐶)) |
11 | solin 5614 | . . . . 5 ⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵)) | |
12 | 3orass 1091 | . . . . 5 ⊢ ((𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵) ↔ (𝐵𝑅𝐶 ∨ (𝐵 = 𝐶 ∨ 𝐶𝑅𝐵))) | |
13 | 11, 12 | sylib 217 | . . . 4 ⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵𝑅𝐶 ∨ (𝐵 = 𝐶 ∨ 𝐶𝑅𝐵))) |
14 | 13 | ord 863 | . . 3 ⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (¬ 𝐵𝑅𝐶 → (𝐵 = 𝐶 ∨ 𝐶𝑅𝐵))) |
15 | 10, 14 | impbid 211 | . 2 ⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ((𝐵 = 𝐶 ∨ 𝐶𝑅𝐵) ↔ ¬ 𝐵𝑅𝐶)) |
16 | 15 | con2bid 355 | 1 ⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵𝑅𝐶 ↔ ¬ (𝐵 = 𝐶 ∨ 𝐶𝑅𝐵))) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 397 ∨ wo 846 ∨ w3o 1087 = wceq 1542 ∈ wcel 2107 class class class wbr 5149 Or wor 5588 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3063 df-rab 3434 df-v 3477 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-br 5150 df-po 5589 df-so 5590 |
This theorem is referenced by: soasym 5620 sotr2 5621 sotr3 5628 sotri2 6131 sotri3 6132 somin1 6135 somincom 6136 soisores 7324 soisoi 7325 fimaxg 9290 suplub2 9456 supgtoreq 9465 fiming 9493 infsupprpr 9499 ordtypelem7 9519 fpwwe2 10638 indpi 10902 nqereu 10924 ltsonq 10964 prub 10989 ltapr 11040 suplem2pr 11048 ltsosr 11089 axpre-lttri 11160 noetasuplem4 27239 noetainflem4 27243 sleloe 27257 prproropf1olem4 46174 |
Copyright terms: Public domain | W3C validator |