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 11064). 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 5503 | . 2 wff 𝑅 Or 𝐴 |
4 | 1, 2 | wpo 5502 | . . 3 wff 𝑅 Po 𝐴 |
5 | vx | . . . . . . . 8 setvar 𝑥 | |
6 | 5 | cv 1538 | . . . . . . 7 class 𝑥 |
7 | vy | . . . . . . . 8 setvar 𝑦 | |
8 | 7 | cv 1538 | . . . . . . 7 class 𝑦 |
9 | 6, 8, 2 | wbr 5075 | . . . . . 6 wff 𝑥𝑅𝑦 |
10 | 5, 7 | weq 1967 | . . . . . 6 wff 𝑥 = 𝑦 |
11 | 8, 6, 2 | wbr 5075 | . . . . . 6 wff 𝑦𝑅𝑥 |
12 | 9, 10, 11 | w3o 1085 | . . . . 5 wff (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) |
13 | 12, 7, 1 | wral 3065 | . . . 4 wff ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) |
14 | 13, 5, 1 | wral 3065 | . . 3 wff ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) |
15 | 4, 14 | wa 396 | . 2 wff (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) |
16 | 3, 15 | wb 205 | 1 wff (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) |
Colors of variables: wff setvar class |
This definition is referenced by: nfso 5510 sopo 5523 soss 5524 soeq1 5525 solin 5529 issod 5537 so0 5540 soinxp 5669 sosn 5674 cnvso 6195 isosolem 7227 sorpss 7590 dfwe2 7633 epweon 7634 soxp 7979 sornom 10042 zorn2lem6 10266 tosso 18146 dfso3 33673 dfso2 33731 soseq 33812 |
Copyright terms: Public domain | W3C validator |