Theorem weinxp

Description: Intersection of well-ordering with Cartesian product of its field. (Contributed by NM, 9-Mar-1997) (Revised by Mario Carneiro, 10-Jul-2014)

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

Proof

Step	Hyp	Ref	Expression
1		frinxp	$$⊢R\mathrm{Fr}A\leftrightarrow \left(R\cap \left(A\times A\right)\right)\mathrm{Fr}A$$
2		soinxp	$$⊢R\mathrm{Or}A\leftrightarrow \left(R\cap \left(A\times A\right)\right)\mathrm{Or}A$$
3	1 2	anbi12i	$$⊢\left(R\mathrm{Fr}A\wedge R\mathrm{Or}A\right)\leftrightarrow \left(\left(R\cap \left(A\times A\right)\right)\mathrm{Fr}A\wedge \left(R\cap \left(A\times A\right)\right)\mathrm{Or}A\right)$$
4		df-we	$$⊢R\mathrm{We}A\leftrightarrow \left(R\mathrm{Fr}A\wedge R\mathrm{Or}A\right)$$
5		df-we	$$⊢\left(R\cap \left(A\times A\right)\right)\mathrm{We}A\leftrightarrow \left(\left(R\cap \left(A\times A\right)\right)\mathrm{Fr}A\wedge \left(R\cap \left(A\times A\right)\right)\mathrm{Or}A\right)$$
6	3 4 5	3bitr4i	$$⊢R\mathrm{We}A\leftrightarrow \left(R\cap \left(A\times A\right)\right)\mathrm{We}A$$