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

Metamath Proof Explorer

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 ( 𝑆 ↾ 𝐴 ) ) ) )