![]() |
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 11281). 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 5583 | . 2 wff 𝑅 Or 𝐴 |
4 | 1, 2 | wpo 5582 | . . 3 wff 𝑅 Po 𝐴 |
5 | vx | . . . . . . . 8 setvar 𝑥 | |
6 | 5 | cv 1541 | . . . . . . 7 class 𝑥 |
7 | vy | . . . . . . . 8 setvar 𝑦 | |
8 | 7 | cv 1541 | . . . . . . 7 class 𝑦 |
9 | 6, 8, 2 | wbr 5144 | . . . . . 6 wff 𝑥𝑅𝑦 |
10 | 5, 7 | weq 1967 | . . . . . 6 wff 𝑥 = 𝑦 |
11 | 8, 6, 2 | wbr 5144 | . . . . . 6 wff 𝑦𝑅𝑥 |
12 | 9, 10, 11 | w3o 1087 | . . . . 5 wff (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) |
13 | 12, 7, 1 | wral 3062 | . . . 4 wff ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) |
14 | 13, 5, 1 | wral 3062 | . . 3 wff ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) |
15 | 4, 14 | wa 397 | . 2 wff (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) |
16 | 3, 15 | wb 205 | 1 wff (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) |
Colors of variables: wff setvar class |
This definition is referenced by: nfso 5590 sopo 5603 soss 5604 soeq1 5605 solin 5609 issod 5617 so0 5620 soinxp 5752 sosn 5757 cnvso 6279 isosolem 7331 sorpss 7705 dfwe2 7748 epweon 7749 soxp 8102 soseq 8132 sornom 10259 zorn2lem6 10483 tosso 18359 dfso3 34620 dfso2 34656 |
Copyright terms: Public domain | W3C validator |