![]() |
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 4177 |
. 2
![]() ![]() ![]() ![]() |
4 | 1, 2 | wpo 4176 |
. . 3
![]() ![]() ![]() ![]() |
5 | vx |
. . . . . . . . 9
![]() ![]() | |
6 | 5 | cv 1313 |
. . . . . . . 8
![]() ![]() |
7 | vy |
. . . . . . . . 9
![]() ![]() | |
8 | 7 | cv 1313 |
. . . . . . . 8
![]() ![]() |
9 | 6, 8, 2 | wbr 3895 |
. . . . . . 7
![]() ![]() ![]() ![]() |
10 | vz |
. . . . . . . . . 10
![]() ![]() | |
11 | 10 | cv 1313 |
. . . . . . . . 9
![]() ![]() |
12 | 6, 11, 2 | wbr 3895 |
. . . . . . . 8
![]() ![]() ![]() ![]() |
13 | 11, 8, 2 | wbr 3895 |
. . . . . . . 8
![]() ![]() ![]() ![]() |
14 | 12, 13 | wo 680 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | 9, 14 | wi 4 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | 15, 10, 1 | wral 2390 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
17 | 16, 7, 1 | wral 2390 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
18 | 17, 5, 1 | wral 2390 |
. . 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 4184 sopo 4195 soss 4196 soeq1 4197 issod 4201 sowlin 4202 so0 4208 ordsoexmid 4437 soinxp 4569 sosng 4572 cnvsom 5040 isosolem 5679 ltsopr 7352 ltsosr 7507 ltso 7765 xrltso 9475 |
Copyright terms: Public domain | W3C validator |