![]() |
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 4297 |
. 2
![]() ![]() ![]() ![]() |
4 | 1, 2 | wpo 4296 |
. . 3
![]() ![]() ![]() ![]() |
5 | vx |
. . . . . . . . 9
![]() ![]() | |
6 | 5 | cv 1352 |
. . . . . . . 8
![]() ![]() |
7 | vy |
. . . . . . . . 9
![]() ![]() | |
8 | 7 | cv 1352 |
. . . . . . . 8
![]() ![]() |
9 | 6, 8, 2 | wbr 4005 |
. . . . . . 7
![]() ![]() ![]() ![]() |
10 | vz |
. . . . . . . . . 10
![]() ![]() | |
11 | 10 | cv 1352 |
. . . . . . . . 9
![]() ![]() |
12 | 6, 11, 2 | wbr 4005 |
. . . . . . . 8
![]() ![]() ![]() ![]() |
13 | 11, 8, 2 | wbr 4005 |
. . . . . . . 8
![]() ![]() ![]() ![]() |
14 | 12, 13 | wo 708 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | 9, 14 | wi 4 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | 15, 10, 1 | wral 2455 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
17 | 16, 7, 1 | wral 2455 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
18 | 17, 5, 1 | wral 2455 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
19 | 4, 18 | wa 104 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
20 | 3, 19 | wb 105 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: nfso 4304 sopo 4315 soss 4316 soeq1 4317 issod 4321 sowlin 4322 so0 4328 ordsoexmid 4563 soinxp 4698 sosng 4701 cnvsom 5174 isosolem 5828 ltsopr 7598 ltsosr 7766 ltso 8038 xrltso 9799 |
Copyright terms: Public domain | W3C validator |