![]() |
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 4079 |
. 2
![]() ![]() ![]() ![]() |
4 | 1, 2 | wpo 4078 |
. . 3
![]() ![]() ![]() ![]() |
5 | vx |
. . . . . . . . 9
![]() ![]() | |
6 | 5 | cv 1284 |
. . . . . . . 8
![]() ![]() |
7 | vy |
. . . . . . . . 9
![]() ![]() | |
8 | 7 | cv 1284 |
. . . . . . . 8
![]() ![]() |
9 | 6, 8, 2 | wbr 3806 |
. . . . . . 7
![]() ![]() ![]() ![]() |
10 | vz |
. . . . . . . . . 10
![]() ![]() | |
11 | 10 | cv 1284 |
. . . . . . . . 9
![]() ![]() |
12 | 6, 11, 2 | wbr 3806 |
. . . . . . . 8
![]() ![]() ![]() ![]() |
13 | 11, 8, 2 | wbr 3806 |
. . . . . . . 8
![]() ![]() ![]() ![]() |
14 | 12, 13 | wo 662 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | 9, 14 | wi 4 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | 15, 10, 1 | wral 2353 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
17 | 16, 7, 1 | wral 2353 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
18 | 17, 5, 1 | wral 2353 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
19 | 4, 18 | wa 102 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
20 | 3, 19 | wb 103 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: nfso 4086 sopo 4097 soss 4098 soeq1 4099 issod 4103 sowlin 4104 so0 4110 ordsoexmid 4334 soinxp 4457 sosng 4460 cnvsom 4912 isosolem 5516 ltsopr 6925 ltsosr 7080 ltso 7333 xrltso 9024 |
Copyright terms: Public domain | W3C validator |