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

Definition df-fr 4501
Description: Define the well-founded relation predicate. Definition 6.24(1) of [TakeutiZaring] p. 30. For alternate definitions, see dffr2 4507 and dffr3 5195. (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 4498 . 2  wff  R  Fr  A
4 vx . . . . . . 7  set  x
54cv 1648 . . . . . 6  class  x
65, 1wss 3280 . . . . 5  wff  x  C_  A
7 c0 3588 . . . . . 6  class  (/)
85, 7wne 2567 . . . . 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 4172 . . . . . . 7  wff  z R y
1514wn 3 . . . . . 6  wff  -.  z R y
1615, 10, 5wral 2666 . . . . 5  wff  A. z  e.  x  -.  z R y
1716, 12, 5wrex 2667 . . . 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  4504  dffr2  4507  frss  4509  freq1  4512  nffr  4516  frinxp  4902  frsn  4907  f1oweALT  6033  frxp  6415  frfi  7311  fpwwe2lem12  8472  fpwwe2lem13  8473  dffr5  25324  dfon2lem9  25361  fnwe2  27018  bnj1154  29074
  Copyright terms: Public domain W3C validator