ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-wetr GIF version

Definition df-wetr 4124
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 4300). 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.)
Assertion
Ref Expression
df-wetr (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
Distinct variable groups:   𝑥,𝐴,𝑦,𝑧   𝑥,𝑅,𝑦,𝑧

Detailed syntax breakdown of Definition df-wetr
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cR . . 3 class 𝑅
31, 2wwe 4120 . 2 wff 𝑅 We 𝐴
41, 2wfr 4118 . . 3 wff 𝑅 Fr 𝐴
5 vx . . . . . . . . . 10 setvar 𝑥
65cv 1284 . . . . . . . . 9 class 𝑥
7 vy . . . . . . . . . 10 setvar 𝑦
87cv 1284 . . . . . . . . 9 class 𝑦
96, 8, 2wbr 3811 . . . . . . . 8 wff 𝑥𝑅𝑦
10 vz . . . . . . . . . 10 setvar 𝑧
1110cv 1284 . . . . . . . . 9 class 𝑧
128, 11, 2wbr 3811 . . . . . . . 8 wff 𝑦𝑅𝑧
139, 12wa 102 . . . . . . 7 wff (𝑥𝑅𝑦𝑦𝑅𝑧)
146, 11, 2wbr 3811 . . . . . . 7 wff 𝑥𝑅𝑧
1513, 14wi 4 . . . . . 6 wff ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)
1615, 10, 1wral 2353 . . . . 5 wff 𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)
1716, 7, 1wral 2353 . . . 4 wff 𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)
1817, 5, 1wral 2353 . . 3 wff 𝑥𝐴𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)
194, 18wa 102 . 2 wff (𝑅 Fr 𝐴 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
203, 19wb 103 1 wff (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
Colors of variables: wff set class
This definition is referenced by:  nfwe  4145  weeq1  4146  weeq2  4147  wefr  4148  wepo  4149  wetrep  4150  we0  4151  ordwe  4353  wessep  4355  reg3exmidlemwe  4356
  Copyright terms: Public domain W3C validator