Metamath Proof Explorer

Theorem elixpsn

Description: Membership in a class of singleton functions. (Contributed by Stefan O'Rear, 24-Jan-2015)

Ref Expression
Assertion elixpsn 
|- ( A e. V -> ( F e. X_ x e. { A } B <-> E. y e. B F = { <. A , y >. } ) )

Proof

Step Hyp Ref Expression
1 sneq 
 |-  ( z = A -> { z } = { A } )
2 1 ixpeq1d 
 |-  ( z = A -> X_ x e. { z } B = X_ x e. { A } B )
3 2 eleq2d 
 |-  ( z = A -> ( F e. X_ x e. { z } B <-> F e. X_ x e. { A } B ) )
4 opeq1 
 |-  ( z = A -> <. z , y >. = <. A , y >. )
5 4 sneqd 
 |-  ( z = A -> { <. z , y >. } = { <. A , y >. } )
6 5 eqeq2d 
 |-  ( z = A -> ( F = { <. z , y >. } <-> F = { <. A , y >. } ) )
7 6 rexbidv 
 |-  ( z = A -> ( E. y e. B F = { <. z , y >. } <-> E. y e. B F = { <. A , y >. } ) )
8 elex 
 |-  ( F e. X_ x e. { z } B -> F e. _V )
9 snex 
 |-  { <. z , y >. } e. _V
10 eleq1 
 |-  ( F = { <. z , y >. } -> ( F e. _V <-> { <. z , y >. } e. _V ) )
11 9 10 mpbiri 
 |-  ( F = { <. z , y >. } -> F e. _V )
12 11 rexlimivw 
 |-  ( E. y e. B F = { <. z , y >. } -> F e. _V )
13 eleq1 
 |-  ( w = F -> ( w e. X_ x e. { z } B <-> F e. X_ x e. { z } B ) )
14 eqeq1 
 |-  ( w = F -> ( w = { <. z , y >. } <-> F = { <. z , y >. } ) )
15 14 rexbidv 
 |-  ( w = F -> ( E. y e. B w = { <. z , y >. } <-> E. y e. B F = { <. z , y >. } ) )
16 vex 
 |-  w e. _V
17 16 elixp 
 |-  ( w e. X_ x e. { z } B <-> ( w Fn { z } /\ A. x e. { z } ( w ` x ) e. B ) )
18 vex 
 |-  z e. _V
19 fveq2 
 |-  ( x = z -> ( w ` x ) = ( w ` z ) )
20 19 eleq1d 
 |-  ( x = z -> ( ( w ` x ) e. B <-> ( w ` z ) e. B ) )
21 18 20 ralsn 
 |-  ( A. x e. { z } ( w ` x ) e. B <-> ( w ` z ) e. B )
22 21 anbi2i 
 |-  ( ( w Fn { z } /\ A. x e. { z } ( w ` x ) e. B ) <-> ( w Fn { z } /\ ( w ` z ) e. B ) )
23 simpl 
 |-  ( ( w Fn { z } /\ ( w ` z ) e. B ) -> w Fn { z } )
24 fveq2 
 |-  ( y = z -> ( w ` y ) = ( w ` z ) )
25 24 eleq1d 
 |-  ( y = z -> ( ( w ` y ) e. B <-> ( w ` z ) e. B ) )
26 18 25 ralsn 
 |-  ( A. y e. { z } ( w ` y ) e. B <-> ( w ` z ) e. B )
27 26 bilanri 
 |-  ( ( w Fn { z } /\ ( w ` z ) e. B ) -> A. y e. { z } ( w ` y ) e. B )
28 ffnfv 
 |-  ( w : { z } --> B <-> ( w Fn { z } /\ A. y e. { z } ( w ` y ) e. B ) )
29 23 27 28 sylanbrc 
 |-  ( ( w Fn { z } /\ ( w ` z ) e. B ) -> w : { z } --> B )
30 18 fsn2 
 |-  ( w : { z } --> B <-> ( ( w ` z ) e. B /\ w = { <. z , ( w ` z ) >. } ) )
31 29 30 sylib 
 |-  ( ( w Fn { z } /\ ( w ` z ) e. B ) -> ( ( w ` z ) e. B /\ w = { <. z , ( w ` z ) >. } ) )
32 opeq2 
 |-  ( y = ( w ` z ) -> <. z , y >. = <. z , ( w ` z ) >. )
33 32 sneqd 
 |-  ( y = ( w ` z ) -> { <. z , y >. } = { <. z , ( w ` z ) >. } )
34 33 rspceeqv 
 |-  ( ( ( w ` z ) e. B /\ w = { <. z , ( w ` z ) >. } ) -> E. y e. B w = { <. z , y >. } )
35 31 34 syl 
 |-  ( ( w Fn { z } /\ ( w ` z ) e. B ) -> E. y e. B w = { <. z , y >. } )
36 vex 
 |-  y e. _V
37 18 36 fvsn 
 |-  ( { <. z , y >. } ` z ) = y
38 id 
 |-  ( y e. B -> y e. B )
39 37 38 eqeltrid 
 |-  ( y e. B -> ( { <. z , y >. } ` z ) e. B )
40 18 36 fnsn 
 |-  { <. z , y >. } Fn { z }
41 39 40 jctil 
 |-  ( y e. B -> ( { <. z , y >. } Fn { z } /\ ( { <. z , y >. } ` z ) e. B ) )
42 fneq1 
 |-  ( w = { <. z , y >. } -> ( w Fn { z } <-> { <. z , y >. } Fn { z } ) )
43 fveq1 
 |-  ( w = { <. z , y >. } -> ( w ` z ) = ( { <. z , y >. } ` z ) )
44 43 eleq1d 
 |-  ( w = { <. z , y >. } -> ( ( w ` z ) e. B <-> ( { <. z , y >. } ` z ) e. B ) )
45 42 44 anbi12d 
 |-  ( w = { <. z , y >. } -> ( ( w Fn { z } /\ ( w ` z ) e. B ) <-> ( { <. z , y >. } Fn { z } /\ ( { <. z , y >. } ` z ) e. B ) ) )
46 41 45 syl5ibrcom 
 |-  ( y e. B -> ( w = { <. z , y >. } -> ( w Fn { z } /\ ( w ` z ) e. B ) ) )
47 46 rexlimiv 
 |-  ( E. y e. B w = { <. z , y >. } -> ( w Fn { z } /\ ( w ` z ) e. B ) )
48 35 47 impbii 
 |-  ( ( w Fn { z } /\ ( w ` z ) e. B ) <-> E. y e. B w = { <. z , y >. } )
49 17 22 48 3bitri 
 |-  ( w e. X_ x e. { z } B <-> E. y e. B w = { <. z , y >. } )
50 13 15 49 vtoclbg 
 |-  ( F e. _V -> ( F e. X_ x e. { z } B <-> E. y e. B F = { <. z , y >. } ) )
51 8 12 50 pm5.21nii 
 |-  ( F e. X_ x e. { z } B <-> E. y e. B F = { <. z , y >. } )
52 3 7 51 vtoclbg 
 |-  ( A e. V -> ( F e. X_ x e. { A } B <-> E. y e. B F = { <. A , y >. } ) )