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