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

Definition df-fr 4815
Description: Define the well-founded relation predicate. Definition 6.24(1) of [TakeutiZaring] p. 30. For alternate definitions, see dffr2 4821 and dffr3 5223. (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 4812 . 2  wff  R  Fr  A
4 vx . . . . . . 7  setvar  x
54cv 1454 . . . . . 6  class  x
65, 1wss 3416 . . . . 5  wff  x  C_  A
7 c0 3743 . . . . . 6  class  (/)
85, 7wne 2633 . . . . 5  wff  x  =/=  (/)
96, 8wa 375 . . . 4  wff  ( x 
C_  A  /\  x  =/=  (/) )
10 vz . . . . . . . . 9  setvar  z
1110cv 1454 . . . . . . . 8  class  z
12 vy . . . . . . . . 9  setvar  y
1312cv 1454 . . . . . . . 8  class  y
1411, 13, 2wbr 4418 . . . . . . 7  wff  z R y
1514wn 3 . . . . . 6  wff  -.  z R y
1615, 10, 5wral 2749 . . . . 5  wff  A. z  e.  x  -.  z R y
1716, 12, 5wrex 2750 . . . 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 1453 . 2  wff  A. x
( ( x  C_  A  /\  x  =/=  (/) )  ->  E. y  e.  x  A. z  e.  x  -.  z R y )
203, 19wb 189 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 setvar class
This definition is referenced by:  fri  4818  dffr2  4821  frss  4823  freq1  4826  nffr  4830  frinxp  4922  frsn  4927  f1oweALT  6809  frxp  6938  frfi  7847  fpwwe2lem12  9097  fpwwe2lem13  9098  bnj1154  29858  dffr5  30443  dfon2lem9  30487  fin2so  31978  fnwe2  35957
  Copyright terms: Public domain W3C validator