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 4187 | . 2 |
4 | 1, 2 | wpo 4186 | . . 3 |
5 | vx | . . . . . . . . 9 | |
6 | 5 | cv 1315 | . . . . . . . 8 |
7 | vy | . . . . . . . . 9 | |
8 | 7 | cv 1315 | . . . . . . . 8 |
9 | 6, 8, 2 | wbr 3899 | . . . . . . 7 |
10 | vz | . . . . . . . . . 10 | |
11 | 10 | cv 1315 | . . . . . . . . 9 |
12 | 6, 11, 2 | wbr 3899 | . . . . . . . 8 |
13 | 11, 8, 2 | wbr 3899 | . . . . . . . 8 |
14 | 12, 13 | wo 682 | . . . . . . 7 |
15 | 9, 14 | wi 4 | . . . . . 6 |
16 | 15, 10, 1 | wral 2393 | . . . . 5 |
17 | 16, 7, 1 | wral 2393 | . . . 4 |
18 | 17, 5, 1 | wral 2393 | . . 3 |
19 | 4, 18 | wa 103 | . 2 |
20 | 3, 19 | wb 104 | 1 |
Colors of variables: wff set class |
This definition is referenced by: nfso 4194 sopo 4205 soss 4206 soeq1 4207 issod 4211 sowlin 4212 so0 4218 ordsoexmid 4447 soinxp 4579 sosng 4582 cnvsom 5052 isosolem 5693 ltsopr 7372 ltsosr 7540 ltso 7810 xrltso 9537 |
Copyright terms: Public domain | W3C validator |