Theorem xrnres4

Description: Two ways to express restriction of range Cartesian product. (Contributed by Peter Mazsa, 29-Dec-2020)

	Ref	Expression
Assertion	xrnres4	⊢ ( ( 𝑅 ⋉ 𝑆 ) ↾ 𝐴 ) = ( ( 𝑅 ⋉ 𝑆 ) ∩ ( 𝐴 × ( ran ( 𝑅 ↾ 𝐴 ) × ran ( 𝑆 ↾ 𝐴 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		xrnres3	⊢ ( ( 𝑅 ⋉ 𝑆 ) ↾ 𝐴 ) = ( ( 𝑅 ↾ 𝐴 ) ⋉ ( 𝑆 ↾ 𝐴 ) )
2		dfres4	⊢ ( 𝑅 ↾ 𝐴 ) = ( 𝑅 ∩ ( 𝐴 × ran ( 𝑅 ↾ 𝐴 ) ) )
3		dfres4	⊢ ( 𝑆 ↾ 𝐴 ) = ( 𝑆 ∩ ( 𝐴 × ran ( 𝑆 ↾ 𝐴 ) ) )
4	2 3	xrneq12i	⊢ ( ( 𝑅 ↾ 𝐴 ) ⋉ ( 𝑆 ↾ 𝐴 ) ) = ( ( 𝑅 ∩ ( 𝐴 × ran ( 𝑅 ↾ 𝐴 ) ) ) ⋉ ( 𝑆 ∩ ( 𝐴 × ran ( 𝑆 ↾ 𝐴 ) ) ) )
5		inxpxrn	⊢ ( ( 𝑅 ∩ ( 𝐴 × ran ( 𝑅 ↾ 𝐴 ) ) ) ⋉ ( 𝑆 ∩ ( 𝐴 × ran ( 𝑆 ↾ 𝐴 ) ) ) ) = ( ( 𝑅 ⋉ 𝑆 ) ∩ ( 𝐴 × ( ran ( 𝑅 ↾ 𝐴 ) × ran ( 𝑆 ↾ 𝐴 ) ) ) )
6	1 4 5	3eqtri	⊢ ( ( 𝑅 ⋉ 𝑆 ) ↾ 𝐴 ) = ( ( 𝑅 ⋉ 𝑆 ) ∩ ( 𝐴 × ( ran ( 𝑅 ↾ 𝐴 ) × ran ( 𝑆 ↾ 𝐴 ) ) ) )