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

Definition df-fr 4825
Description: Define the well-founded relation predicate. Definition 6.24(1) of [TakeutiZaring] p. 30. For alternate definitions, see dffr2 4831 and dffr3 5356. (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 4822 . 2  wff  R  Fr  A
4 vx . . . . . . 7  setvar  x
54cv 1380 . . . . . 6  class  x
65, 1wss 3459 . . . . 5  wff  x  C_  A
7 c0 3768 . . . . . 6  class  (/)
85, 7wne 2636 . . . . 5  wff  x  =/=  (/)
96, 8wa 369 . . . 4  wff  ( x 
C_  A  /\  x  =/=  (/) )
10 vz . . . . . . . . 9  setvar  z
1110cv 1380 . . . . . . . 8  class  z
12 vy . . . . . . . . 9  setvar  y
1312cv 1380 . . . . . . . 8  class  y
1411, 13, 2wbr 4434 . . . . . . 7  wff  z R y
1514wn 3 . . . . . 6  wff  -.  z R y
1615, 10, 5wral 2791 . . . . 5  wff  A. z  e.  x  -.  z R y
1716, 12, 5wrex 2792 . . . 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 1379 . 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  4828  dffr2  4831  frss  4833  freq1  4836  nffr  4840  frinxp  5052  frsn  5057  f1oweALT  6766  frxp  6892  frfi  7764  fpwwe2lem12  9019  fpwwe2lem13  9020  dffr5  29154  dfon2lem9  29195  fin2so  30012  fnwe2  30971  bnj1154  33783
  Copyright terms: Public domain W3C validator