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 4407). Given excluded middle, well-ordering is usually defined to require trichotomy (and the definition of is typically also different). (Contributed by Mario Carneiro and Jim Kingdon, 23-Sep-2021.) |
Ref | Expression |
---|---|
df-wetr |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | cR | . . 3 | |
3 | 1, 2 | wwe 4222 | . 2 |
4 | 1, 2 | wfr 4220 | . . 3 |
5 | vx | . . . . . . . . . 10 | |
6 | 5 | cv 1315 | . . . . . . . . 9 |
7 | vy | . . . . . . . . . 10 | |
8 | 7 | cv 1315 | . . . . . . . . 9 |
9 | 6, 8, 2 | wbr 3899 | . . . . . . . 8 |
10 | vz | . . . . . . . . . 10 | |
11 | 10 | cv 1315 | . . . . . . . . 9 |
12 | 8, 11, 2 | wbr 3899 | . . . . . . . 8 |
13 | 9, 12 | wa 103 | . . . . . . 7 |
14 | 6, 11, 2 | wbr 3899 | . . . . . . 7 |
15 | 13, 14 | wi 4 | . . . . . 6 |
16 | 15, 10, 1 | wral 2393 | . . . . 5 |
17 | 16, 7, 1 | wral 2393 | . . . 4 |
18 | 17, 5, 1 | wral 2393 | . . 3 |
19 | 4, 18 | wa 103 | . 2 |
20 | 3, 19 | wb 104 | 1 |
Colors of variables: wff set class |
This definition is referenced by: nfwe 4247 weeq1 4248 weeq2 4249 wefr 4250 wepo 4251 wetrep 4252 we0 4253 ordwe 4460 wessep 4462 reg3exmidlemwe 4463 |
Copyright terms: Public domain | W3C validator |