Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-iso | Unicode version |
Description: Define the strict linear order predicate. The expression is true if relationship orders . The property is called weak linearity by Proposition 11.2.3 of [HoTT], p. (varies). If we assumed excluded middle, it would be equivalent to trichotomy, . (Contributed by NM, 21-Jan-1996.) (Revised by Jim Kingdon, 4-Oct-2018.) |
Ref | Expression |
---|---|
df-iso |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | cR | . . 3 | |
3 | 1, 2 | wor 4032 | . 2 |
4 | 1, 2 | wpo 4031 | . . 3 |
5 | vx | . . . . . . . . 9 | |
6 | 5 | cv 1242 | . . . . . . . 8 |
7 | vy | . . . . . . . . 9 | |
8 | 7 | cv 1242 | . . . . . . . 8 |
9 | 6, 8, 2 | wbr 3764 | . . . . . . 7 |
10 | vz | . . . . . . . . . 10 | |
11 | 10 | cv 1242 | . . . . . . . . 9 |
12 | 6, 11, 2 | wbr 3764 | . . . . . . . 8 |
13 | 11, 8, 2 | wbr 3764 | . . . . . . . 8 |
14 | 12, 13 | wo 629 | . . . . . . 7 |
15 | 9, 14 | wi 4 | . . . . . 6 |
16 | 15, 10, 1 | wral 2306 | . . . . 5 |
17 | 16, 7, 1 | wral 2306 | . . . 4 |
18 | 17, 5, 1 | wral 2306 | . . 3 |
19 | 4, 18 | wa 97 | . 2 |
20 | 3, 19 | wb 98 | 1 |
Colors of variables: wff set class |
This definition is referenced by: nfso 4039 sopo 4050 soss 4051 soeq1 4052 issod 4056 sowlin 4057 so0 4063 ordsoexmid 4286 soinxp 4410 sosng 4413 cnvsom 4861 isosolem 5463 ltsopr 6694 ltsosr 6849 ltso 7096 xrltso 8717 |
Copyright terms: Public domain | W3C validator |