This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ R ⋉ S ↾ A = R ↾ A ⋉ S ↾ A

Proof

Step Hyp Ref Expression
1 resco ⊢ 1 st ↾ V × V -1 ∘ R ↾ A = 1 st ↾ V × V -1 ∘ R ↾ A
2 resco ⊢ 2 nd ↾ V × V -1 ∘ S ↾ A = 2 nd ↾ V × V -1 ∘ S ↾ A
3 1 2 ineq12i ⊢ 1 st ↾ V × V -1 ∘ R ↾ A ∩ 2 nd ↾ V × V -1 ∘ S ↾ A = 1 st ↾ V × V -1 ∘ R ↾ A ∩ 2 nd ↾ V × V -1 ∘ S ↾ A
4 df-xrn ⊢ R ⋉ S = 1 st ↾ V × V -1 ∘ R ∩ 2 nd ↾ V × V -1 ∘ S
5 4 reseq1i ⊢ R ⋉ S ↾ A = 1 st ↾ V × V -1 ∘ R ∩ 2 nd ↾ V × V -1 ∘ S ↾ A
6 resindir ⊢ 1 st ↾ V × V -1 ∘ R ∩ 2 nd ↾ V × V -1 ∘ S ↾ A = 1 st ↾ V × V -1 ∘ R ↾ A ∩ 2 nd ↾ V × V -1 ∘ S ↾ A
7 5 6 eqtri ⊢ R ⋉ S ↾ A = 1 st ↾ V × V -1 ∘ R ↾ A ∩ 2 nd ↾ V × V -1 ∘ S ↾ A
8 df-xrn ⊢ R ↾ A ⋉ S ↾ A = 1 st ↾ V × V -1 ∘ R ↾ A ∩ 2 nd ↾ V × V -1 ∘ S ↾ A
9 3 7 8 3eqtr4i ⊢ R ⋉ S ↾ A = R ↾ A ⋉ S ↾ A