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

Definition df-fr 4431
Description: Define the well-founded relation predicate. Definition 6.24(1) of [TakeutiZaring] p. 30. For alternate definitions, see dffr2 4437 and dffr3 5124. (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 4428 . 2  wff  R  Fr  A
4 vx . . . . . . 7  set  x
54cv 1641 . . . . . 6  class  x
65, 1wss 3228 . . . . 5  wff  x  C_  A
7 c0 3531 . . . . . 6  class  (/)
85, 7wne 2521 . . . . 5  wff  x  =/=  (/)
96, 8wa 358 . . . 4  wff  ( x 
C_  A  /\  x  =/=  (/) )
10 vz . . . . . . . . 9  set  z
1110cv 1641 . . . . . . . 8  class  z
12 vy . . . . . . . . 9  set  y
1312cv 1641 . . . . . . . 8  class  y
1411, 13, 2wbr 4102 . . . . . . 7  wff  z R y
1514wn 3 . . . . . 6  wff  -.  z R y
1615, 10, 5wral 2619 . . . . 5  wff  A. z  e.  x  -.  z R y
1716, 12, 5wrex 2620 . . . 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 1540 . 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  4434  dffr2  4437  frss  4439  freq1  4442  nffr  4446  frinxp  4834  frsn  4839  f1oweALT  5935  frxp  6309  frfi  7189  fpwwe2lem12  8350  fpwwe2lem13  8351  dffr5  24668  dfon2lem9  24705  fnwe2  26473  bnj1154  28774
  Copyright terms: Public domain W3C validator