Theorem frinxp

Description: Intersection of well-founded relation with Cartesian product of its field. (Contributed by Mario Carneiro, 10-Jul-2014)

	Ref	Expression
Assertion	frinxp	$$⊢R\mathrm{Fr}A\leftrightarrow \left(R\cap \left(A\times A\right)\right)\mathrm{Fr}A$$

Proof

Step	Hyp	Ref	Expression
1		ssel	$$⊢z\subseteq A\to \left(x\in z\to x\in A\right)$$
2		ssel	$$⊢z\subseteq A\to \left(y\in z\to y\in A\right)$$
3	1 2	anim12d	$$⊢z\subseteq A\to \left(\left(x\in z\wedge y\in z\right)\to \left(x\in A\wedge y\in A\right)\right)$$
4		brinxp	$$⊢\left(y\in A\wedge x\in A\right)\to \left(yRx\leftrightarrow y\left(R\cap \left(A\times A\right)\right)x\right)$$
5	4	ancoms	$$⊢\left(x\in A\wedge y\in A\right)\to \left(yRx\leftrightarrow y\left(R\cap \left(A\times A\right)\right)x\right)$$
6	3 5	syl6	$$⊢z\subseteq A\to \left(\left(x\in z\wedge y\in z\right)\to \left(yRx\leftrightarrow y\left(R\cap \left(A\times A\right)\right)x\right)\right)$$
7	6	impl	$$⊢\left(\left(z\subseteq A\wedge x\in z\right)\wedge y\in z\right)\to \left(yRx\leftrightarrow y\left(R\cap \left(A\times A\right)\right)x\right)$$
8	7	notbid	$$⊢\left(\left(z\subseteq A\wedge x\in z\right)\wedge y\in z\right)\to \left(\neg yRx\leftrightarrow \neg y\left(R\cap \left(A\times A\right)\right)x\right)$$
9	8	ralbidva	$$⊢\left(z\subseteq A\wedge x\in z\right)\to \left(\forall y\in z\neg yRx\leftrightarrow \forall y\in z\neg y\left(R\cap \left(A\times A\right)\right)x\right)$$
10	9	rexbidva	$$⊢z\subseteq A\to \left(\exists x\in z\forall y\in z\neg yRx\leftrightarrow \exists x\in z\forall y\in z\neg y\left(R\cap \left(A\times A\right)\right)x\right)$$
11	10	adantr	$$⊢\left(z\subseteq A\wedge z\ne \varnothing \right)\to \left(\exists x\in z\forall y\in z\neg yRx\leftrightarrow \exists x\in z\forall y\in z\neg y\left(R\cap \left(A\times A\right)\right)x\right)$$
12	11	pm5.74i	$$⊢\left(\left(z\subseteq A\wedge z\ne \varnothing \right)\to \exists x\in z\forall y\in z\neg yRx\right)\leftrightarrow \left(\left(z\subseteq A\wedge z\ne \varnothing \right)\to \exists x\in z\forall y\in z\neg y\left(R\cap \left(A\times A\right)\right)x\right)$$
13	12	albii	$$⊢\forall z\left(\left(z\subseteq A\wedge z\ne \varnothing \right)\to \exists x\in z\forall y\in z\neg yRx\right)\leftrightarrow \forall z\left(\left(z\subseteq A\wedge z\ne \varnothing \right)\to \exists x\in z\forall y\in z\neg y\left(R\cap \left(A\times A\right)\right)x\right)$$
14		df-fr	$$⊢R\mathrm{Fr}A\leftrightarrow \forall z\left(\left(z\subseteq A\wedge z\ne \varnothing \right)\to \exists x\in z\forall y\in z\neg yRx\right)$$
15		df-fr	$$⊢\left(R\cap \left(A\times A\right)\right)\mathrm{Fr}A\leftrightarrow \forall z\left(\left(z\subseteq A\wedge z\ne \varnothing \right)\to \exists x\in z\forall y\in z\neg y\left(R\cap \left(A\times A\right)\right)x\right)$$
16	13 14 15	3bitr4i	$$⊢R\mathrm{Fr}A\leftrightarrow \left(R\cap \left(A\times A\right)\right)\mathrm{Fr}A$$