![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-wetr | GIF 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 don't have that as seen at ordtriexmid 4351). Given excluded middle, well-ordering is usually defined to require trichotomy (and the defintion of Fr is typically also different). (Contributed by Mario Carneiro and Jim Kingdon, 23-Sep-2021.) |
Ref | Expression |
---|---|
df-wetr | ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cR | . . 3 class 𝑅 | |
3 | 1, 2 | wwe 4166 | . 2 wff 𝑅 We 𝐴 |
4 | 1, 2 | wfr 4164 | . . 3 wff 𝑅 Fr 𝐴 |
5 | vx | . . . . . . . . . 10 setvar 𝑥 | |
6 | 5 | cv 1289 | . . . . . . . . 9 class 𝑥 |
7 | vy | . . . . . . . . . 10 setvar 𝑦 | |
8 | 7 | cv 1289 | . . . . . . . . 9 class 𝑦 |
9 | 6, 8, 2 | wbr 3851 | . . . . . . . 8 wff 𝑥𝑅𝑦 |
10 | vz | . . . . . . . . . 10 setvar 𝑧 | |
11 | 10 | cv 1289 | . . . . . . . . 9 class 𝑧 |
12 | 8, 11, 2 | wbr 3851 | . . . . . . . 8 wff 𝑦𝑅𝑧 |
13 | 9, 12 | wa 103 | . . . . . . 7 wff (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) |
14 | 6, 11, 2 | wbr 3851 | . . . . . . 7 wff 𝑥𝑅𝑧 |
15 | 13, 14 | wi 4 | . . . . . 6 wff ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) |
16 | 15, 10, 1 | wral 2360 | . . . . 5 wff ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) |
17 | 16, 7, 1 | wral 2360 | . . . 4 wff ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) |
18 | 17, 5, 1 | wral 2360 | . . 3 wff ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) |
19 | 4, 18 | wa 103 | . 2 wff (𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) |
20 | 3, 19 | wb 104 | 1 wff (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))) |
Colors of variables: wff set class |
This definition is referenced by: nfwe 4191 weeq1 4192 weeq2 4193 wefr 4194 wepo 4195 wetrep 4196 we0 4197 ordwe 4404 wessep 4406 reg3exmidlemwe 4407 |
Copyright terms: Public domain | W3C validator |