| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > df-so | Structured version Visualization version GIF version | ||
| Description: Define the strict complete (linear) order predicate. The expression 𝑅 Or 𝐴 is true if relationship 𝑅 orders 𝐴. For example, < Or ℝ is true (ltso 11341). Equivalent to Definition 6.19(1) of [TakeutiZaring] p. 29. (Contributed by NM, 21-Jan-1996.) |
| Ref | Expression |
|---|---|
| df-so | ⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cA | . . 3 class 𝐴 | |
| 2 | cR | . . 3 class 𝑅 | |
| 3 | 1, 2 | wor 5591 | . 2 wff 𝑅 Or 𝐴 |
| 4 | 1, 2 | wpo 5590 | . . 3 wff 𝑅 Po 𝐴 |
| 5 | vx | . . . . . . . 8 setvar 𝑥 | |
| 6 | 5 | cv 1539 | . . . . . . 7 class 𝑥 |
| 7 | vy | . . . . . . . 8 setvar 𝑦 | |
| 8 | 7 | cv 1539 | . . . . . . 7 class 𝑦 |
| 9 | 6, 8, 2 | wbr 5143 | . . . . . 6 wff 𝑥𝑅𝑦 |
| 10 | 5, 7 | weq 1962 | . . . . . 6 wff 𝑥 = 𝑦 |
| 11 | 8, 6, 2 | wbr 5143 | . . . . . 6 wff 𝑦𝑅𝑥 |
| 12 | 9, 10, 11 | w3o 1086 | . . . . 5 wff (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) |
| 13 | 12, 7, 1 | wral 3061 | . . . 4 wff ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) |
| 14 | 13, 5, 1 | wral 3061 | . . 3 wff ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) |
| 15 | 4, 14 | wa 395 | . 2 wff (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) |
| 16 | 3, 15 | wb 206 | 1 wff (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) |
| Colors of variables: wff setvar class |
| This definition is referenced by: nfso 5599 sopo 5611 soss 5612 soeq1 5613 solin 5619 issod 5627 so0 5630 soinxp 5767 sosn 5772 cnvso 6308 isosolem 7367 sorpss 7748 dfwe2 7794 epweon 7795 soxp 8154 soseq 8184 sornom 10317 zorn2lem6 10541 tosso 18464 dfso3 35720 dfso2 35755 |
| Copyright terms: Public domain | W3C validator |