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

Definition df-fr 4324
Description: Define the well-founded relation predicate. Definition 6.24(1) of [TakeutiZaring] p. 30. For alternate definitions, see dffr2 4330 and dffr3 5033. (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 4321 . 2  wff  R  Fr  A
4 vx . . . . . . 7  set  x
54cv 1618 . . . . . 6  class  x
65, 1wss 3127 . . . . 5  wff  x  C_  A
7 c0 3430 . . . . . 6  class  (/)
85, 7wne 2421 . . . . 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 3997 . . . . . . 7  wff  z R y
1514wn 5 . . . . . 6  wff  -.  z R y
1615, 10, 5wral 2518 . . . . 5  wff  A. z  e.  x  -.  z R y
1716, 12, 5wrex 2519 . . . 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  4327  dffr2  4330  frss  4332  freq1  4335  nffr  4339  frinxp  4743  frsn  4748  f1oweALT  5785  frxp  6159  frfi  7070  fpwwe2lem12  8231  fpwwe2lem13  8232  dffr5  23482  dfon2lem9  23517  fnwe2  26518  bnj1154  28161
  Copyright terms: Public domain W3C validator