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

Definition df-fr 4838
Description: Define the well-founded relation predicate. Definition 6.24(1) of [TakeutiZaring] p. 30. For alternate definitions, see dffr2 4844 and dffr3 5367. (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 4835 . 2  wff  R  Fr  A
4 vx . . . . . . 7  setvar  x
54cv 1378 . . . . . 6  class  x
65, 1wss 3476 . . . . 5  wff  x  C_  A
7 c0 3785 . . . . . 6  class  (/)
85, 7wne 2662 . . . . 5  wff  x  =/=  (/)
96, 8wa 369 . . . 4  wff  ( x 
C_  A  /\  x  =/=  (/) )
10 vz . . . . . . . . 9  setvar  z
1110cv 1378 . . . . . . . 8  class  z
12 vy . . . . . . . . 9  setvar  y
1312cv 1378 . . . . . . . 8  class  y
1411, 13, 2wbr 4447 . . . . . . 7  wff  z R y
1514wn 3 . . . . . 6  wff  -.  z R y
1615, 10, 5wral 2814 . . . . 5  wff  A. z  e.  x  -.  z R y
1716, 12, 5wrex 2815 . . . 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 1377 . 2  wff  A. x
( ( x  C_  A  /\  x  =/=  (/) )  ->  E. y  e.  x  A. z  e.  x  -.  z R y )
203, 19wb 184 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  4841  dffr2  4844  frss  4846  freq1  4849  nffr  4853  frinxp  5064  frsn  5069  f1oweALT  6765  frxp  6890  frfi  7761  fpwwe2lem12  9015  fpwwe2lem13  9016  dffr5  28759  dfon2lem9  28800  fin2so  29617  fnwe2  30603  bnj1154  33134
  Copyright terms: Public domain W3C validator