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

Definition df-fr 4351
Description: Define the well-founded relation predicate. Definition 6.24(1) of [TakeutiZaring] p. 30. For alternate definitions, see dffr2 4357 and dffr3 5044. (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 4348 . 2  wff  R  Fr  A
4 vx . . . . . . 7  set  x
54cv 1622 . . . . . 6  class  x
65, 1wss 3153 . . . . 5  wff  x  C_  A
7 c0 3456 . . . . . 6  class  (/)
85, 7wne 2447 . . . . 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 4024 . . . . . . 7  wff  z R y
1514wn 3 . . . . . 6  wff  -.  z R y
1615, 10, 5wral 2544 . . . . 5  wff  A. z  e.  x  -.  z R y
1716, 12, 5wrex 2545 . . . 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  4354  dffr2  4357  frss  4359  freq1  4362  nffr  4366  frinxp  4754  frsn  4759  f1oweALT  5813  frxp  6187  frfi  7098  fpwwe2lem12  8259  fpwwe2lem13  8260  dffr5  23516  dfon2lem9  23551  fnwe2  26561  bnj1154  28308
  Copyright terms: Public domain W3C validator