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

Definition df-fr 4748
Description: Define the well-founded relation predicate. Definition 6.24(1) of [TakeutiZaring] p. 30. For alternate definitions, see dffr2 4754 and dffr3 5156. (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 4745 . 2  wff  R  Fr  A
4 vx . . . . . . 7  setvar  x
54cv 1436 . . . . . 6  class  x
65, 1wss 3372 . . . . 5  wff  x  C_  A
7 c0 3697 . . . . . 6  class  (/)
85, 7wne 2593 . . . . 5  wff  x  =/=  (/)
96, 8wa 370 . . . 4  wff  ( x 
C_  A  /\  x  =/=  (/) )
10 vz . . . . . . . . 9  setvar  z
1110cv 1436 . . . . . . . 8  class  z
12 vy . . . . . . . . 9  setvar  y
1312cv 1436 . . . . . . . 8  class  y
1411, 13, 2wbr 4359 . . . . . . 7  wff  z R y
1514wn 3 . . . . . 6  wff  -.  z R y
1615, 10, 5wral 2708 . . . . 5  wff  A. z  e.  x  -.  z R y
1716, 12, 5wrex 2709 . . . 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 1435 . 2  wff  A. x
( ( x  C_  A  /\  x  =/=  (/) )  ->  E. y  e.  x  A. z  e.  x  -.  z R y )
203, 19wb 187 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  4751  dffr2  4754  frss  4756  freq1  4759  nffr  4763  frinxp  4855  frsn  4860  f1oweALT  6728  frxp  6854  frfi  7762  fpwwe2lem12  9010  fpwwe2lem13  9011  bnj1154  29753  dffr5  30337  dfon2lem9  30381  fin2so  31833  fnwe2  35818
  Copyright terms: Public domain W3C validator