This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem disjimxrn

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

		Ref	Expression
	Assertion	disjimxrn	$⊢ Disj S \to Disj R ⋉ S$

Step	Hyp	Ref	Expression
1		disjorimxrn	$⊢ (Disj R \lor Disj S) \to Disj R ⋉ S$
2	1	olcs	$⊢ Disj S \to Disj R ⋉ S$