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 ◡ 𝐹 ∧ ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ 𝐶 ∧ ( 𝐹 ↾ 𝐵 ) : 𝐵 –onto→ 𝐷 ) → ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) : ( 𝐴 ∖ 𝐵 ) –1-1-onto→ ( 𝐶 ∖ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 fofun ⊢ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ 𝐶 → Fun ( 𝐹 ↾ 𝐴 ) )
2 difss ⊢ ( 𝐴 ∖ 𝐵 ) ⊆ 𝐴
3 fof ⊢ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ 𝐶 → ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ 𝐶 )
4 3 fdmd ⊢ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ 𝐶 → dom ( 𝐹 ↾ 𝐴 ) = 𝐴 )
5 2 4 sseqtrrid ⊢ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ 𝐶 → ( 𝐴 ∖ 𝐵 ) ⊆ dom ( 𝐹 ↾ 𝐴 ) )
6 fores ⊢ ( ( Fun ( 𝐹 ↾ 𝐴 ) ∧ ( 𝐴 ∖ 𝐵 ) ⊆ dom ( 𝐹 ↾ 𝐴 ) ) → ( ( 𝐹 ↾ 𝐴 ) ↾ ( 𝐴 ∖ 𝐵 ) ) : ( 𝐴 ∖ 𝐵 ) –onto→ ( ( 𝐹 ↾ 𝐴 ) “ ( 𝐴 ∖ 𝐵 ) ) )
7 1 5 6 syl2anc ⊢ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ 𝐶 → ( ( 𝐹 ↾ 𝐴 ) ↾ ( 𝐴 ∖ 𝐵 ) ) : ( 𝐴 ∖ 𝐵 ) –onto→ ( ( 𝐹 ↾ 𝐴 ) “ ( 𝐴 ∖ 𝐵 ) ) )
8 resres ⊢ ( ( 𝐹 ↾ 𝐴 ) ↾ ( 𝐴 ∖ 𝐵 ) ) = ( 𝐹 ↾ ( 𝐴 ∩ ( 𝐴 ∖ 𝐵 ) ) )
9 indif ⊢ ( 𝐴 ∩ ( 𝐴 ∖ 𝐵 ) ) = ( 𝐴 ∖ 𝐵 )
10 9 reseq2i ⊢ ( 𝐹 ↾ ( 𝐴 ∩ ( 𝐴 ∖ 𝐵 ) ) ) = ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) )
11 8 10 eqtri ⊢ ( ( 𝐹 ↾ 𝐴 ) ↾ ( 𝐴 ∖ 𝐵 ) ) = ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) )
12 foeq1 ⊢ ( ( ( 𝐹 ↾ 𝐴 ) ↾ ( 𝐴 ∖ 𝐵 ) ) = ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) → ( ( ( 𝐹 ↾ 𝐴 ) ↾ ( 𝐴 ∖ 𝐵 ) ) : ( 𝐴 ∖ 𝐵 ) –onto→ ( ( 𝐹 ↾ 𝐴 ) “ ( 𝐴 ∖ 𝐵 ) ) ↔ ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) : ( 𝐴 ∖ 𝐵 ) –onto→ ( ( 𝐹 ↾ 𝐴 ) “ ( 𝐴 ∖ 𝐵 ) ) ) )
13 11 12 ax-mp ⊢ ( ( ( 𝐹 ↾ 𝐴 ) ↾ ( 𝐴 ∖ 𝐵 ) ) : ( 𝐴 ∖ 𝐵 ) –onto→ ( ( 𝐹 ↾ 𝐴 ) “ ( 𝐴 ∖ 𝐵 ) ) ↔ ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) : ( 𝐴 ∖ 𝐵 ) –onto→ ( ( 𝐹 ↾ 𝐴 ) “ ( 𝐴 ∖ 𝐵 ) ) )
14 11 rneqi ⊢ ran ( ( 𝐹 ↾ 𝐴 ) ↾ ( 𝐴 ∖ 𝐵 ) ) = ran ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) )
15 df-ima ⊢ ( ( 𝐹 ↾ 𝐴 ) “ ( 𝐴 ∖ 𝐵 ) ) = ran ( ( 𝐹 ↾ 𝐴 ) ↾ ( 𝐴 ∖ 𝐵 ) )
16 df-ima ⊢ ( 𝐹 “ ( 𝐴 ∖ 𝐵 ) ) = ran ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) )
17 14 15 16 3eqtr4i ⊢ ( ( 𝐹 ↾ 𝐴 ) “ ( 𝐴 ∖ 𝐵 ) ) = ( 𝐹 “ ( 𝐴 ∖ 𝐵 ) )
18 foeq3 ⊢ ( ( ( 𝐹 ↾ 𝐴 ) “ ( 𝐴 ∖ 𝐵 ) ) = ( 𝐹 “ ( 𝐴 ∖ 𝐵 ) ) → ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) : ( 𝐴 ∖ 𝐵 ) –onto→ ( ( 𝐹 ↾ 𝐴 ) “ ( 𝐴 ∖ 𝐵 ) ) ↔ ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) : ( 𝐴 ∖ 𝐵 ) –onto→ ( 𝐹 “ ( 𝐴 ∖ 𝐵 ) ) ) )
19 17 18 ax-mp ⊢ ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) : ( 𝐴 ∖ 𝐵 ) –onto→ ( ( 𝐹 ↾ 𝐴 ) “ ( 𝐴 ∖ 𝐵 ) ) ↔ ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) : ( 𝐴 ∖ 𝐵 ) –onto→ ( 𝐹 “ ( 𝐴 ∖ 𝐵 ) ) )
20 13 19 bitri ⊢ ( ( ( 𝐹 ↾ 𝐴 ) ↾ ( 𝐴 ∖ 𝐵 ) ) : ( 𝐴 ∖ 𝐵 ) –onto→ ( ( 𝐹 ↾ 𝐴 ) “ ( 𝐴 ∖ 𝐵 ) ) ↔ ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) : ( 𝐴 ∖ 𝐵 ) –onto→ ( 𝐹 “ ( 𝐴 ∖ 𝐵 ) ) )
21 7 20 sylib ⊢ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ 𝐶 → ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) : ( 𝐴 ∖ 𝐵 ) –onto→ ( 𝐹 “ ( 𝐴 ∖ 𝐵 ) ) )
22 funres11 ⊢ ( Fun ◡ 𝐹 → Fun ◡ ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) )
23 dff1o3 ⊢ ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) : ( 𝐴 ∖ 𝐵 ) –1-1-onto→ ( 𝐹 “ ( 𝐴 ∖ 𝐵 ) ) ↔ ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) : ( 𝐴 ∖ 𝐵 ) –onto→ ( 𝐹 “ ( 𝐴 ∖ 𝐵 ) ) ∧ Fun ◡ ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ) )
24 23 biimpri ⊢ ( ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) : ( 𝐴 ∖ 𝐵 ) –onto→ ( 𝐹 “ ( 𝐴 ∖ 𝐵 ) ) ∧ Fun ◡ ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ) → ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) : ( 𝐴 ∖ 𝐵 ) –1-1-onto→ ( 𝐹 “ ( 𝐴 ∖ 𝐵 ) ) )
25 21 22 24 syl2anr ⊢ ( ( Fun ◡ 𝐹 ∧ ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ 𝐶 ) → ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) : ( 𝐴 ∖ 𝐵 ) –1-1-onto→ ( 𝐹 “ ( 𝐴 ∖ 𝐵 ) ) )
26 25 3adant3 ⊢ ( ( Fun ◡ 𝐹 ∧ ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ 𝐶 ∧ ( 𝐹 ↾ 𝐵 ) : 𝐵 –onto→ 𝐷 ) → ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) : ( 𝐴 ∖ 𝐵 ) –1-1-onto→ ( 𝐹 “ ( 𝐴 ∖ 𝐵 ) ) )
27 df-ima ⊢ ( 𝐹 “ 𝐴 ) = ran ( 𝐹 ↾ 𝐴 )
28 forn ⊢ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ 𝐶 → ran ( 𝐹 ↾ 𝐴 ) = 𝐶 )
29 27 28 syl5eq ⊢ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ 𝐶 → ( 𝐹 “ 𝐴 ) = 𝐶 )
30 df-ima ⊢ ( 𝐹 “ 𝐵 ) = ran ( 𝐹 ↾ 𝐵 )
31 forn ⊢ ( ( 𝐹 ↾ 𝐵 ) : 𝐵 –onto→ 𝐷 → ran ( 𝐹 ↾ 𝐵 ) = 𝐷 )
32 30 31 syl5eq ⊢ ( ( 𝐹 ↾ 𝐵 ) : 𝐵 –onto→ 𝐷 → ( 𝐹 “ 𝐵 ) = 𝐷 )
33 29 32 anim12i ⊢ ( ( ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ 𝐶 ∧ ( 𝐹 ↾ 𝐵 ) : 𝐵 –onto→ 𝐷 ) → ( ( 𝐹 “ 𝐴 ) = 𝐶 ∧ ( 𝐹 “ 𝐵 ) = 𝐷 ) )
34 imadif ⊢ ( Fun ◡ 𝐹 → ( 𝐹 “ ( 𝐴 ∖ 𝐵 ) ) = ( ( 𝐹 “ 𝐴 ) ∖ ( 𝐹 “ 𝐵 ) ) )
35 difeq12 ⊢ ( ( ( 𝐹 “ 𝐴 ) = 𝐶 ∧ ( 𝐹 “ 𝐵 ) = 𝐷 ) → ( ( 𝐹 “ 𝐴 ) ∖ ( 𝐹 “ 𝐵 ) ) = ( 𝐶 ∖ 𝐷 ) )
36 34 35 sylan9eq ⊢ ( ( Fun ◡ 𝐹 ∧ ( ( 𝐹 “ 𝐴 ) = 𝐶 ∧ ( 𝐹 “ 𝐵 ) = 𝐷 ) ) → ( 𝐹 “ ( 𝐴 ∖ 𝐵 ) ) = ( 𝐶 ∖ 𝐷 ) )
37 33 36 sylan2 ⊢ ( ( Fun ◡ 𝐹 ∧ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ 𝐶 ∧ ( 𝐹 ↾ 𝐵 ) : 𝐵 –onto→ 𝐷 ) ) → ( 𝐹 “ ( 𝐴 ∖ 𝐵 ) ) = ( 𝐶 ∖ 𝐷 ) )
38 37 3impb ⊢ ( ( Fun ◡ 𝐹 ∧ ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ 𝐶 ∧ ( 𝐹 ↾ 𝐵 ) : 𝐵 –onto→ 𝐷 ) → ( 𝐹 “ ( 𝐴 ∖ 𝐵 ) ) = ( 𝐶 ∖ 𝐷 ) )
39 38 f1oeq3d ⊢ ( ( Fun ◡ 𝐹 ∧ ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ 𝐶 ∧ ( 𝐹 ↾ 𝐵 ) : 𝐵 –onto→ 𝐷 ) → ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) : ( 𝐴 ∖ 𝐵 ) –1-1-onto→ ( 𝐹 “ ( 𝐴 ∖ 𝐵 ) ) ↔ ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) : ( 𝐴 ∖ 𝐵 ) –1-1-onto→ ( 𝐶 ∖ 𝐷 ) ) )
40 26 39 mpbid ⊢ ( ( Fun ◡ 𝐹 ∧ ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ 𝐶 ∧ ( 𝐹 ↾ 𝐵 ) : 𝐵 –onto→ 𝐷 ) → ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) : ( 𝐴 ∖ 𝐵 ) –1-1-onto→ ( 𝐶 ∖ 𝐷 ) )