![]() |
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 11294). 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 5588 | . 2 wff 𝑅 Or 𝐴 |
4 | 1, 2 | wpo 5587 | . . 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 5149 | . . . . . 6 wff 𝑥𝑅𝑦 |
10 | 5, 7 | weq 1967 | . . . . . 6 wff 𝑥 = 𝑦 |
11 | 8, 6, 2 | wbr 5149 | . . . . . 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 5595 sopo 5608 soss 5609 soeq1 5610 solin 5614 issod 5622 so0 5625 soinxp 5758 sosn 5763 cnvso 6288 isosolem 7344 sorpss 7718 dfwe2 7761 epweon 7762 soxp 8115 soseq 8145 sornom 10272 zorn2lem6 10496 tosso 18372 dfso3 34689 dfso2 34725 |
Copyright terms: Public domain | W3C validator |