Metamath Proof Explorer

Theorem funpartfun

Description: The functional part of F is a function. (Contributed by Scott Fenton, 16-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Assertion funpartfun 
|- Fun Funpart F

Proof

Step Hyp Ref Expression
1 relres 
 |-  Rel ( F |` dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) )
2 vex 
 |-  z e. _V
3 2 brresi 
 |-  ( x ( F |` dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) ) z <-> ( x e. dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) /\ x F z ) )
4 3 simprbi 
 |-  ( x ( F |` dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) ) z -> x F z )
5 vex 
 |-  y e. _V
6 5 brresi 
 |-  ( x ( F |` dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) ) y <-> ( x e. dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) /\ x F y ) )
7 funpartlem 
 |-  ( x e. dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) <-> E. w ( F " { x } ) = { w } )
8 7 anbi1i 
 |-  ( ( x e. dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) /\ x F y ) <-> ( E. w ( F " { x } ) = { w } /\ x F y ) )
9 6 8 bitri 
 |-  ( x ( F |` dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) ) y <-> ( E. w ( F " { x } ) = { w } /\ x F y ) )
10 df-br 
 |-  ( x F y <-> <. x , y >. e. F )
11 df-br 
 |-  ( x F z <-> <. x , z >. e. F )
12 10 11 anbi12i 
 |-  ( ( x F y /\ x F z ) <-> ( <. x , y >. e. F /\ <. x , z >. e. F ) )
13 vex 
 |-  x e. _V
14 13 5 elimasn 
 |-  ( y e. ( F " { x } ) <-> <. x , y >. e. F )
15 13 2 elimasn 
 |-  ( z e. ( F " { x } ) <-> <. x , z >. e. F )
16 14 15 anbi12i 
 |-  ( ( y e. ( F " { x } ) /\ z e. ( F " { x } ) ) <-> ( <. x , y >. e. F /\ <. x , z >. e. F ) )
17 12 16 bitr4i 
 |-  ( ( x F y /\ x F z ) <-> ( y e. ( F " { x } ) /\ z e. ( F " { x } ) ) )
18 eleq2 
 |-  ( ( F " { x } ) = { w } -> ( y e. ( F " { x } ) <-> y e. { w } ) )
19 eleq2 
 |-  ( ( F " { x } ) = { w } -> ( z e. ( F " { x } ) <-> z e. { w } ) )
20 18 19 anbi12d 
 |-  ( ( F " { x } ) = { w } -> ( ( y e. ( F " { x } ) /\ z e. ( F " { x } ) ) <-> ( y e. { w } /\ z e. { w } ) ) )
21 velsn 
 |-  ( y e. { w } <-> y = w )
22 velsn 
 |-  ( z e. { w } <-> z = w )
23 equtr2 
 |-  ( ( y = w /\ z = w ) -> y = z )
24 21 22 23 syl2anb 
 |-  ( ( y e. { w } /\ z e. { w } ) -> y = z )
25 20 24 syl6bi 
 |-  ( ( F " { x } ) = { w } -> ( ( y e. ( F " { x } ) /\ z e. ( F " { x } ) ) -> y = z ) )
26 17 25 syl5bi 
 |-  ( ( F " { x } ) = { w } -> ( ( x F y /\ x F z ) -> y = z ) )
27 26 exlimiv 
 |-  ( E. w ( F " { x } ) = { w } -> ( ( x F y /\ x F z ) -> y = z ) )
28 27 impl 
 |-  ( ( ( E. w ( F " { x } ) = { w } /\ x F y ) /\ x F z ) -> y = z )
29 9 28 sylanb 
 |-  ( ( x ( F |` dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) ) y /\ x F z ) -> y = z )
30 4 29 sylan2 
 |-  ( ( x ( F |` dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) ) y /\ x ( F |` dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) ) z ) -> y = z )
31 30 gen2 
 |-  A. y A. z ( ( x ( F |` dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) ) y /\ x ( F |` dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) ) z ) -> y = z )
32 31 ax-gen 
 |-  A. x A. y A. z ( ( x ( F |` dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) ) y /\ x ( F |` dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) ) z ) -> y = z )
33 df-funpart 
 |-  Funpart F = ( F |` dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) )
34 33 funeqi 
 |-  ( Fun Funpart F <-> Fun ( F |` dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) ) )
35 dffun2 
 |-  ( Fun ( F |` dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) ) <-> ( Rel ( F |` dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) ) /\ A. x A. y A. z ( ( x ( F |` dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) ) y /\ x ( F |` dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) ) z ) -> y = z ) ) )
36 34 35 bitri 
 |-  ( Fun Funpart F <-> ( Rel ( F |` dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) ) /\ A. x A. y A. z ( ( x ( F |` dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) ) y /\ x ( F |` dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) ) z ) -> y = z ) ) )
37 1 32 36 mpbir2an 
 |-  Fun Funpart F