# 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 ( ( 𝐴𝑉𝑅𝑊 ∧ ( 𝑆𝐴 ) ∈ 𝑋 ) → ( 𝑅 ⋉ ( 𝑆𝐴 ) ) ∈ V )

### Proof

Step Hyp Ref Expression
1 xrnres3 ( ( 𝑅𝑆 ) ↾ 𝐴 ) = ( ( 𝑅𝐴 ) ⋉ ( 𝑆𝐴 ) )
2 xrnres2 ( ( 𝑅𝑆 ) ↾ 𝐴 ) = ( 𝑅 ⋉ ( 𝑆𝐴 ) )
3 1 2 eqtr3i ( ( 𝑅𝐴 ) ⋉ ( 𝑆𝐴 ) ) = ( 𝑅 ⋉ ( 𝑆𝐴 ) )
4 dfres4 ( 𝑅𝐴 ) = ( 𝑅 ∩ ( 𝐴 × ran ( 𝑅𝐴 ) ) )
5 dfres4 ( 𝑆𝐴 ) = ( 𝑆 ∩ ( 𝐴 × ran ( 𝑆𝐴 ) ) )
6 4 5 xrneq12i ( ( 𝑅𝐴 ) ⋉ ( 𝑆𝐴 ) ) = ( ( 𝑅 ∩ ( 𝐴 × ran ( 𝑅𝐴 ) ) ) ⋉ ( 𝑆 ∩ ( 𝐴 × ran ( 𝑆𝐴 ) ) ) )
7 simp1 ( ( 𝐴𝑉𝑅𝑊 ∧ ( 𝑆𝐴 ) ∈ 𝑋 ) → 𝐴𝑉 )
8 resexg ( 𝑅𝑊 → ( 𝑅𝐴 ) ∈ V )
9 rnexg ( ( 𝑅𝐴 ) ∈ V → ran ( 𝑅𝐴 ) ∈ V )
10 8 9 syl ( 𝑅𝑊 → ran ( 𝑅𝐴 ) ∈ V )
11 10 3ad2ant2 ( ( 𝐴𝑉𝑅𝑊 ∧ ( 𝑆𝐴 ) ∈ 𝑋 ) → ran ( 𝑅𝐴 ) ∈ V )
12 rnexg ( ( 𝑆𝐴 ) ∈ 𝑋 → ran ( 𝑆𝐴 ) ∈ V )
13 12 3ad2ant3 ( ( 𝐴𝑉𝑅𝑊 ∧ ( 𝑆𝐴 ) ∈ 𝑋 ) → ran ( 𝑆𝐴 ) ∈ V )
14 inxpxrn ( ( 𝑅 ∩ ( 𝐴 × ran ( 𝑅𝐴 ) ) ) ⋉ ( 𝑆 ∩ ( 𝐴 × ran ( 𝑆𝐴 ) ) ) ) = ( ( 𝑅𝑆 ) ∩ ( 𝐴 × ( ran ( 𝑅𝐴 ) × ran ( 𝑆𝐴 ) ) ) )
15 xrninxpex ( ( 𝐴𝑉 ∧ ran ( 𝑅𝐴 ) ∈ V ∧ ran ( 𝑆𝐴 ) ∈ V ) → ( ( 𝑅𝑆 ) ∩ ( 𝐴 × ( ran ( 𝑅𝐴 ) × ran ( 𝑆𝐴 ) ) ) ) ∈ V )
16 14 15 eqeltrid ( ( 𝐴𝑉 ∧ ran ( 𝑅𝐴 ) ∈ V ∧ ran ( 𝑆𝐴 ) ∈ V ) → ( ( 𝑅 ∩ ( 𝐴 × ran ( 𝑅𝐴 ) ) ) ⋉ ( 𝑆 ∩ ( 𝐴 × ran ( 𝑆𝐴 ) ) ) ) ∈ V )
17 7 11 13 16 syl3anc ( ( 𝐴𝑉𝑅𝑊 ∧ ( 𝑆𝐴 ) ∈ 𝑋 ) → ( ( 𝑅 ∩ ( 𝐴 × ran ( 𝑅𝐴 ) ) ) ⋉ ( 𝑆 ∩ ( 𝐴 × ran ( 𝑆𝐴 ) ) ) ) ∈ V )
18 6 17 eqeltrid ( ( 𝐴𝑉𝑅𝑊 ∧ ( 𝑆𝐴 ) ∈ 𝑋 ) → ( ( 𝑅𝐴 ) ⋉ ( 𝑆𝐴 ) ) ∈ V )
19 3 18 eqeltrrid ( ( 𝐴𝑉𝑅𝑊 ∧ ( 𝑆𝐴 ) ∈ 𝑋 ) → ( 𝑅 ⋉ ( 𝑆𝐴 ) ) ∈ V )