# 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
`|- ( ( A e. V /\ R e. W /\ ( S |` A ) e. X ) -> ( R |X. ( S |` A ) ) e. _V )`

### Proof

Step Hyp Ref Expression
1 xrnres3
` |-  ( ( R |X. S ) |` A ) = ( ( R |` A ) |X. ( S |` A ) )`
2 xrnres2
` |-  ( ( R |X. S ) |` A ) = ( R |X. ( S |` A ) )`
3 1 2 eqtr3i
` |-  ( ( R |` A ) |X. ( S |` A ) ) = ( R |X. ( S |` A ) )`
4 dfres4
` |-  ( R |` A ) = ( R i^i ( A X. ran ( R |` A ) ) )`
5 dfres4
` |-  ( S |` A ) = ( S i^i ( A X. ran ( S |` A ) ) )`
6 4 5 xrneq12i
` |-  ( ( R |` A ) |X. ( S |` A ) ) = ( ( R i^i ( A X. ran ( R |` A ) ) ) |X. ( S i^i ( A X. ran ( S |` A ) ) ) )`
7 simp1
` |-  ( ( A e. V /\ R e. W /\ ( S |` A ) e. X ) -> A e. V )`
8 resexg
` |-  ( R e. W -> ( R |` A ) e. _V )`
9 rnexg
` |-  ( ( R |` A ) e. _V -> ran ( R |` A ) e. _V )`
10 8 9 syl
` |-  ( R e. W -> ran ( R |` A ) e. _V )`
` |-  ( ( A e. V /\ R e. W /\ ( S |` A ) e. X ) -> ran ( R |` A ) e. _V )`
12 rnexg
` |-  ( ( S |` A ) e. X -> ran ( S |` A ) e. _V )`
` |-  ( ( A e. V /\ R e. W /\ ( S |` A ) e. X ) -> ran ( S |` A ) e. _V )`
` |-  ( ( R i^i ( A X. ran ( R |` A ) ) ) |X. ( S i^i ( A X. ran ( S |` A ) ) ) ) = ( ( R |X. S ) i^i ( A X. ( ran ( R |` A ) X. ran ( S |` A ) ) ) )`
` |-  ( ( A e. V /\ ran ( R |` A ) e. _V /\ ran ( S |` A ) e. _V ) -> ( ( R |X. S ) i^i ( A X. ( ran ( R |` A ) X. ran ( S |` A ) ) ) ) e. _V )`
` |-  ( ( A e. V /\ ran ( R |` A ) e. _V /\ ran ( S |` A ) e. _V ) -> ( ( R i^i ( A X. ran ( R |` A ) ) ) |X. ( S i^i ( A X. ran ( S |` A ) ) ) ) e. _V )`
` |-  ( ( A e. V /\ R e. W /\ ( S |` A ) e. X ) -> ( ( R i^i ( A X. ran ( R |` A ) ) ) |X. ( S i^i ( A X. ran ( S |` A ) ) ) ) e. _V )`
` |-  ( ( A e. V /\ R e. W /\ ( S |` A ) e. X ) -> ( ( R |` A ) |X. ( S |` A ) ) e. _V )`
` |-  ( ( A e. V /\ R e. W /\ ( S |` A ) e. X ) -> ( R |X. ( S |` A ) ) e. _V )`