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

Definition df-fr 4804
Description: Define the well-founded relation predicate. Definition 6.24(1) of [TakeutiZaring] p. 30. For alternate definitions, see dffr2 4810 and dffr3 5212. (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 4801 . 2  wff  R  Fr  A
4 vx . . . . . . 7  setvar  x
54cv 1436 . . . . . 6  class  x
65, 1wss 3433 . . . . 5  wff  x  C_  A
7 c0 3758 . . . . . 6  class  (/)
85, 7wne 2616 . . . . 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 4417 . . . . . . 7  wff  z R y
1514wn 3 . . . . . 6  wff  -.  z R y
1615, 10, 5wral 2773 . . . . 5  wff  A. z  e.  x  -.  z R y
1716, 12, 5wrex 2774 . . . 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  4807  dffr2  4810  frss  4812  freq1  4815  nffr  4819  frinxp  4911  frsn  4916  f1oweALT  6782  frxp  6908  frfi  7813  fpwwe2lem12  9055  fpwwe2lem13  9056  bnj1154  29593  dffr5  30177  dfon2lem9  30221  fin2so  31636  fnwe2  35621
  Copyright terms: Public domain W3C validator