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

Metamath Proof Explorer

Theorem fnreseql

Description: Two functions are equal on a subset iff their equalizer contains that subset. (Contributed by Stefan O'Rear, 7-Mar-2015)

Ref Expression
Assertion fnreseql 
|- ( ( F Fn A /\ G Fn A /\ X C_ A ) -> ( ( F |` X ) = ( G |` X ) <-> X C_ dom ( F i^i G ) ) )

Proof

Step Hyp Ref Expression
1 fnssres 
 |-  ( ( F Fn A /\ X C_ A ) -> ( F |` X ) Fn X )
2 1 3adant2 
 |-  ( ( F Fn A /\ G Fn A /\ X C_ A ) -> ( F |` X ) Fn X )
3 fnssres 
 |-  ( ( G Fn A /\ X C_ A ) -> ( G |` X ) Fn X )
4 3 3adant1 
 |-  ( ( F Fn A /\ G Fn A /\ X C_ A ) -> ( G |` X ) Fn X )
5 fneqeql 
 |-  ( ( ( F |` X ) Fn X /\ ( G |` X ) Fn X ) -> ( ( F |` X ) = ( G |` X ) <-> dom ( ( F |` X ) i^i ( G |` X ) ) = X ) )
6 2 4 5 syl2anc 
 |-  ( ( F Fn A /\ G Fn A /\ X C_ A ) -> ( ( F |` X ) = ( G |` X ) <-> dom ( ( F |` X ) i^i ( G |` X ) ) = X ) )
7 resindir 
 |-  ( ( F i^i G ) |` X ) = ( ( F |` X ) i^i ( G |` X ) )
8 7 dmeqi 
 |-  dom ( ( F i^i G ) |` X ) = dom ( ( F |` X ) i^i ( G |` X ) )
9 dmres 
 |-  dom ( ( F i^i G ) |` X ) = ( X i^i dom ( F i^i G ) )
10 8 9 eqtr3i 
 |-  dom ( ( F |` X ) i^i ( G |` X ) ) = ( X i^i dom ( F i^i G ) )
11 10 eqeq1i 
 |-  ( dom ( ( F |` X ) i^i ( G |` X ) ) = X <-> ( X i^i dom ( F i^i G ) ) = X )
12 dfss2 
 |-  ( X C_ dom ( F i^i G ) <-> ( X i^i dom ( F i^i G ) ) = X )
13 11 12 bitr4i 
 |-  ( dom ( ( F |` X ) i^i ( G |` X ) ) = X <-> X C_ dom ( F i^i G ) )
14 6 13 bitrdi 
 |-  ( ( F Fn A /\ G Fn A /\ X C_ A ) -> ( ( F |` X ) = ( G |` X ) <-> X C_ dom ( F i^i G ) ) )