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

Metamath Proof Explorer

Theorem xrnres2

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

Ref Expression
Assertion xrnres2 ⊢ R ⋉ S ↾ A = R ⋉ S ↾ A

Proof

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