![]() |
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 ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
df-iso |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA |
. . 3
![]() ![]() | |
2 | cR |
. . 3
![]() ![]() | |
3 | 1, 2 | wor 4023 |
. 2
![]() ![]() ![]() ![]() |
4 | 1, 2 | wpo 4022 |
. . 3
![]() ![]() ![]() ![]() |
5 | vx |
. . . . . . . . 9
![]() ![]() | |
6 | 5 | cv 1241 |
. . . . . . . 8
![]() ![]() |
7 | vy |
. . . . . . . . 9
![]() ![]() | |
8 | 7 | cv 1241 |
. . . . . . . 8
![]() ![]() |
9 | 6, 8, 2 | wbr 3755 |
. . . . . . 7
![]() ![]() ![]() ![]() |
10 | vz |
. . . . . . . . . 10
![]() ![]() | |
11 | 10 | cv 1241 |
. . . . . . . . 9
![]() ![]() |
12 | 6, 11, 2 | wbr 3755 |
. . . . . . . 8
![]() ![]() ![]() ![]() |
13 | 11, 8, 2 | wbr 3755 |
. . . . . . . 8
![]() ![]() ![]() ![]() |
14 | 12, 13 | wo 628 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | 9, 14 | wi 4 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | 15, 10, 1 | wral 2300 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
17 | 16, 7, 1 | wral 2300 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
18 | 17, 5, 1 | wral 2300 |
. . 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 4030 sopo 4041 soss 4042 soeq1 4043 issod 4047 sowlin 4048 so0 4054 ordsoexmid 4240 soinxp 4353 sosng 4356 cnvsom 4804 isosolem 5406 ltsopr 6570 ltsosr 6692 ltso 6893 xrltso 8487 |
Copyright terms: Public domain | W3C validator |