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

Definition df-wetr 4161
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 4338). 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  |-  ( R  We  A  <->  ( R  Fr  A  /\  A. x  e.  A  A. y  e.  A  A. z  e.  A  ( (
x R y  /\  y R z )  ->  x R z ) ) )
Distinct variable groups:    x, A, y, z    x, R, y, z

Detailed syntax breakdown of Definition df-wetr
StepHypRef Expression
1 cA . . 3  class  A
2 cR . . 3  class  R
31, 2wwe 4157 . 2  wff  R  We  A
41, 2wfr 4155 . . 3  wff  R  Fr  A
5 vx . . . . . . . . . 10  setvar  x
65cv 1288 . . . . . . . . 9  class  x
7 vy . . . . . . . . . 10  setvar  y
87cv 1288 . . . . . . . . 9  class  y
96, 8, 2wbr 3845 . . . . . . . 8  wff  x R y
10 vz . . . . . . . . . 10  setvar  z
1110cv 1288 . . . . . . . . 9  class  z
128, 11, 2wbr 3845 . . . . . . . 8  wff  y R z
139, 12wa 102 . . . . . . 7  wff  ( x R y  /\  y R z )
146, 11, 2wbr 3845 . . . . . . 7  wff  x R z
1513, 14wi 4 . . . . . 6  wff  ( ( x R y  /\  y R z )  ->  x R z )
1615, 10, 1wral 2359 . . . . 5  wff  A. z  e.  A  ( (
x R y  /\  y R z )  ->  x R z )
1716, 7, 1wral 2359 . . . 4  wff  A. y  e.  A  A. z  e.  A  ( (
x R y  /\  y R z )  ->  x R z )
1817, 5, 1wral 2359 . . 3  wff  A. x  e.  A  A. y  e.  A  A. z  e.  A  ( (
x R y  /\  y R z )  ->  x R z )
194, 18wa 102 . 2  wff  ( R  Fr  A  /\  A. x  e.  A  A. y  e.  A  A. z  e.  A  (
( x R y  /\  y R z )  ->  x R
z ) )
203, 19wb 103 1  wff  ( R  We  A  <->  ( R  Fr  A  /\  A. x  e.  A  A. y  e.  A  A. z  e.  A  ( (
x R y  /\  y R z )  ->  x R z ) ) )
Colors of variables: wff set class
This definition is referenced by:  nfwe  4182  weeq1  4183  weeq2  4184  wefr  4185  wepo  4186  wetrep  4187  we0  4188  ordwe  4391  wessep  4393  reg3exmidlemwe  4394
  Copyright terms: Public domain W3C validator