# Metamath Proof Explorer

## Theorem xrnresex

Description: Sufficient condition for a restricted range Cartesian product to be a set. (Contributed by Peter Mazsa, 16-Dec-2020) (Revised by Peter Mazsa, 7-Sep-2021)

Ref Expression
Assertion xrnresex ${⊢}\left({A}\in {V}\wedge {R}\in {W}\wedge {{S}↾}_{{A}}\in {X}\right)\to {R}⋉\left({{S}↾}_{{A}}\right)\in \mathrm{V}$

### Proof

Step Hyp Ref Expression
1 xrnres3 ${⊢}{{R}⋉{S}↾}_{{A}}=\left({{R}↾}_{{A}}\right)⋉\left({{S}↾}_{{A}}\right)$
2 xrnres2 ${⊢}{{R}⋉{S}↾}_{{A}}={R}⋉\left({{S}↾}_{{A}}\right)$
3 1 2 eqtr3i ${⊢}\left({{R}↾}_{{A}}\right)⋉\left({{S}↾}_{{A}}\right)={R}⋉\left({{S}↾}_{{A}}\right)$
4 dfres4 ${⊢}{{R}↾}_{{A}}={R}\cap \left({A}×\mathrm{ran}\left({{R}↾}_{{A}}\right)\right)$
5 dfres4 ${⊢}{{S}↾}_{{A}}={S}\cap \left({A}×\mathrm{ran}\left({{S}↾}_{{A}}\right)\right)$
6 4 5 xrneq12i ${⊢}\left({{R}↾}_{{A}}\right)⋉\left({{S}↾}_{{A}}\right)=\left({R}\cap \left({A}×\mathrm{ran}\left({{R}↾}_{{A}}\right)\right)\right)⋉\left({S}\cap \left({A}×\mathrm{ran}\left({{S}↾}_{{A}}\right)\right)\right)$
7 simp1 ${⊢}\left({A}\in {V}\wedge {R}\in {W}\wedge {{S}↾}_{{A}}\in {X}\right)\to {A}\in {V}$
8 resexg ${⊢}{R}\in {W}\to {{R}↾}_{{A}}\in \mathrm{V}$
9 rnexg ${⊢}{{R}↾}_{{A}}\in \mathrm{V}\to \mathrm{ran}\left({{R}↾}_{{A}}\right)\in \mathrm{V}$
10 8 9 syl ${⊢}{R}\in {W}\to \mathrm{ran}\left({{R}↾}_{{A}}\right)\in \mathrm{V}$
11 10 3ad2ant2 ${⊢}\left({A}\in {V}\wedge {R}\in {W}\wedge {{S}↾}_{{A}}\in {X}\right)\to \mathrm{ran}\left({{R}↾}_{{A}}\right)\in \mathrm{V}$
12 rnexg ${⊢}{{S}↾}_{{A}}\in {X}\to \mathrm{ran}\left({{S}↾}_{{A}}\right)\in \mathrm{V}$
13 12 3ad2ant3 ${⊢}\left({A}\in {V}\wedge {R}\in {W}\wedge {{S}↾}_{{A}}\in {X}\right)\to \mathrm{ran}\left({{S}↾}_{{A}}\right)\in \mathrm{V}$
14 inxpxrn ${⊢}\left({R}\cap \left({A}×\mathrm{ran}\left({{R}↾}_{{A}}\right)\right)\right)⋉\left({S}\cap \left({A}×\mathrm{ran}\left({{S}↾}_{{A}}\right)\right)\right)={R}⋉{S}\cap \left({A}×\left(\mathrm{ran}\left({{R}↾}_{{A}}\right)×\mathrm{ran}\left({{S}↾}_{{A}}\right)\right)\right)$
15 xrninxpex ${⊢}\left({A}\in {V}\wedge \mathrm{ran}\left({{R}↾}_{{A}}\right)\in \mathrm{V}\wedge \mathrm{ran}\left({{S}↾}_{{A}}\right)\in \mathrm{V}\right)\to {R}⋉{S}\cap \left({A}×\left(\mathrm{ran}\left({{R}↾}_{{A}}\right)×\mathrm{ran}\left({{S}↾}_{{A}}\right)\right)\right)\in \mathrm{V}$
16 14 15 eqeltrid ${⊢}\left({A}\in {V}\wedge \mathrm{ran}\left({{R}↾}_{{A}}\right)\in \mathrm{V}\wedge \mathrm{ran}\left({{S}↾}_{{A}}\right)\in \mathrm{V}\right)\to \left({R}\cap \left({A}×\mathrm{ran}\left({{R}↾}_{{A}}\right)\right)\right)⋉\left({S}\cap \left({A}×\mathrm{ran}\left({{S}↾}_{{A}}\right)\right)\right)\in \mathrm{V}$
17 7 11 13 16 syl3anc ${⊢}\left({A}\in {V}\wedge {R}\in {W}\wedge {{S}↾}_{{A}}\in {X}\right)\to \left({R}\cap \left({A}×\mathrm{ran}\left({{R}↾}_{{A}}\right)\right)\right)⋉\left({S}\cap \left({A}×\mathrm{ran}\left({{S}↾}_{{A}}\right)\right)\right)\in \mathrm{V}$
18 6 17 eqeltrid ${⊢}\left({A}\in {V}\wedge {R}\in {W}\wedge {{S}↾}_{{A}}\in {X}\right)\to \left({{R}↾}_{{A}}\right)⋉\left({{S}↾}_{{A}}\right)\in \mathrm{V}$
19 3 18 eqeltrrid ${⊢}\left({A}\in {V}\wedge {R}\in {W}\wedge {{S}↾}_{{A}}\in {X}\right)\to {R}⋉\left({{S}↾}_{{A}}\right)\in \mathrm{V}$