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

Definition df-fr 4533
Description: Define the well-founded relation predicate. Definition 6.24(1) of [TakeutiZaring] p. 30. For alternate definitions, see dffr2 4539 and dffr3 5227. (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 4530 . 2  wff  R  Fr  A
4 vx . . . . . . 7  set  x
54cv 1651 . . . . . 6  class  x
65, 1wss 3312 . . . . 5  wff  x  C_  A
7 c0 3620 . . . . . 6  class  (/)
85, 7wne 2598 . . . . 5  wff  x  =/=  (/)
96, 8wa 359 . . . 4  wff  ( x 
C_  A  /\  x  =/=  (/) )
10 vz . . . . . . . . 9  set  z
1110cv 1651 . . . . . . . 8  class  z
12 vy . . . . . . . . 9  set  y
1312cv 1651 . . . . . . . 8  class  y
1411, 13, 2wbr 4204 . . . . . . 7  wff  z R y
1514wn 3 . . . . . 6  wff  -.  z R y
1615, 10, 5wral 2697 . . . . 5  wff  A. z  e.  x  -.  z R y
1716, 12, 5wrex 2698 . . . 4  wff  E. y  e.  x  A. z  e.  x  -.  z R y
189, 17wi 4 . . 3  wff  ( ( x  C_  A  /\  x  =/=  (/) )  ->  E. y  e.  x  A. z  e.  x  -.  z R y )
1918, 4wal 1549 . 2  wff  A. x
( ( x  C_  A  /\  x  =/=  (/) )  ->  E. y  e.  x  A. z  e.  x  -.  z R y )
203, 19wb 177 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  4536  dffr2  4539  frss  4541  freq1  4544  nffr  4548  frinxp  4934  frsn  4939  f1oweALT  6065  frxp  6447  frfi  7343  fpwwe2lem12  8505  fpwwe2lem13  8506  dffr5  25365  dfon2lem9  25402  fnwe2  27065  bnj1154  29222
  Copyright terms: Public domain W3C validator