Theorem dffr4

Description: Alternate definition of well-founded relation. (Contributed by Scott Fenton, 2-Feb-2011)

	Ref	Expression
Assertion	dffr4	$$⊢R\mathrm{Fr}A\leftrightarrow \forall x\left(\left(x\subseteq A\wedge x\ne \varnothing \right)\to \exists y\in xPred\left(R,x,y\right)=\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		dffr3	$$⊢R\mathrm{Fr}A\leftrightarrow \forall x\left(\left(x\subseteq A\wedge x\ne \varnothing \right)\to \exists y\in xx\cap R^{-1}\left[\left\{y\right\}\right]=\varnothing \right)$$
2		df-pred	$$⊢Pred\left(R,x,y\right)=x\cap R^{-1}\left[\left\{y\right\}\right]$$
3	2	eqeq1i	$$⊢Pred\left(R,x,y\right)=\varnothing \leftrightarrow x\cap R^{-1}\left[\left\{y\right\}\right]=\varnothing$$
4	3	rexbii	$$⊢\exists y\in xPred\left(R,x,y\right)=\varnothing \leftrightarrow \exists y\in xx\cap R^{-1}\left[\left\{y\right\}\right]=\varnothing$$
5	4	imbi2i	$$⊢\left(\left(x\subseteq A\wedge x\ne \varnothing \right)\to \exists y\in xPred\left(R,x,y\right)=\varnothing \right)\leftrightarrow \left(\left(x\subseteq A\wedge x\ne \varnothing \right)\to \exists y\in xx\cap R^{-1}\left[\left\{y\right\}\right]=\varnothing \right)$$
6	5	albii	$$⊢\forall x\left(\left(x\subseteq A\wedge x\ne \varnothing \right)\to \exists y\in xPred\left(R,x,y\right)=\varnothing \right)\leftrightarrow \forall x\left(\left(x\subseteq A\wedge x\ne \varnothing \right)\to \exists y\in xx\cap R^{-1}\left[\left\{y\right\}\right]=\varnothing \right)$$
7	1 6	bitr4i	$$⊢R\mathrm{Fr}A\leftrightarrow \forall x\left(\left(x\subseteq A\wedge x\ne \varnothing \right)\to \exists y\in xPred\left(R,x,y\right)=\varnothing \right)$$