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 ( 𝑅 ⋉ ( 𝑆 ↾ 𝐴 ) ) ↔ ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] ( 𝑅 ⋉ 𝑆 ) ∩ [ 𝑣 ] ( 𝑅 ⋉ 𝑆 ) ) = ∅ ) )