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

Metamath Proof Explorer

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 ) )