Metamath Proof Explorer

Theorem soinxp

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

		Ref	Expression
	Assertion	soinxp	$⊢ R Or A \leftrightarrow (R \cap (A \times A)) Or A$

Proof

Step	Hyp	Ref	Expression
1		poinxp	$⊢ R Po A \leftrightarrow (R \cap (A \times A)) Po A$
2		brinxp	$⊢ (x \in A \land y \in A) \to (x R y \leftrightarrow x (R \cap (A \times A)) y)$
3		biidd	$⊢ (x \in A \land y \in A) \to (x = y \leftrightarrow x = y)$
4		brinxp	$⊢ (y \in A \land x \in A) \to (y R x \leftrightarrow y (R \cap (A \times A)) x)$
5	4	ancoms	$⊢ (x \in A \land y \in A) \to (y R x \leftrightarrow y (R \cap (A \times A)) x)$
6	2 3 5	3orbi123d	$⊢ (x \in A \land y \in A) \to ((x R y \lor x = y \lor y R x) \leftrightarrow (x (R \cap (A \times A)) y \lor x = y \lor y (R \cap (A \times A)) x))$
7	6	ralbidva	$⊢ x \in A \to (\forall y \in A (x R y \lor x = y \lor y R x) \leftrightarrow \forall y \in A (x (R \cap (A \times A)) y \lor x = y \lor y (R \cap (A \times A)) x))$
8	7	ralbiia	$⊢ \forall x \in A \forall y \in A (x R y \lor x = y \lor y R x) \leftrightarrow \forall x \in A \forall y \in A (x (R \cap (A \times A)) y \lor x = y \lor y (R \cap (A \times A)) x)$
9	1 8	anbi12i	$⊢ (R Po A \land \forall x \in A \forall y \in A (x R y \lor x = y \lor y R x)) \leftrightarrow ((R \cap (A \times A)) Po A \land \forall x \in A \forall y \in A (x (R \cap (A \times A)) y \lor x = y \lor y (R \cap (A \times A)) x))$
10		df-so	$⊢ R Or A \leftrightarrow (R Po A \land \forall x \in A \forall y \in A (x R y \lor x = y \lor y R x))$
11		df-so	$⊢ (R \cap (A \times A)) Or A \leftrightarrow ((R \cap (A \times A)) Po A \land \forall x \in A \forall y \in A (x (R \cap (A \times A)) y \lor x = y \lor y (R \cap (A \times A)) x))$
12	9 10 11	3bitr4i	$⊢ R Or A \leftrightarrow (R \cap (A \times A)) Or A$