Metamath Proof Explorer


Theorem disjxrn

Description: Two ways of saying that a range Cartesian product is disjoint. (Contributed by Peter Mazsa, 17-Jun-2020) (Revised by Peter Mazsa, 21-Sep-2021)

Ref Expression
Assertion disjxrn ( Disj ( 𝑅𝑆 ) ↔ ( ≀ 𝑅 ∩ ≀ 𝑆 ) ⊆ I )

Proof

Step Hyp Ref Expression
1 xrnrel Rel ( 𝑅𝑆 )
2 dfdisjALTV2 ( Disj ( 𝑅𝑆 ) ↔ ( ≀ ( 𝑅𝑆 ) ⊆ I ∧ Rel ( 𝑅𝑆 ) ) )
3 1 2 mpbiran2 ( Disj ( 𝑅𝑆 ) ↔ ≀ ( 𝑅𝑆 ) ⊆ I )
4 1cosscnvxrn ( 𝑅𝑆 ) = ( ≀ 𝑅 ∩ ≀ 𝑆 )
5 4 sseq1i ( ≀ ( 𝑅𝑆 ) ⊆ I ↔ ( ≀ 𝑅 ∩ ≀ 𝑆 ) ⊆ I )
6 3 5 bitri ( Disj ( 𝑅𝑆 ) ↔ ( ≀ 𝑅 ∩ ≀ 𝑆 ) ⊆ I )