Theorem 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 \/ Disj S ) -> Disj ( R |X. S ) )

Proof

Step	Hyp	Ref	Expression
1		dfdisjALTV2	|- ( Disj R <-> ( ,~ `' R C_ _I /\ Rel R ) )
2	1	simplbi	|- ( Disj R -> ,~ `' R C_ _I )
3		dfdisjALTV2	|- ( Disj S <-> ( ,~ `' S C_ _I /\ Rel S ) )
4	3	simplbi	|- ( Disj S -> ,~ `' S C_ _I )
5	2 4	orim12i	|- ( ( Disj R \/ Disj S ) -> ( ,~ `' R C_ _I \/ ,~ `' S C_ _I ) )
6		inss	|- ( ( ,~ `' R C_ _I \/ ,~ `' S C_ _I ) -> ( ,~ `' R i^i ,~ `' S ) C_ _I )
7	5 6	syl	|- ( ( Disj R \/ Disj S ) -> ( ,~ `' R i^i ,~ `' S ) C_ _I )
8		disjxrn	|- ( Disj ( R |X. S ) <-> ( ,~ `' R i^i ,~ `' S ) C_ _I )
9	7 8	sylibr	|- ( ( Disj R \/ Disj S ) -> Disj ( R |X. S ) )