Metamath Proof Explorer

Theorem funpartlem

Description: Lemma for funpartfun . Show membership in the restriction. (Contributed by Scott Fenton, 4-Dec-2017)

Ref Expression
Assertion funpartlem 
|- ( A e. dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) <-> E. x ( F " { A } ) = { x } )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) -> A e. _V )
2 vsnid 
 |-  x e. { x }
3 eleq2 
 |-  ( ( F " { A } ) = { x } -> ( x e. ( F " { A } ) <-> x e. { x } ) )
4 2 3 mpbiri 
 |-  ( ( F " { A } ) = { x } -> x e. ( F " { A } ) )
5 n0i 
 |-  ( x e. ( F " { A } ) -> -. ( F " { A } ) = (/) )
6 snprc 
 |-  ( -. A e. _V <-> { A } = (/) )
7 6 biimpi 
 |-  ( -. A e. _V -> { A } = (/) )
8 7 imaeq2d 
 |-  ( -. A e. _V -> ( F " { A } ) = ( F " (/) ) )
9 ima0 
 |-  ( F " (/) ) = (/)
10 8 9 eqtrdi 
 |-  ( -. A e. _V -> ( F " { A } ) = (/) )
11 5 10 nsyl2 
 |-  ( x e. ( F " { A } ) -> A e. _V )
12 4 11 syl 
 |-  ( ( F " { A } ) = { x } -> A e. _V )
13 12 exlimiv 
 |-  ( E. x ( F " { A } ) = { x } -> A e. _V )
14 eleq1 
 |-  ( y = A -> ( y e. dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) <-> A e. dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) ) )
15 sneq 
 |-  ( y = A -> { y } = { A } )
16 15 imaeq2d 
 |-  ( y = A -> ( F " { y } ) = ( F " { A } ) )
17 16 eqeq1d 
 |-  ( y = A -> ( ( F " { y } ) = { x } <-> ( F " { A } ) = { x } ) )
18 17 exbidv 
 |-  ( y = A -> ( E. x ( F " { y } ) = { x } <-> E. x ( F " { A } ) = { x } ) )
19 vex 
 |-  y e. _V
20 19 eldm 
 |-  ( y e. dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) <-> E. z y ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) z )
21 brxp 
 |-  ( y ( _V X. Singletons ) z <-> ( y e. _V /\ z e. Singletons ) )
22 19 21 mpbiran 
 |-  ( y ( _V X. Singletons ) z <-> z e. Singletons )
23 elsingles 
 |-  ( z e. Singletons <-> E. x z = { x } )
24 22 23 bitri 
 |-  ( y ( _V X. Singletons ) z <-> E. x z = { x } )
25 24 anbi2i 
 |-  ( ( y ( Image F o. Singleton ) z /\ y ( _V X. Singletons ) z ) <-> ( y ( Image F o. Singleton ) z /\ E. x z = { x } ) )
26 brin 
 |-  ( y ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) z <-> ( y ( Image F o. Singleton ) z /\ y ( _V X. Singletons ) z ) )
27 19.42v 
 |-  ( E. x ( y ( Image F o. Singleton ) z /\ z = { x } ) <-> ( y ( Image F o. Singleton ) z /\ E. x z = { x } ) )
28 25 26 27 3bitr4i 
 |-  ( y ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) z <-> E. x ( y ( Image F o. Singleton ) z /\ z = { x } ) )
29 28 exbii 
 |-  ( E. z y ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) z <-> E. z E. x ( y ( Image F o. Singleton ) z /\ z = { x } ) )
30 excom 
 |-  ( E. z E. x ( y ( Image F o. Singleton ) z /\ z = { x } ) <-> E. x E. z ( y ( Image F o. Singleton ) z /\ z = { x } ) )
31 29 30 bitri 
 |-  ( E. z y ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) z <-> E. x E. z ( y ( Image F o. Singleton ) z /\ z = { x } ) )
32 exancom 
 |-  ( E. z ( y ( Image F o. Singleton ) z /\ z = { x } ) <-> E. z ( z = { x } /\ y ( Image F o. Singleton ) z ) )
33 snex 
 |-  { x } e. _V
34 breq2 
 |-  ( z = { x } -> ( y ( Image F o. Singleton ) z <-> y ( Image F o. Singleton ) { x } ) )
35 33 34 ceqsexv 
 |-  ( E. z ( z = { x } /\ y ( Image F o. Singleton ) z ) <-> y ( Image F o. Singleton ) { x } )
36 19 33 brco 
 |-  ( y ( Image F o. Singleton ) { x } <-> E. z ( y Singleton z /\ z Image F { x } ) )
37 vex 
 |-  z e. _V
38 19 37 brsingle 
 |-  ( y Singleton z <-> z = { y } )
39 38 anbi1i 
 |-  ( ( y Singleton z /\ z Image F { x } ) <-> ( z = { y } /\ z Image F { x } ) )
40 39 exbii 
 |-  ( E. z ( y Singleton z /\ z Image F { x } ) <-> E. z ( z = { y } /\ z Image F { x } ) )
41 snex 
 |-  { y } e. _V
42 breq1 
 |-  ( z = { y } -> ( z Image F { x } <-> { y } Image F { x } ) )
43 41 42 ceqsexv 
 |-  ( E. z ( z = { y } /\ z Image F { x } ) <-> { y } Image F { x } )
44 41 33 brimage 
 |-  ( { y } Image F { x } <-> { x } = ( F " { y } ) )
45 eqcom 
 |-  ( { x } = ( F " { y } ) <-> ( F " { y } ) = { x } )
46 43 44 45 3bitri 
 |-  ( E. z ( z = { y } /\ z Image F { x } ) <-> ( F " { y } ) = { x } )
47 36 40 46 3bitri 
 |-  ( y ( Image F o. Singleton ) { x } <-> ( F " { y } ) = { x } )
48 32 35 47 3bitri 
 |-  ( E. z ( y ( Image F o. Singleton ) z /\ z = { x } ) <-> ( F " { y } ) = { x } )
49 48 exbii 
 |-  ( E. x E. z ( y ( Image F o. Singleton ) z /\ z = { x } ) <-> E. x ( F " { y } ) = { x } )
50 20 31 49 3bitri 
 |-  ( y e. dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) <-> E. x ( F " { y } ) = { x } )
51 14 18 50 vtoclbg 
 |-  ( A e. _V -> ( A e. dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) <-> E. x ( F " { A } ) = { x } ) )
52 1 13 51 pm5.21nii 
 |-  ( A e. dom ( ( Image F o. Singleton ) i^i ( _V X. Singletons ) ) <-> E. x ( F " { A } ) = { x } )