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