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 9997). 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 4958 | . 2 wff 𝑅 Or 𝐴 |
4 | 1, 2 | wpo 4957 | . . 3 wff 𝑅 Po 𝐴 |
5 | vx | . . . . . . . 8 setvar 𝑥 | |
6 | 5 | cv 1474 | . . . . . . 7 class 𝑥 |
7 | vy | . . . . . . . 8 setvar 𝑦 | |
8 | 7 | cv 1474 | . . . . . . 7 class 𝑦 |
9 | 6, 8, 2 | wbr 4583 | . . . . . 6 wff 𝑥𝑅𝑦 |
10 | 5, 7 | weq 1861 | . . . . . 6 wff 𝑥 = 𝑦 |
11 | 8, 6, 2 | wbr 4583 | . . . . . 6 wff 𝑦𝑅𝑥 |
12 | 9, 10, 11 | w3o 1030 | . . . . 5 wff (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) |
13 | 12, 7, 1 | wral 2896 | . . . 4 wff ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) |
14 | 13, 5, 1 | wral 2896 | . . 3 wff ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) |
15 | 4, 14 | wa 383 | . 2 wff (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) |
16 | 3, 15 | wb 195 | 1 wff (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) |
Colors of variables: wff setvar class |
This definition is referenced by: nfso 4965 sopo 4976 soss 4977 soeq1 4978 solin 4982 issod 4989 so0 4992 soinxp 5106 sosn 5111 cnvso 5591 isosolem 6497 sorpss 6840 dfwe2 6873 soxp 7177 sornom 8982 zorn2lem6 9206 tosso 16859 dfso3 30856 dfso2 30897 soseq 30995 |
Copyright terms: Public domain | W3C validator |