Metamath Proof Explorer

Theorem poinxp

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

		Ref	Expression
	Assertion	poinxp	$⊢ R Po A \leftrightarrow (R \cap (A \times A)) Po A$

Proof

Step	Hyp	Ref	Expression
1		brinxp	$⊢ (x \in A \land x \in A) \to (x R x \leftrightarrow x (R \cap (A \times A)) x)$
2	1	anidms	$⊢ x \in A \to (x R x \leftrightarrow x (R \cap (A \times A)) x)$
3	2	ad2antrr	$⊢ ((x \in A \land y \in A) \land z \in A) \to (x R x \leftrightarrow x (R \cap (A \times A)) x)$
4	3	notbid	$⊢ ((x \in A \land y \in A) \land z \in A) \to (\neg x R x \leftrightarrow \neg x (R \cap (A \times A)) x)$
5		brinxp	$⊢ (x \in A \land y \in A) \to (x R y \leftrightarrow x (R \cap (A \times A)) y)$
6	5	adantr	$⊢ ((x \in A \land y \in A) \land z \in A) \to (x R y \leftrightarrow x (R \cap (A \times A)) y)$
7		brinxp	$⊢ (y \in A \land z \in A) \to (y R z \leftrightarrow y (R \cap (A \times A)) z)$
8	7	adantll	$⊢ ((x \in A \land y \in A) \land z \in A) \to (y R z \leftrightarrow y (R \cap (A \times A)) z)$
9	6 8	anbi12d	$⊢ ((x \in A \land y \in A) \land z \in A) \to ((x R y \land y R z) \leftrightarrow (x (R \cap (A \times A)) y \land y (R \cap (A \times A)) z))$
10		brinxp	$⊢ (x \in A \land z \in A) \to (x R z \leftrightarrow x (R \cap (A \times A)) z)$
11	10	adantlr	$⊢ ((x \in A \land y \in A) \land z \in A) \to (x R z \leftrightarrow x (R \cap (A \times A)) z)$
12	9 11	imbi12d	$⊢ ((x \in A \land y \in A) \land z \in A) \to (((x R y \land y R z) \to x R z) \leftrightarrow ((x (R \cap (A \times A)) y \land y (R \cap (A \times A)) z) \to x (R \cap (A \times A)) z))$
13	4 12	anbi12d	$⊢ ((x \in A \land y \in A) \land z \in A) \to ((\neg x R x \land ((x R y \land y R z) \to x R z)) \leftrightarrow (\neg x (R \cap (A \times A)) x \land ((x (R \cap (A \times A)) y \land y (R \cap (A \times A)) z) \to x (R \cap (A \times A)) z)))$
14	13	ralbidva	$⊢ (x \in A \land y \in A) \to (\forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z)) \leftrightarrow \forall z \in A (\neg x (R \cap (A \times A)) x \land ((x (R \cap (A \times A)) y \land y (R \cap (A \times A)) z) \to x (R \cap (A \times A)) z)))$
15	14	ralbidva	$⊢ x \in A \to (\forall y \in A \forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z)) \leftrightarrow \forall y \in A \forall z \in A (\neg x (R \cap (A \times A)) x \land ((x (R \cap (A \times A)) y \land y (R \cap (A \times A)) z) \to x (R \cap (A \times A)) z)))$
16	15	ralbiia	$⊢ \forall x \in A \forall y \in A \forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z)) \leftrightarrow \forall x \in A \forall y \in A \forall z \in A (\neg x (R \cap (A \times A)) x \land ((x (R \cap (A \times A)) y \land y (R \cap (A \times A)) z) \to x (R \cap (A \times A)) z))$
17		df-po	$⊢ R Po A \leftrightarrow \forall x \in A \forall y \in A \forall z \in A (\neg x R x \land ((x R y \land y R z) \to x R z))$
18		df-po	$⊢ (R \cap (A \times A)) Po A \leftrightarrow \forall x \in A \forall y \in A \forall z \in A (\neg x (R \cap (A \times A)) x \land ((x (R \cap (A \times A)) y \land y (R \cap (A \times A)) z) \to x (R \cap (A \times A)) z))$
19	16 17 18	3bitr4i	$⊢ R Po A \leftrightarrow (R \cap (A \times A)) Po A$