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

Definition df-fr 4509
Description: Define the well-founded relation predicate. Definition 6.24(1) of [TakeutiZaring] p. 30. For alternate definitions, see dffr2 4515 and dffr3 5203. (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 4506 . 2  wff  R  Fr  A
4 vx . . . . . . 7  set  x
54cv 1648 . . . . . 6  class  x
65, 1wss 3288 . . . . 5  wff  x  C_  A
7 c0 3596 . . . . . 6  class  (/)
85, 7wne 2575 . . . . 5  wff  x  =/=  (/)
96, 8wa 359 . . . 4  wff  ( x 
C_  A  /\  x  =/=  (/) )
10 vz . . . . . . . . 9  set  z
1110cv 1648 . . . . . . . 8  class  z
12 vy . . . . . . . . 9  set  y
1312cv 1648 . . . . . . . 8  class  y
1411, 13, 2wbr 4180 . . . . . . 7  wff  z R y
1514wn 3 . . . . . 6  wff  -.  z R y
1615, 10, 5wral 2674 . . . . 5  wff  A. z  e.  x  -.  z R y
1716, 12, 5wrex 2675 . . . 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 1546 . 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  4512  dffr2  4515  frss  4517  freq1  4520  nffr  4524  frinxp  4910  frsn  4915  f1oweALT  6041  frxp  6423  frfi  7319  fpwwe2lem12  8480  fpwwe2lem13  8481  dffr5  25332  dfon2lem9  25369  fnwe2  27026  bnj1154  29086
  Copyright terms: Public domain W3C validator