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 10710). 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 5467 | . 2 wff 𝑅 Or 𝐴 |
4 | 1, 2 | wpo 5466 | . . 3 wff 𝑅 Po 𝐴 |
5 | vx | . . . . . . . 8 setvar 𝑥 | |
6 | 5 | cv 1527 | . . . . . . 7 class 𝑥 |
7 | vy | . . . . . . . 8 setvar 𝑦 | |
8 | 7 | cv 1527 | . . . . . . 7 class 𝑦 |
9 | 6, 8, 2 | wbr 5058 | . . . . . 6 wff 𝑥𝑅𝑦 |
10 | 5, 7 | weq 1955 | . . . . . 6 wff 𝑥 = 𝑦 |
11 | 8, 6, 2 | wbr 5058 | . . . . . 6 wff 𝑦𝑅𝑥 |
12 | 9, 10, 11 | w3o 1078 | . . . . 5 wff (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) |
13 | 12, 7, 1 | wral 3138 | . . . 4 wff ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) |
14 | 13, 5, 1 | wral 3138 | . . 3 wff ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) |
15 | 4, 14 | wa 396 | . 2 wff (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) |
16 | 3, 15 | wb 207 | 1 wff (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) |
Colors of variables: wff setvar class |
This definition is referenced by: nfso 5474 sopo 5486 soss 5487 soeq1 5488 solin 5492 issod 5500 so0 5503 soinxp 5627 sosn 5632 cnvso 6133 isosolem 7089 sorpss 7443 dfwe2 7484 soxp 7814 sornom 9688 zorn2lem6 9912 tosso 17636 dfso3 32848 dfso2 32888 soseq 32994 |
Copyright terms: Public domain | W3C validator |