Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > sopo | Structured version Visualization version GIF version |
Description: A strict linear order is a strict partial order. (Contributed by NM, 28-Mar-1997.) |
Ref | Expression |
---|---|
sopo | ⊢ (𝑅 Or 𝐴 → 𝑅 Po 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-so 5036 | . 2 ⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) | |
2 | 1 | simplbi 476 | 1 ⊢ (𝑅 Or 𝐴 → 𝑅 Po 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ w3o 1036 ∀wral 2912 class class class wbr 4653 Po wpo 5033 Or wor 5034 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 df-an 386 df-so 5036 |
This theorem is referenced by: sonr 5056 sotr 5057 so2nr 5059 so3nr 5060 soltmin 5532 predso 5699 soxp 7290 fimax2g 8206 wofi 8209 fimin2g 8403 ordtypelem8 8430 wemaplem2 8452 wemapsolem 8455 cantnf 8590 fin23lem27 9150 iccpnfhmeo 22744 xrhmeo 22745 logccv 24409 ex-po 27292 xrge0iifiso 29981 soseq 31751 incsequz2 33545 |
Copyright terms: Public domain | W3C validator |