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

Definition df-fr 4352
Description: Define the well-founded relation predicate. Definition 6.24(1) of [TakeutiZaring] p. 30. For alternate definitions, see dffr2 4358 and dffr3 5045. (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 4349 . 2  wff  R  Fr  A
4 vx . . . . . . 7  set  x
54cv 1622 . . . . . 6  class  x
65, 1wss 3152 . . . . 5  wff  x  C_  A
7 c0 3455 . . . . . 6  class  (/)
85, 7wne 2446 . . . . 5  wff  x  =/=  (/)
96, 8wa 358 . . . 4  wff  ( x 
C_  A  /\  x  =/=  (/) )
10 vz . . . . . . . . 9  set  z
1110cv 1622 . . . . . . . 8  class  z
12 vy . . . . . . . . 9  set  y
1312cv 1622 . . . . . . . 8  class  y
1411, 13, 2wbr 4023 . . . . . . 7  wff  z R y
1514wn 3 . . . . . 6  wff  -.  z R y
1615, 10, 5wral 2543 . . . . 5  wff  A. z  e.  x  -.  z R y
1716, 12, 5wrex 2544 . . . 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 1527 . 2  wff  A. x
( ( x  C_  A  /\  x  =/=  (/) )  ->  E. y  e.  x  A. z  e.  x  -.  z R y )
203, 19wb 176 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  4355  dffr2  4358  frss  4360  freq1  4363  nffr  4367  frinxp  4755  frsn  4760  f1oweALT  5851  frxp  6225  frfi  7102  fpwwe2lem12  8263  fpwwe2lem13  8264  dffr5  24110  dfon2lem9  24147  fnwe2  27150  bnj1154  29029
  Copyright terms: Public domain W3C validator