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

Definition df-wetr 4117
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 4293). 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 4113 . 2  wff  R  We  A
41, 2wfr 4111 . . 3  wff  R  Fr  A
5 vx . . . . . . . . . 10  setvar  x
65cv 1284 . . . . . . . . 9  class  x
7 vy . . . . . . . . . 10  setvar  y
87cv 1284 . . . . . . . . 9  class  y
96, 8, 2wbr 3805 . . . . . . . 8  wff  x R y
10 vz . . . . . . . . . 10  setvar  z
1110cv 1284 . . . . . . . . 9  class  z
128, 11, 2wbr 3805 . . . . . . . 8  wff  y R z
139, 12wa 102 . . . . . . 7  wff  ( x R y  /\  y R z )
146, 11, 2wbr 3805 . . . . . . 7  wff  x R z
1513, 14wi 4 . . . . . 6  wff  ( ( x R y  /\  y R z )  ->  x R z )
1615, 10, 1wral 2353 . . . . 5  wff  A. z  e.  A  ( (
x R y  /\  y R z )  ->  x R z )
1716, 7, 1wral 2353 . . . 4  wff  A. y  e.  A  A. z  e.  A  ( (
x R y  /\  y R z )  ->  x R z )
1817, 5, 1wral 2353 . . 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  4138  weeq1  4139  weeq2  4140  wefr  4141  wepo  4142  wetrep  4143  we0  4144  ordwe  4346  wessep  4348  reg3exmidlemwe  4349
  Copyright terms: Public domain W3C validator