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 ∈ V ∧ R ∈ W ∧ S ↾ A ∈ X → R ⋉ S ↾ A ∈ V

Proof

Step Hyp Ref Expression
1 xrnres3 ⊢ R ⋉ S ↾ A = R ↾ A ⋉ S ↾ A
2 xrnres2 ⊢ R ⋉ S ↾ A = R ⋉ S ↾ A
3 1 2 eqtr3i ⊢ R ↾ A ⋉ S ↾ A = R ⋉ S ↾ A
4 dfres4 ⊢ R ↾ A = R ∩ A × ran ⁡ R ↾ A
5 dfres4 ⊢ S ↾ A = S ∩ A × ran ⁡ S ↾ A
6 4 5 xrneq12i ⊢ R ↾ A ⋉ S ↾ A = R ∩ A × ran ⁡ R ↾ A ⋉ S ∩ A × ran ⁡ S ↾ A
7 simp1 ⊢ A ∈ V ∧ R ∈ W ∧ S ↾ A ∈ X → A ∈ V
8 resexg ⊢ R ∈ W → R ↾ A ∈ V
9 rnexg ⊢ R ↾ A ∈ V → ran ⁡ R ↾ A ∈ V
10 8 9 syl ⊢ R ∈ W → ran ⁡ R ↾ A ∈ V
11 10 3ad2ant2 ⊢ A ∈ V ∧ R ∈ W ∧ S ↾ A ∈ X → ran ⁡ R ↾ A ∈ V
12 rnexg ⊢ S ↾ A ∈ X → ran ⁡ S ↾ A ∈ V
13 12 3ad2ant3 ⊢ A ∈ V ∧ R ∈ W ∧ S ↾ A ∈ X → ran ⁡ S ↾ A ∈ V
14 inxpxrn ⊢ R ∩ A × ran ⁡ R ↾ A ⋉ S ∩ A × ran ⁡ S ↾ A = R ⋉ S ∩ A × ran ⁡ R ↾ A × ran ⁡ S ↾ A
15 xrninxpex ⊢ A ∈ V ∧ ran ⁡ R ↾ A ∈ V ∧ ran ⁡ S ↾ A ∈ V → R ⋉ S ∩ A × ran ⁡ R ↾ A × ran ⁡ S ↾ A ∈ V
16 14 15 eqeltrid ⊢ A ∈ V ∧ ran ⁡ R ↾ A ∈ V ∧ ran ⁡ S ↾ A ∈ V → R ∩ A × ran ⁡ R ↾ A ⋉ S ∩ A × ran ⁡ S ↾ A ∈ V
17 7 11 13 16 syl3anc ⊢ A ∈ V ∧ R ∈ W ∧ S ↾ A ∈ X → R ∩ A × ran ⁡ R ↾ A ⋉ S ∩ A × ran ⁡ S ↾ A ∈ V
18 6 17 eqeltrid ⊢ A ∈ V ∧ R ∈ W ∧ S ↾ A ∈ X → R ↾ A ⋉ S ↾ A ∈ V
19 3 18 eqeltrrid ⊢ A ∈ V ∧ R ∈ W ∧ S ↾ A ∈ X → R ⋉ S ↾ A ∈ V