xptrrel

Description: The cross product is always a transitive relation. (Contributed by RP, 24-Dec-2019)

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

Step	Hyp	Ref	Expression
1		inss1	$⊢ dom (A \times B) \cap ran (A \times B) \subseteq dom (A \times B)$
2		dmxpss	$⊢ dom (A \times B) \subseteq A$
3	1 2	sstri	$⊢ dom (A \times B) \cap ran (A \times B) \subseteq A$
4		inss2	$⊢ dom (A \times B) \cap ran (A \times B) \subseteq ran (A \times B)$
5		rnxpss	$⊢ ran (A \times B) \subseteq B$
6	4 5	sstri	$⊢ dom (A \times B) \cap ran (A \times B) \subseteq B$
7	3 6	ssini	$⊢ dom (A \times B) \cap ran (A \times B) \subseteq A \cap B$
8		eqimss	$⊢ A \cap B = \emptyset \to A \cap B \subseteq \emptyset$
9	7 8	sstrid	$⊢ A \cap B = \emptyset \to dom (A \times B) \cap ran (A \times B) \subseteq \emptyset$
10		ss0	$⊢ dom (A \times B) \cap ran (A \times B) \subseteq \emptyset \to dom (A \times B) \cap ran (A \times B) = \emptyset$
11	9 10	syl	$⊢ A \cap B = \emptyset \to dom (A \times B) \cap ran (A \times B) = \emptyset$
12	11	coemptyd	$⊢ A \cap B = \emptyset \to (A \times B) \circ (A \times B) = \emptyset$
13		0ss	$⊢ \emptyset \subseteq A \times B$
14	12 13	eqsstrdi	$⊢ A \cap B = \emptyset \to (A \times B) \circ (A \times B) \subseteq A \times B$
15		neqne	$⊢ \neg A \cap B = \emptyset \to A \cap B \neq \emptyset$
16	15	xpcoidgend	$⊢ \neg A \cap B = \emptyset \to (A \times B) \circ (A \times B) = A \times B$
17		ssid	$⊢ A \times B \subseteq A \times B$
18	16 17	eqsstrdi	$⊢ \neg A \cap B = \emptyset \to (A \times B) \circ (A \times B) \subseteq A \times B$
19	14 18	pm2.61i	$⊢ (A \times B) \circ (A \times B) \subseteq A \times B$

Metamath Proof Explorer