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 We A \leftrightarrow (R \cap (A \times A)) We A$

Proof

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

Metamath Proof Explorer

Theorem weinxp

Proof