Metamath Proof Explorer


Theorem fnresin

Description: Restriction of a function with a subclass of its domain. (Contributed by Thierry Arnoux, 10-Oct-2017)

Ref Expression
Assertion fnresin
|- ( F Fn A -> ( F |` B ) Fn ( A i^i B ) )

Proof

Step Hyp Ref Expression
1 fnresin1
 |-  ( F Fn A -> ( F |` ( A i^i B ) ) Fn ( A i^i B ) )
2 resindi
 |-  ( F |` ( A i^i B ) ) = ( ( F |` A ) i^i ( F |` B ) )
3 fnresdm
 |-  ( F Fn A -> ( F |` A ) = F )
4 3 ineq1d
 |-  ( F Fn A -> ( ( F |` A ) i^i ( F |` B ) ) = ( F i^i ( F |` B ) ) )
5 incom
 |-  ( ( F |` B ) i^i F ) = ( F i^i ( F |` B ) )
6 resss
 |-  ( F |` B ) C_ F
7 df-ss
 |-  ( ( F |` B ) C_ F <-> ( ( F |` B ) i^i F ) = ( F |` B ) )
8 6 7 mpbi
 |-  ( ( F |` B ) i^i F ) = ( F |` B )
9 5 8 eqtr3i
 |-  ( F i^i ( F |` B ) ) = ( F |` B )
10 4 9 eqtrdi
 |-  ( F Fn A -> ( ( F |` A ) i^i ( F |` B ) ) = ( F |` B ) )
11 2 10 syl5eq
 |-  ( F Fn A -> ( F |` ( A i^i B ) ) = ( F |` B ) )
12 11 fneq1d
 |-  ( F Fn A -> ( ( F |` ( A i^i B ) ) Fn ( A i^i B ) <-> ( F |` B ) Fn ( A i^i B ) ) )
13 1 12 mpbid
 |-  ( F Fn A -> ( F |` B ) Fn ( A i^i B ) )