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\mathrm{Fr}A\leftrightarrow \forall x\left(\left(x\subseteq A\wedge x\ne \varnothing \right)\to \exists y\in x\forall z\in x\neg zRy\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	$$classR$$
1		cA	$$classA$$
2	1 0	wfr	$$wffR\mathrm{Fr}A$$
3		vx	$$setvarx$$
4	3	cv	$$setvarx$$
5	4 1	wss	$$wffx\subseteq A$$
6		c0	$$class\varnothing$$
7	4 6	wne	$$wffx\ne \varnothing$$
8	5 7	wa	$$wff\left(x\subseteq A\wedge x\ne \varnothing \right)$$
9		vy	$$setvary$$
10		vz	$$setvarz$$
11	10	cv	$$setvarz$$
12	9	cv	$$setvary$$
13	11 12 0	wbr	$$wffzRy$$
14	13	wn	$$wff\neg zRy$$
15	14 10 4	wral	$$wff\forall z\in x\neg zRy$$
16	15 9 4	wrex	$$wff\exists y\in x\forall z\in x\neg zRy$$
17	8 16	wi	$$wff\left(\left(x\subseteq A\wedge x\ne \varnothing \right)\to \exists y\in x\forall z\in x\neg zRy\right)$$
18	17 3	wal	$$wff\forall x\left(\left(x\subseteq A\wedge x\ne \varnothing \right)\to \exists y\in x\forall z\in x\neg zRy\right)$$
19	2 18	wb	$$wff\left(R\mathrm{Fr}A\leftrightarrow \forall x\left(\left(x\subseteq A\wedge x\ne \varnothing \right)\to \exists y\in x\forall z\in x\neg zRy\right)\right)$$