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

Metamath Proof Explorer

Theorem disjxrnres5

Description: Disjoint range Cartesian product. (Contributed by Peter Mazsa, 25-Aug-2023)

Ref Expression
Assertion disjxrnres5 ( Disj ( 𝑅 ⋉ ( 𝑆 ↾ 𝐴 ) ) ↔ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] ( 𝑅 ⋉ 𝑆 ) ∩ [ 𝑣 ] ( 𝑅 ⋉ 𝑆 ) ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 xrnres2 ⊢ ( ( 𝑅 ⋉ 𝑆 ) ↾ 𝐴 ) = ( 𝑅 ⋉ ( 𝑆 ↾ 𝐴 ) )
2 1 disjeqi ⊢ ( Disj ( ( 𝑅 ⋉ 𝑆 ) ↾ 𝐴 ) ↔ Disj ( 𝑅 ⋉ ( 𝑆 ↾ 𝐴 ) ) )
3 xrnrel ⊢ Rel ( 𝑅 ⋉ 𝑆 )
4 disjres ⊢ ( Rel ( 𝑅 ⋉ 𝑆 ) → ( Disj ( ( 𝑅 ⋉ 𝑆 ) ↾ 𝐴 ) ↔ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] ( 𝑅 ⋉ 𝑆 ) ∩ [ 𝑣 ] ( 𝑅 ⋉ 𝑆 ) ) = ∅ ) ) )
5 3 4 ax-mp ⊢ ( Disj ( ( 𝑅 ⋉ 𝑆 ) ↾ 𝐴 ) ↔ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] ( 𝑅 ⋉ 𝑆 ) ∩ [ 𝑣 ] ( 𝑅 ⋉ 𝑆 ) ) = ∅ ) )
6 2 5 bitr3i ⊢ ( Disj ( 𝑅 ⋉ ( 𝑆 ↾ 𝐴 ) ) ↔ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] ( 𝑅 ⋉ 𝑆 ) ∩ [ 𝑣 ] ( 𝑅 ⋉ 𝑆 ) ) = ∅ ) )