Metamath Proof Explorer

Theorem xrnres3

Description: Two ways to express restriction of range Cartesian product, see also xrnres , xrnres2 . (Contributed by Peter Mazsa, 28-Mar-2020)

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

Proof

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