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

Definition df-fr 4354
Description: Define the well-founded relation predicate. Definition 6.24(1) of [TakeutiZaring] p. 30. For alternate definitions, see dffr2 4360 and dffr3 5047. (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 4351 . 2  wff  R  Fr  A
4 vx . . . . . . 7  set  x
54cv 1624 . . . . . 6  class  x
65, 1wss 3154 . . . . 5  wff  x  C_  A
7 c0 3457 . . . . . 6  class  (/)
85, 7wne 2448 . . . . 5  wff  x  =/=  (/)
96, 8wa 358 . . . 4  wff  ( x 
C_  A  /\  x  =/=  (/) )
10 vz . . . . . . . . 9  set  z
1110cv 1624 . . . . . . . 8  class  z
12 vy . . . . . . . . 9  set  y
1312cv 1624 . . . . . . . 8  class  y
1411, 13, 2wbr 4025 . . . . . . 7  wff  z R y
1514wn 3 . . . . . 6  wff  -.  z R y
1615, 10, 5wral 2545 . . . . 5  wff  A. z  e.  x  -.  z R y
1716, 12, 5wrex 2546 . . . 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 1529 . 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  4357  dffr2  4360  frss  4362  freq1  4365  nffr  4369  frinxp  4757  frsn  4762  f1oweALT  5853  frxp  6227  frfi  7104  fpwwe2lem12  8265  fpwwe2lem13  8266  dffr5  24112  dfon2lem9  24149  fnwe2  27161  bnj1154  29102
  Copyright terms: Public domain W3C validator