Metamath Proof Explorer

Theorem resdif

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

Ref Expression
Assertion resdif ⊢ 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 fofun ⊢ F ↾ A : A ⟶ onto C → Fun ⁡ F ↾ A
2 difss ⊢ A ∖ B ⊆ A
3 fof ⊢ F ↾ A : A ⟶ onto C → F ↾ A : A ⟶ C
4 3 fdmd ⊢ F ↾ A : A ⟶ onto C → dom ⁡ F ↾ A = A
5 2 4 sseqtrrid ⊢ F ↾ A : A ⟶ onto C → A ∖ B ⊆ dom ⁡ F ↾ A
6 fores ⊢ Fun ⁡ F ↾ A ∧ A ∖ B ⊆ dom ⁡ F ↾ A → F ↾ A ↾ A ∖ B : A ∖ B ⟶ onto F ↾ A A ∖ B
7 1 5 6 syl2anc ⊢ F ↾ A : A ⟶ onto C → F ↾ A ↾ A ∖ B : A ∖ B ⟶ onto F ↾ A A ∖ B
8 resres ⊢ F ↾ A ↾ A ∖ B = F ↾ A ∩ A ∖ B
9 indif ⊢ A ∩ A ∖ B = A ∖ B
10 9 reseq2i ⊢ F ↾ A ∩ A ∖ B = F ↾ A ∖ B
11 8 10 eqtri ⊢ F ↾ A ↾ A ∖ B = F ↾ A ∖ B
12 foeq1 ⊢ F ↾ A ↾ A ∖ B = F ↾ A ∖ B → F ↾ A ↾ A ∖ B : A ∖ B ⟶ onto F ↾ A A ∖ B ↔ F ↾ A ∖ B : A ∖ B ⟶ onto F ↾ A A ∖ B
13 11 12 ax-mp ⊢ F ↾ A ↾ A ∖ B : A ∖ B ⟶ onto F ↾ A A ∖ B ↔ F ↾ A ∖ B : A ∖ B ⟶ onto F ↾ A A ∖ B
14 11 rneqi ⊢ ran ⁡ F ↾ A ↾ A ∖ B = ran ⁡ F ↾ A ∖ B
15 df-ima ⊢ F ↾ A A ∖ B = ran ⁡ F ↾ A ↾ A ∖ B
16 df-ima ⊢ F A ∖ B = ran ⁡ F ↾ A ∖ B
17 14 15 16 3eqtr4i ⊢ F ↾ A A ∖ B = F A ∖ B
18 foeq3 ⊢ F ↾ A A ∖ B = F A ∖ B → F ↾ A ∖ B : A ∖ B ⟶ onto F ↾ A A ∖ B ↔ F ↾ A ∖ B : A ∖ B ⟶ onto F A ∖ B
19 17 18 ax-mp ⊢ F ↾ A ∖ B : A ∖ B ⟶ onto F ↾ A A ∖ B ↔ F ↾ A ∖ B : A ∖ B ⟶ onto F A ∖ B
20 13 19 bitri ⊢ F ↾ A ↾ A ∖ B : A ∖ B ⟶ onto F ↾ A A ∖ B ↔ F ↾ A ∖ B : A ∖ B ⟶ onto F A ∖ B
21 7 20 sylib ⊢ F ↾ A : A ⟶ onto C → F ↾ A ∖ B : A ∖ B ⟶ onto F A ∖ B
22 funres11 ⊢ Fun ⁡ F -1 → Fun ⁡ F ↾ A ∖ B -1
23 dff1o3 ⊢ F ↾ A ∖ B : A ∖ B ⟶ 1-1 onto F A ∖ B ↔ F ↾ A ∖ B : A ∖ B ⟶ onto F A ∖ B ∧ Fun ⁡ F ↾ A ∖ B -1
24 23 biimpri ⊢ F ↾ A ∖ B : A ∖ B ⟶ onto F A ∖ B ∧ Fun ⁡ F ↾ A ∖ B -1 → F ↾ A ∖ B : A ∖ B ⟶ 1-1 onto F A ∖ B
25 21 22 24 syl2anr ⊢ Fun ⁡ F -1 ∧ F ↾ A : A ⟶ onto C → F ↾ A ∖ B : A ∖ B ⟶ 1-1 onto F A ∖ B
26 25 3adant3 ⊢ Fun ⁡ F -1 ∧ F ↾ A : A ⟶ onto C ∧ F ↾ B : B ⟶ onto D → F ↾ A ∖ B : A ∖ B ⟶ 1-1 onto F A ∖ B
27 df-ima ⊢ F A = ran ⁡ F ↾ A
28 forn ⊢ F ↾ A : A ⟶ onto C → ran ⁡ F ↾ A = C
29 27 28 syl5eq ⊢ F ↾ A : A ⟶ onto C → F A = C
30 df-ima ⊢ F B = ran ⁡ F ↾ B
31 forn ⊢ F ↾ B : B ⟶ onto D → ran ⁡ F ↾ B = D
32 30 31 syl5eq ⊢ F ↾ B : B ⟶ onto D → F B = D
33 29 32 anim12i ⊢ F ↾ A : A ⟶ onto C ∧ F ↾ B : B ⟶ onto D → F A = C ∧ F B = D
34 imadif ⊢ Fun ⁡ F -1 → F A ∖ B = F A ∖ F B
35 difeq12 ⊢ F A = C ∧ F B = D → F A ∖ F B = C ∖ D
36 34 35 sylan9eq ⊢ Fun ⁡ F -1 ∧ F A = C ∧ F B = D → F A ∖ B = C ∖ D
37 33 36 sylan2 ⊢ Fun ⁡ F -1 ∧ F ↾ A : A ⟶ onto C ∧ F ↾ B : B ⟶ onto D → F A ∖ B = C ∖ D
38 37 3impb ⊢ Fun ⁡ F -1 ∧ F ↾ A : A ⟶ onto C ∧ F ↾ B : B ⟶ onto D → F A ∖ B = C ∖ D
39 38 f1oeq3d ⊢ Fun ⁡ F -1 ∧ F ↾ A : A ⟶ onto C ∧ F ↾ B : B ⟶ onto D → F ↾ A ∖ B : A ∖ B ⟶ 1-1 onto F A ∖ B ↔ F ↾ A ∖ B : A ∖ B ⟶ 1-1 onto C ∖ D
40 26 39 mpbid ⊢ Fun ⁡ F -1 ∧ F ↾ A : A ⟶ onto C ∧ F ↾ B : B ⟶ onto D → F ↾ A ∖ B : A ∖ B ⟶ 1-1 onto C ∖ D