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

Definition df-wetr 4226
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  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 4222 . 2  wff  R  We  A
41, 2wfr 4220 . . 3  wff  R  Fr  A
5 vx . . . . . . . . . 10  setvar  x
65cv 1315 . . . . . . . . 9  class  x
7 vy . . . . . . . . . 10  setvar  y
87cv 1315 . . . . . . . . 9  class  y
96, 8, 2wbr 3899 . . . . . . . 8  wff  x R y
10 vz . . . . . . . . . 10  setvar  z
1110cv 1315 . . . . . . . . 9  class  z
128, 11, 2wbr 3899 . . . . . . . 8  wff  y R z
139, 12wa 103 . . . . . . 7  wff  ( x R y  /\  y R z )
146, 11, 2wbr 3899 . . . . . . 7  wff  x R z
1513, 14wi 4 . . . . . 6  wff  ( ( x R y  /\  y R z )  ->  x R z )
1615, 10, 1wral 2393 . . . . 5  wff  A. z  e.  A  ( (
x R y  /\  y R z )  ->  x R z )
1716, 7, 1wral 2393 . . . 4  wff  A. y  e.  A  A. z  e.  A  ( (
x R y  /\  y R z )  ->  x R z )
1817, 5, 1wral 2393 . . 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 103 . 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 104 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  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