Metamath Proof Explorer

Theorem eqfnun

Description: Two functions on A u. B are equal if and only if they have equal restrictions to both A and B . (Contributed by Jeff Madsen, 19-Jun-2011)

Ref Expression
Assertion eqfnun 
|- ( ( F Fn ( A u. B ) /\ G Fn ( A u. B ) ) -> ( F = G <-> ( ( F |` A ) = ( G |` A ) /\ ( F |` B ) = ( G |` B ) ) ) )

Proof

Step Hyp Ref Expression
1 reseq1 
 |-  ( F = G -> ( F |` A ) = ( G |` A ) )
2 reseq1 
 |-  ( F = G -> ( F |` B ) = ( G |` B ) )
3 1 2 jca 
 |-  ( F = G -> ( ( F |` A ) = ( G |` A ) /\ ( F |` B ) = ( G |` B ) ) )
4 elun 
 |-  ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) )
5 fveq1 
 |-  ( ( F |` A ) = ( G |` A ) -> ( ( F |` A ) ` x ) = ( ( G |` A ) ` x ) )
6 fvres 
 |-  ( x e. A -> ( ( F |` A ) ` x ) = ( F ` x ) )
7 5 6 sylan9req 
 |-  ( ( ( F |` A ) = ( G |` A ) /\ x e. A ) -> ( ( G |` A ) ` x ) = ( F ` x ) )
8 fvres 
 |-  ( x e. A -> ( ( G |` A ) ` x ) = ( G ` x ) )
9 8 adantl 
 |-  ( ( ( F |` A ) = ( G |` A ) /\ x e. A ) -> ( ( G |` A ) ` x ) = ( G ` x ) )
10 7 9 eqtr3d 
 |-  ( ( ( F |` A ) = ( G |` A ) /\ x e. A ) -> ( F ` x ) = ( G ` x ) )
11 10 adantlr 
 |-  ( ( ( ( F |` A ) = ( G |` A ) /\ ( F |` B ) = ( G |` B ) ) /\ x e. A ) -> ( F ` x ) = ( G ` x ) )
12 fveq1 
 |-  ( ( F |` B ) = ( G |` B ) -> ( ( F |` B ) ` x ) = ( ( G |` B ) ` x ) )
13 fvres 
 |-  ( x e. B -> ( ( F |` B ) ` x ) = ( F ` x ) )
14 12 13 sylan9req 
 |-  ( ( ( F |` B ) = ( G |` B ) /\ x e. B ) -> ( ( G |` B ) ` x ) = ( F ` x ) )
15 fvres 
 |-  ( x e. B -> ( ( G |` B ) ` x ) = ( G ` x ) )
16 15 adantl 
 |-  ( ( ( F |` B ) = ( G |` B ) /\ x e. B ) -> ( ( G |` B ) ` x ) = ( G ` x ) )
17 14 16 eqtr3d 
 |-  ( ( ( F |` B ) = ( G |` B ) /\ x e. B ) -> ( F ` x ) = ( G ` x ) )
18 17 adantll 
 |-  ( ( ( ( F |` A ) = ( G |` A ) /\ ( F |` B ) = ( G |` B ) ) /\ x e. B ) -> ( F ` x ) = ( G ` x ) )
19 11 18 jaodan 
 |-  ( ( ( ( F |` A ) = ( G |` A ) /\ ( F |` B ) = ( G |` B ) ) /\ ( x e. A \/ x e. B ) ) -> ( F ` x ) = ( G ` x ) )
20 4 19 sylan2b 
 |-  ( ( ( ( F |` A ) = ( G |` A ) /\ ( F |` B ) = ( G |` B ) ) /\ x e. ( A u. B ) ) -> ( F ` x ) = ( G ` x ) )
21 20 ralrimiva 
 |-  ( ( ( F |` A ) = ( G |` A ) /\ ( F |` B ) = ( G |` B ) ) -> A. x e. ( A u. B ) ( F ` x ) = ( G ` x ) )
22 eqfnfv 
 |-  ( ( F Fn ( A u. B ) /\ G Fn ( A u. B ) ) -> ( F = G <-> A. x e. ( A u. B ) ( F ` x ) = ( G ` x ) ) )
23 21 22 syl5ibr 
 |-  ( ( F Fn ( A u. B ) /\ G Fn ( A u. B ) ) -> ( ( ( F |` A ) = ( G |` A ) /\ ( F |` B ) = ( G |` B ) ) -> F = G ) )
24 3 23 impbid2 
 |-  ( ( F Fn ( A u. B ) /\ G Fn ( A u. B ) ) -> ( F = G <-> ( ( F |` A ) = ( G |` A ) /\ ( F |` B ) = ( G |` B ) ) ) )