MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-fr Unicode version

Definition df-fr 4289
Description: Define the well-founded relation predicate. Definition 6.24(1) of [TakeutiZaring] p. 30. For alternate definitions, see dffr2 4295 and dffr3 4998. (Contributed by NM, 3-Apr-1994.)
Assertion
Ref Expression
df-fr  |-  ( R  Fr  A  <->  A. x
( ( x  C_  A  /\  x  =/=  (/) )  ->  E. y  e.  x  A. z  e.  x  -.  z R y ) )
Distinct variable groups:    x, y,
z, R    x, A, y, z

Detailed syntax breakdown of Definition df-fr
StepHypRef Expression
1 cA . . 3  class  A
2 cR . . 3  class  R
31, 2wfr 4286 . 2  wff  R  Fr  A
4 vx . . . . . . 7  set  x
54cv 1618 . . . . . 6  class  x
65, 1wss 3094 . . . . 5  wff  x  C_  A
7 c0 3397 . . . . . 6  class  (/)
85, 7wne 2419 . . . . 5  wff  x  =/=  (/)
96, 8wa 360 . . . 4  wff  ( x 
C_  A  /\  x  =/=  (/) )
10 vz . . . . . . . . 9  set  z
1110cv 1618 . . . . . . . 8  class  z
12 vy . . . . . . . . 9  set  y
1312cv 1618 . . . . . . . 8  class  y
1411, 13, 2wbr 3963 . . . . . . 7  wff  z R y
1514wn 5 . . . . . 6  wff  -.  z R y
1615, 10, 5wral 2516 . . . . 5  wff  A. z  e.  x  -.  z R y
1716, 12, 5wrex 2517 . . . 4  wff  E. y  e.  x  A. z  e.  x  -.  z R y
189, 17wi 6 . . 3  wff  ( ( x  C_  A  /\  x  =/=  (/) )  ->  E. y  e.  x  A. z  e.  x  -.  z R y )
1918, 4wal 1532 . 2  wff  A. x
( ( x  C_  A  /\  x  =/=  (/) )  ->  E. y  e.  x  A. z  e.  x  -.  z R y )
203, 19wb 178 1  wff  ( R  Fr  A  <->  A. x
( ( x  C_  A  /\  x  =/=  (/) )  ->  E. y  e.  x  A. z  e.  x  -.  z R y ) )
Colors of variables: wff set class
This definition is referenced by:  fri  4292  dffr2  4295  frss  4297  freq1  4300  nffr  4304  frinxp  4708  frsn  4713  f1oweALT  5750  frxp  6124  frfi  7035  fpwwe2lem12  8196  fpwwe2lem13  8197  dffr5  23446  dfon2lem9  23481  fnwe2  26482  bnj1154  28041
  Copyright terms: Public domain W3C validator