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

Proof

Step	Hyp	Ref	Expression
1		resdif	⊢ ( ( Fun ◡ 𝐹 ∧ ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ 𝐶 ∧ ( 𝐹 ↾ 𝐵 ) : 𝐵 –onto→ 𝐷 ) → ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) : ( 𝐴 ∖ 𝐵 ) –1-1-onto→ ( 𝐶 ∖ 𝐷 ) )
2		f1ofo	⊢ ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) : ( 𝐴 ∖ 𝐵 ) –1-1-onto→ ( 𝐶 ∖ 𝐷 ) → ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) : ( 𝐴 ∖ 𝐵 ) –onto→ ( 𝐶 ∖ 𝐷 ) )
3	1 2	syl	⊢ ( ( Fun ◡ 𝐹 ∧ ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ 𝐶 ∧ ( 𝐹 ↾ 𝐵 ) : 𝐵 –onto→ 𝐷 ) → ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) : ( 𝐴 ∖ 𝐵 ) –onto→ ( 𝐶 ∖ 𝐷 ) )
4		resdif	⊢ ( ( Fun ◡ 𝐹 ∧ ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ 𝐶 ∧ ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) : ( 𝐴 ∖ 𝐵 ) –onto→ ( 𝐶 ∖ 𝐷 ) ) → ( 𝐹 ↾ ( 𝐴 ∖ ( 𝐴 ∖ 𝐵 ) ) ) : ( 𝐴 ∖ ( 𝐴 ∖ 𝐵 ) ) –1-1-onto→ ( 𝐶 ∖ ( 𝐶 ∖ 𝐷 ) ) )
5	3 4	syld3an3	⊢ ( ( Fun ◡ 𝐹 ∧ ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ 𝐶 ∧ ( 𝐹 ↾ 𝐵 ) : 𝐵 –onto→ 𝐷 ) → ( 𝐹 ↾ ( 𝐴 ∖ ( 𝐴 ∖ 𝐵 ) ) ) : ( 𝐴 ∖ ( 𝐴 ∖ 𝐵 ) ) –1-1-onto→ ( 𝐶 ∖ ( 𝐶 ∖ 𝐷 ) ) )
6		dfin4	⊢ ( 𝐶 ∩ 𝐷 ) = ( 𝐶 ∖ ( 𝐶 ∖ 𝐷 ) )
7		f1oeq3	⊢ ( ( 𝐶 ∩ 𝐷 ) = ( 𝐶 ∖ ( 𝐶 ∖ 𝐷 ) ) → ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) : ( 𝐴 ∩ 𝐵 ) –1-1-onto→ ( 𝐶 ∩ 𝐷 ) ↔ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) : ( 𝐴 ∩ 𝐵 ) –1-1-onto→ ( 𝐶 ∖ ( 𝐶 ∖ 𝐷 ) ) ) )
8	6 7	ax-mp	⊢ ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) : ( 𝐴 ∩ 𝐵 ) –1-1-onto→ ( 𝐶 ∩ 𝐷 ) ↔ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) : ( 𝐴 ∩ 𝐵 ) –1-1-onto→ ( 𝐶 ∖ ( 𝐶 ∖ 𝐷 ) ) )
9		dfin4	⊢ ( 𝐴 ∩ 𝐵 ) = ( 𝐴 ∖ ( 𝐴 ∖ 𝐵 ) )
10		f1oeq2	⊢ ( ( 𝐴 ∩ 𝐵 ) = ( 𝐴 ∖ ( 𝐴 ∖ 𝐵 ) ) → ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) : ( 𝐴 ∩ 𝐵 ) –1-1-onto→ ( 𝐶 ∖ ( 𝐶 ∖ 𝐷 ) ) ↔ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) : ( 𝐴 ∖ ( 𝐴 ∖ 𝐵 ) ) –1-1-onto→ ( 𝐶 ∖ ( 𝐶 ∖ 𝐷 ) ) ) )
11	9 10	ax-mp	⊢ ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) : ( 𝐴 ∩ 𝐵 ) –1-1-onto→ ( 𝐶 ∖ ( 𝐶 ∖ 𝐷 ) ) ↔ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) : ( 𝐴 ∖ ( 𝐴 ∖ 𝐵 ) ) –1-1-onto→ ( 𝐶 ∖ ( 𝐶 ∖ 𝐷 ) ) )
12	9	reseq2i	⊢ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐹 ↾ ( 𝐴 ∖ ( 𝐴 ∖ 𝐵 ) ) )
13		f1oeq1	⊢ ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐹 ↾ ( 𝐴 ∖ ( 𝐴 ∖ 𝐵 ) ) ) → ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) : ( 𝐴 ∖ ( 𝐴 ∖ 𝐵 ) ) –1-1-onto→ ( 𝐶 ∖ ( 𝐶 ∖ 𝐷 ) ) ↔ ( 𝐹 ↾ ( 𝐴 ∖ ( 𝐴 ∖ 𝐵 ) ) ) : ( 𝐴 ∖ ( 𝐴 ∖ 𝐵 ) ) –1-1-onto→ ( 𝐶 ∖ ( 𝐶 ∖ 𝐷 ) ) ) )
14	12 13	ax-mp	⊢ ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) : ( 𝐴 ∖ ( 𝐴 ∖ 𝐵 ) ) –1-1-onto→ ( 𝐶 ∖ ( 𝐶 ∖ 𝐷 ) ) ↔ ( 𝐹 ↾ ( 𝐴 ∖ ( 𝐴 ∖ 𝐵 ) ) ) : ( 𝐴 ∖ ( 𝐴 ∖ 𝐵 ) ) –1-1-onto→ ( 𝐶 ∖ ( 𝐶 ∖ 𝐷 ) ) )
15	8 11 14	3bitrri	⊢ ( ( 𝐹 ↾ ( 𝐴 ∖ ( 𝐴 ∖ 𝐵 ) ) ) : ( 𝐴 ∖ ( 𝐴 ∖ 𝐵 ) ) –1-1-onto→ ( 𝐶 ∖ ( 𝐶 ∖ 𝐷 ) ) ↔ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) : ( 𝐴 ∩ 𝐵 ) –1-1-onto→ ( 𝐶 ∩ 𝐷 ) )
16	5 15	sylib	⊢ ( ( Fun ◡ 𝐹 ∧ ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ 𝐶 ∧ ( 𝐹 ↾ 𝐵 ) : 𝐵 –onto→ 𝐷 ) → ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) : ( 𝐴 ∩ 𝐵 ) –1-1-onto→ ( 𝐶 ∩ 𝐷 ) )