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

Definition df-wetr 4365
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 4553). 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 4361 . 2  wff  R  We  A
41, 2wfr 4359 . . 3  wff  R  Fr  A
5 vx . . . . . . . . . 10  setvar  x
65cv 1363 . . . . . . . . 9  class  x
7 vy . . . . . . . . . 10  setvar  y
87cv 1363 . . . . . . . . 9  class  y
96, 8, 2wbr 4029 . . . . . . . 8  wff  x R y
10 vz . . . . . . . . . 10  setvar  z
1110cv 1363 . . . . . . . . 9  class  z
128, 11, 2wbr 4029 . . . . . . . 8  wff  y R z
139, 12wa 104 . . . . . . 7  wff  ( x R y  /\  y R z )
146, 11, 2wbr 4029 . . . . . . 7  wff  x R z
1513, 14wi 4 . . . . . 6  wff  ( ( x R y  /\  y R z )  ->  x R z )
1615, 10, 1wral 2472 . . . . 5  wff  A. z  e.  A  ( (
x R y  /\  y R z )  ->  x R z )
1716, 7, 1wral 2472 . . . 4  wff  A. y  e.  A  A. z  e.  A  ( (
x R y  /\  y R z )  ->  x R z )
1817, 5, 1wral 2472 . . 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 104 . 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 105 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  4386  weeq1  4387  weeq2  4388  wefr  4389  wepo  4390  wetrep  4391  we0  4392  ordwe  4608  wessep  4610  reg3exmidlemwe  4611
  Copyright terms: Public domain W3C validator