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 𝑅 ∨ Disj 𝑆 ) → Disj ( 𝑅 ⋉ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		dfdisjALTV2	⊢ ( Disj 𝑅 ↔ ( ≀ ◡ 𝑅 ⊆ I ∧ Rel 𝑅 ) )
2	1	simplbi	⊢ ( Disj 𝑅 → ≀ ◡ 𝑅 ⊆ I )
3		dfdisjALTV2	⊢ ( Disj 𝑆 ↔ ( ≀ ◡ 𝑆 ⊆ I ∧ Rel 𝑆 ) )
4	3	simplbi	⊢ ( Disj 𝑆 → ≀ ◡ 𝑆 ⊆ I )
5	2 4	orim12i	⊢ ( ( Disj 𝑅 ∨ Disj 𝑆 ) → ( ≀ ◡ 𝑅 ⊆ I ∨ ≀ ◡ 𝑆 ⊆ I ) )
6		inss	⊢ ( ( ≀ ◡ 𝑅 ⊆ I ∨ ≀ ◡ 𝑆 ⊆ I ) → ( ≀ ◡ 𝑅 ∩ ≀ ◡ 𝑆 ) ⊆ I )
7	5 6	syl	⊢ ( ( Disj 𝑅 ∨ Disj 𝑆 ) → ( ≀ ◡ 𝑅 ∩ ≀ ◡ 𝑆 ) ⊆ I )
8		disjxrn	⊢ ( Disj ( 𝑅 ⋉ 𝑆 ) ↔ ( ≀ ◡ 𝑅 ∩ ≀ ◡ 𝑆 ) ⊆ I )
9	7 8	sylibr	⊢ ( ( Disj 𝑅 ∨ Disj 𝑆 ) → Disj ( 𝑅 ⋉ 𝑆 ) )