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 𝑆 → Disj ( 𝑅 ⋉ 𝑆 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | disjorimxrn | ⊢ ( ( Disj 𝑅 ∨ Disj 𝑆 ) → Disj ( 𝑅 ⋉ 𝑆 ) ) | |
2 | 1 | olcs | ⊢ ( Disj 𝑆 → Disj ( 𝑅 ⋉ 𝑆 ) ) |