Metamath Proof Explorer


Theorem xrnres

Description: Two ways to express restriction of range Cartesian product, see also xrnres2 , xrnres3 . (Contributed by Peter Mazsa, 5-Jun-2021)

Ref Expression
Assertion xrnres ( ( 𝑅𝑆 ) ↾ 𝐴 ) = ( ( 𝑅𝐴 ) ⋉ 𝑆 )

Proof

Step Hyp Ref Expression
1 resco ( ( ( 1st ↾ ( V × V ) ) ∘ 𝑅 ) ↾ 𝐴 ) = ( ( 1st ↾ ( V × V ) ) ∘ ( 𝑅𝐴 ) )
2 1 ineq1i ( ( ( ( 1st ↾ ( V × V ) ) ∘ 𝑅 ) ↾ 𝐴 ) ∩ ( ( 2nd ↾ ( V × V ) ) ∘ 𝑆 ) ) = ( ( ( 1st ↾ ( V × V ) ) ∘ ( 𝑅𝐴 ) ) ∩ ( ( 2nd ↾ ( V × V ) ) ∘ 𝑆 ) )
3 df-xrn ( 𝑅𝑆 ) = ( ( ( 1st ↾ ( V × V ) ) ∘ 𝑅 ) ∩ ( ( 2nd ↾ ( V × V ) ) ∘ 𝑆 ) )
4 3 reseq1i ( ( 𝑅𝑆 ) ↾ 𝐴 ) = ( ( ( ( 1st ↾ ( V × V ) ) ∘ 𝑅 ) ∩ ( ( 2nd ↾ ( V × V ) ) ∘ 𝑆 ) ) ↾ 𝐴 )
5 inres2 ( ( ( ( 1st ↾ ( V × V ) ) ∘ 𝑅 ) ↾ 𝐴 ) ∩ ( ( 2nd ↾ ( V × V ) ) ∘ 𝑆 ) ) = ( ( ( ( 1st ↾ ( V × V ) ) ∘ 𝑅 ) ∩ ( ( 2nd ↾ ( V × V ) ) ∘ 𝑆 ) ) ↾ 𝐴 )
6 4 5 eqtr4i ( ( 𝑅𝑆 ) ↾ 𝐴 ) = ( ( ( ( 1st ↾ ( V × V ) ) ∘ 𝑅 ) ↾ 𝐴 ) ∩ ( ( 2nd ↾ ( V × V ) ) ∘ 𝑆 ) )
7 df-xrn ( ( 𝑅𝐴 ) ⋉ 𝑆 ) = ( ( ( 1st ↾ ( V × V ) ) ∘ ( 𝑅𝐴 ) ) ∩ ( ( 2nd ↾ ( V × V ) ) ∘ 𝑆 ) )
8 2 6 7 3eqtr4i ( ( 𝑅𝑆 ) ↾ 𝐴 ) = ( ( 𝑅𝐴 ) ⋉ 𝑆 )