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 ⊢ R ⋉ S ↾ A = R ⋉ S ∩ A × ran ⁡ R ↾ A × ran ⁡ S ↾ A

Proof

Step Hyp Ref Expression
1 xrnres3 ⊢ R ⋉ S ↾ A = R ↾ A ⋉ S ↾ A
2 dfres4 ⊢ R ↾ A = R ∩ A × ran ⁡ R ↾ A
3 dfres4 ⊢ S ↾ A = S ∩ A × ran ⁡ S ↾ A
4 2 3 xrneq12i ⊢ R ↾ A ⋉ S ↾ A = R ∩ A × ran ⁡ R ↾ A ⋉ S ∩ A × ran ⁡ S ↾ A
5 inxpxrn ⊢ R ∩ A × ran ⁡ R ↾ A ⋉ S ∩ A × ran ⁡ S ↾ A = R ⋉ S ∩ A × ran ⁡ R ↾ A × ran ⁡ S ↾ A
6 1 4 5 3eqtri ⊢ R ⋉ S ↾ A = R ⋉ S ∩ A × ran ⁡ R ↾ A × ran ⁡ S ↾ A