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

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 dfss2 
 |-  ( ( 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 eqtrid 
 |-  ( 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 ) )