This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-fr

Description: Define the well-founded relation predicate. Definition 6.24(1) of TakeutiZaring p. 30. For alternate definitions, see dffr2 and dffr3 . A class is called well-founded when the membership relation _E (see df-eprel ) is well-founded on it, that is, A is well-founded if _E Fr A (some sources request that the membership relation be well-founded on its transitive closure). (Contributed by NM, 3-Apr-1994)

Ref Expression
Assertion df-fr 
|- ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. z e. x -. z R y ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR 
 |-  R
1 cA 
 |-  A
2 1 0 wfr 
 |-  R Fr A
3 vx 
 |-  x
4 3 cv 
 |-  x
5 4 1 wss 
 |-  x C_ A
6 c0 
 |-  (/)
7 4 6 wne 
 |-  x =/= (/)
8 5 7 wa 
 |-  ( x C_ A /\ x =/= (/) )
9 vy 
 |-  y
10 vz 
 |-  z
11 10 cv 
 |-  z
12 9 cv 
 |-  y
13 11 12 0 wbr 
 |-  z R y
14 13 wn 
 |-  -. z R y
15 14 10 4 wral 
 |-  A. z e. x -. z R y
16 15 9 4 wrex 
 |-  E. y e. x A. z e. x -. z R y
17 8 16 wi 
 |-  ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. z e. x -. z R y )
18 17 3 wal 
 |-  A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. z e. x -. z R y )
19 2 18 wb 
 |-  ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. z e. x -. z R y ) )