| 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 5593 | . 2 ⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) | |
| 2 | 1 | simplbi 497 | 1 ⊢ (𝑅 Or 𝐴 → 𝑅 Po 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∨ w3o 1086 ∀wral 3061 class class class wbr 5143 Po wpo 5590 Or wor 5591 |
| 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 207 df-an 396 df-so 5593 |
| This theorem is referenced by: sonr 5616 sotr 5617 so2nr 5620 so3nr 5621 soltmin 6156 predso 6345 tz6.26 6368 wfi 6371 wfisg 6374 wfis2fg 6377 soxp 8154 soseq 8184 wfrfun 8372 wfrresex 8373 wfr2a 8374 wfr1 8375 on2recsfn 8705 on2recsov 8706 on2ind 8707 on3ind 8708 fimax2g 9322 wofi 9325 fimin2g 9537 ordtypelem8 9565 wemaplem2 9587 wemapsolem 9590 cantnf 9733 fin23lem27 10368 iccpnfhmeo 24976 xrhmeo 24977 logccv 26705 ex-po 30454 xrge0iifiso 33934 weiunso 36467 incsequz2 37756 epirron 43266 oneptr 43267 prproropf1olem1 47490 |
| Copyright terms: Public domain | W3C validator |