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

Metamath Proof Explorer

Theorem resin

Description: The restriction of a one-to-one onto function to an intersection maps onto the intersection of the images. (Contributed by Paul Chapman, 11-Apr-2009)

Ref Expression
Assertion resin ⊢ Fun ⁡ F -1 ∧ F ↾ A : A ⟶ onto C ∧ F ↾ B : B ⟶ onto D → F ↾ A ∩ B : A ∩ B ⟶ 1-1 onto C ∩ D

Proof

Step Hyp Ref Expression
1 resdif ⊢ Fun ⁡ F -1 ∧ F ↾ A : A ⟶ onto C ∧ F ↾ B : B ⟶ onto D → F ↾ A ∖ B : A ∖ B ⟶ 1-1 onto C ∖ D
2 f1ofo ⊢ F ↾ A ∖ B : A ∖ B ⟶ 1-1 onto C ∖ D → F ↾ A ∖ B : A ∖ B ⟶ onto C ∖ D
3 1 2 syl ⊢ Fun ⁡ F -1 ∧ F ↾ A : A ⟶ onto C ∧ F ↾ B : B ⟶ onto D → F ↾ A ∖ B : A ∖ B ⟶ onto C ∖ D
4 resdif ⊢ Fun ⁡ F -1 ∧ F ↾ A : A ⟶ onto C ∧ F ↾ A ∖ B : A ∖ B ⟶ onto C ∖ D → F ↾ A ∖ A ∖ B : A ∖ A ∖ B ⟶ 1-1 onto C ∖ C ∖ D
5 3 4 syld3an3 ⊢ Fun ⁡ F -1 ∧ F ↾ A : A ⟶ onto C ∧ F ↾ B : B ⟶ onto D → F ↾ A ∖ A ∖ B : A ∖ A ∖ B ⟶ 1-1 onto C ∖ C ∖ D
6 dfin4 ⊢ C ∩ D = C ∖ C ∖ D
7 f1oeq3 ⊢ C ∩ D = C ∖ C ∖ D → F ↾ A ∩ B : A ∩ B ⟶ 1-1 onto C ∩ D ↔ F ↾ A ∩ B : A ∩ B ⟶ 1-1 onto C ∖ C ∖ D
8 6 7 ax-mp ⊢ F ↾ A ∩ B : A ∩ B ⟶ 1-1 onto C ∩ D ↔ F ↾ A ∩ B : A ∩ B ⟶ 1-1 onto C ∖ C ∖ D
9 dfin4 ⊢ A ∩ B = A ∖ A ∖ B
10 f1oeq2 ⊢ A ∩ B = A ∖ A ∖ B → F ↾ A ∩ B : A ∩ B ⟶ 1-1 onto C ∖ C ∖ D ↔ F ↾ A ∩ B : A ∖ A ∖ B ⟶ 1-1 onto C ∖ C ∖ D
11 9 10 ax-mp ⊢ F ↾ A ∩ B : A ∩ B ⟶ 1-1 onto C ∖ C ∖ D ↔ F ↾ A ∩ B : A ∖ A ∖ B ⟶ 1-1 onto C ∖ C ∖ D
12 9 reseq2i ⊢ F ↾ A ∩ B = F ↾ A ∖ A ∖ B
13 f1oeq1 ⊢ F ↾ A ∩ B = F ↾ A ∖ A ∖ B → F ↾ A ∩ B : A ∖ A ∖ B ⟶ 1-1 onto C ∖ C ∖ D ↔ F ↾ A ∖ A ∖ B : A ∖ A ∖ B ⟶ 1-1 onto C ∖ C ∖ D
14 12 13 ax-mp ⊢ F ↾ A ∩ B : A ∖ A ∖ B ⟶ 1-1 onto C ∖ C ∖ D ↔ F ↾ A ∖ A ∖ B : A ∖ A ∖ B ⟶ 1-1 onto C ∖ C ∖ D
15 8 11 14 3bitrri ⊢ F ↾ A ∖ A ∖ B : A ∖ A ∖ B ⟶ 1-1 onto C ∖ C ∖ D ↔ F ↾ A ∩ B : A ∩ B ⟶ 1-1 onto C ∩ D
16 5 15 sylib ⊢ Fun ⁡ F -1 ∧ F ↾ A : A ⟶ onto C ∧ F ↾ B : B ⟶ onto D → F ↾ A ∩ B : A ∩ B ⟶ 1-1 onto C ∩ D