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 )
11 10 3ad2ant2 
 |-  ( ( 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 )
13 12 3ad2ant3 
 |-  ( ( A e. V /\ R e. W /\ ( S |` A ) e. X ) -> ran ( S |` A ) e. _V )
14 inxpxrn 
 |-  ( ( 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 ) ) ) )
15 xrninxpex 
 |-  ( ( 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 )
16 14 15 eqeltrid 
 |-  ( ( 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 )
17 7 11 13 16 syl3anc 
 |-  ( ( 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 )
18 6 17 eqeltrid 
 |-  ( ( A e. V /\ R e. W /\ ( S |` A ) e. X ) -> ( ( R |` A ) |X. ( S |` A ) ) e. _V )
19 3 18 eqeltrrid 
 |-  ( ( A e. V /\ R e. W /\ ( S |` A ) e. X ) -> ( R |X. ( S |` A ) ) e. _V )