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 ) )