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 )