xpidtr

Description: A Cartesian square is a transitive relation. (Contributed by FL, 31-Jul-2009)

		Ref	Expression
	Assertion	xpidtr	$⊢ (A \times A) \circ (A \times A) \subseteq A \times A$

Step	Hyp	Ref	Expression
1		brxp	$⊢ x (A \times A) y \leftrightarrow (x \in A \land y \in A)$
2		brxp	$⊢ y (A \times A) z \leftrightarrow (y \in A \land z \in A)$
3		brxp	$⊢ x (A \times A) z \leftrightarrow (x \in A \land z \in A)$
4	3	simplbi2com	$⊢ z \in A \to (x \in A \to x (A \times A) z)$
5	2 4	simplbiim	$⊢ y (A \times A) z \to (x \in A \to x (A \times A) z)$
6	5	com12	$⊢ x \in A \to (y (A \times A) z \to x (A \times A) z)$
7	6	adantr	$⊢ (x \in A \land y \in A) \to (y (A \times A) z \to x (A \times A) z)$
8	1 7	sylbi	$⊢ x (A \times A) y \to (y (A \times A) z \to x (A \times A) z)$
9	8	imp	$⊢ (x (A \times A) y \land y (A \times A) z) \to x (A \times A) z$
10	9	ax-gen	$⊢ \forall z ((x (A \times A) y \land y (A \times A) z) \to x (A \times A) z)$
11	10	gen2	$⊢ \forall x \forall y \forall z ((x (A \times A) y \land y (A \times A) z) \to x (A \times A) z)$
12		cotr	$⊢ (A \times A) \circ (A \times A) \subseteq A \times A \leftrightarrow \forall x \forall y \forall z ((x (A \times A) y \land y (A \times A) z) \to x (A \times A) z)$
13	11 12	mpbir	$⊢ (A \times A) \circ (A \times A) \subseteq A \times A$

Metamath Proof Explorer