disjorimxrn

Description: Disjointness condition for range Cartesian product. (Contributed by Peter Mazsa, 12-Jul-2020) (Revised by Peter Mazsa, 22-Sep-2021)

		Ref	Expression
	Assertion	disjorimxrn	$⊢ (Disj R \lor Disj S) \to Disj R ⋉ S$

Step	Hyp	Ref	Expression
1		dfdisjALTV2	$⊢ Disj R \leftrightarrow (≀ R^{-1} \subseteq I \land Rel R)$
2	1	simplbi	$⊢ Disj R \to ≀ R^{-1} \subseteq I$
3		dfdisjALTV2	$⊢ Disj S \leftrightarrow (≀ S^{-1} \subseteq I \land Rel S)$
4	3	simplbi	$⊢ Disj S \to ≀ S^{-1} \subseteq I$
5	2 4	orim12i	$⊢ (Disj R \lor Disj S) \to (≀ R^{-1} \subseteq I \lor ≀ S^{-1} \subseteq I)$
6		inss	$⊢ (≀ R^{-1} \subseteq I \lor ≀ S^{-1} \subseteq I) \to ≀ R^{-1} \cap ≀ S^{-1} \subseteq I$
7	5 6	syl	$⊢ (Disj R \lor Disj S) \to ≀ R^{-1} \cap ≀ S^{-1} \subseteq I$
8		disjxrn	$⊢ Disj R ⋉ S \leftrightarrow ≀ R^{-1} \cap ≀ S^{-1} \subseteq I$
9	7 8	sylibr	$⊢ (Disj R \lor Disj S) \to Disj R ⋉ S$

Metamath Proof Explorer