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

Metamath Proof Explorer

Theorem fores

Description: Restriction of an onto function. (Contributed by NM, 4-Mar-1997)

Ref Expression
Assertion fores ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ ( 𝐹 “ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 funres ⊢ ( Fun 𝐹 → Fun ( 𝐹 ↾ 𝐴 ) )
2 1 anim1i ⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( Fun ( 𝐹 ↾ 𝐴 ) ∧ 𝐴 ⊆ dom 𝐹 ) )
3 df-fn ⊢ ( ( 𝐹 ↾ 𝐴 ) Fn 𝐴 ↔ ( Fun ( 𝐹 ↾ 𝐴 ) ∧ dom ( 𝐹 ↾ 𝐴 ) = 𝐴 ) )
4 df-ima ⊢ ( 𝐹 “ 𝐴 ) = ran ( 𝐹 ↾ 𝐴 )
5 4 eqcomi ⊢ ran ( 𝐹 ↾ 𝐴 ) = ( 𝐹 “ 𝐴 )
6 df-fo ⊢ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ ( 𝐹 “ 𝐴 ) ↔ ( ( 𝐹 ↾ 𝐴 ) Fn 𝐴 ∧ ran ( 𝐹 ↾ 𝐴 ) = ( 𝐹 “ 𝐴 ) ) )
7 5 6 mpbiran2 ⊢ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ ( 𝐹 “ 𝐴 ) ↔ ( 𝐹 ↾ 𝐴 ) Fn 𝐴 )
8 ssdmres ⊢ ( 𝐴 ⊆ dom 𝐹 ↔ dom ( 𝐹 ↾ 𝐴 ) = 𝐴 )
9 8 anbi2i ⊢ ( ( Fun ( 𝐹 ↾ 𝐴 ) ∧ 𝐴 ⊆ dom 𝐹 ) ↔ ( Fun ( 𝐹 ↾ 𝐴 ) ∧ dom ( 𝐹 ↾ 𝐴 ) = 𝐴 ) )
10 3 7 9 3bitr4i ⊢ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ ( 𝐹 “ 𝐴 ) ↔ ( Fun ( 𝐹 ↾ 𝐴 ) ∧ 𝐴 ⊆ dom 𝐹 ) )
11 2 10 sylibr ⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( 𝐹 ↾ 𝐴 ) : 𝐴 –onto→ ( 𝐹 “ 𝐴 ) )