![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-wetr | Unicode version |
Description: Define the well-ordering
predicate. It is unusual to define
"well-ordering" in the absence of excluded middle, but we mean
an
ordering which is like the ordering which we have for ordinals (for
example, it does not entail trichotomy because ordinals do not have that
as seen at ordtriexmid 4553). Given excluded middle, well-ordering is
usually defined to require trichotomy (and the definition of ![]() |
Ref | Expression |
---|---|
df-wetr |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA |
. . 3
![]() ![]() | |
2 | cR |
. . 3
![]() ![]() | |
3 | 1, 2 | wwe 4361 |
. 2
![]() ![]() ![]() ![]() |
4 | 1, 2 | wfr 4359 |
. . 3
![]() ![]() ![]() ![]() |
5 | vx |
. . . . . . . . . 10
![]() ![]() | |
6 | 5 | cv 1363 |
. . . . . . . . 9
![]() ![]() |
7 | vy |
. . . . . . . . . 10
![]() ![]() | |
8 | 7 | cv 1363 |
. . . . . . . . 9
![]() ![]() |
9 | 6, 8, 2 | wbr 4029 |
. . . . . . . 8
![]() ![]() ![]() ![]() |
10 | vz |
. . . . . . . . . 10
![]() ![]() | |
11 | 10 | cv 1363 |
. . . . . . . . 9
![]() ![]() |
12 | 8, 11, 2 | wbr 4029 |
. . . . . . . 8
![]() ![]() ![]() ![]() |
13 | 9, 12 | wa 104 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
14 | 6, 11, 2 | wbr 4029 |
. . . . . . 7
![]() ![]() ![]() ![]() |
15 | 13, 14 | wi 4 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | 15, 10, 1 | wral 2472 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
17 | 16, 7, 1 | wral 2472 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
18 | 17, 5, 1 | wral 2472 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
19 | 4, 18 | wa 104 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
20 | 3, 19 | wb 105 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: nfwe 4386 weeq1 4387 weeq2 4388 wefr 4389 wepo 4390 wetrep 4391 we0 4392 ordwe 4608 wessep 4610 reg3exmidlemwe 4611 |
Copyright terms: Public domain | W3C validator |