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 biimpri 
 |-  ( ( w ` z ) e. B -> A. y e. { z } ( w ` y ) e. B )
28 27 adantl 
 |-  ( ( w Fn { z } /\ ( w ` z ) e. B ) -> A. y e. { z } ( w ` y ) e. B )
29 ffnfv 
 |-  ( w : { z } --> B <-> ( w Fn { z } /\ A. y e. { z } ( w ` y ) e. B ) )
30 23 28 29 sylanbrc 
 |-  ( ( w Fn { z } /\ ( w ` z ) e. B ) -> w : { z } --> B )
31 18 fsn2 
 |-  ( w : { z } --> B <-> ( ( w ` z ) e. B /\ w = { <. z , ( w ` z ) >. } ) )
32 30 31 sylib 
 |-  ( ( w Fn { z } /\ ( w ` z ) e. B ) -> ( ( w ` z ) e. B /\ w = { <. z , ( w ` z ) >. } ) )
33 opeq2 
 |-  ( y = ( w ` z ) -> <. z , y >. = <. z , ( w ` z ) >. )
34 33 sneqd 
 |-  ( y = ( w ` z ) -> { <. z , y >. } = { <. z , ( w ` z ) >. } )
35 34 rspceeqv 
 |-  ( ( ( w ` z ) e. B /\ w = { <. z , ( w ` z ) >. } ) -> E. y e. B w = { <. z , y >. } )
36 32 35 syl 
 |-  ( ( w Fn { z } /\ ( w ` z ) e. B ) -> E. y e. B w = { <. z , y >. } )
37 vex 
 |-  y e. _V
38 18 37 fvsn 
 |-  ( { <. z , y >. } ` z ) = y
39 id 
 |-  ( y e. B -> y e. B )
40 38 39 eqeltrid 
 |-  ( y e. B -> ( { <. z , y >. } ` z ) e. B )
41 18 37 fnsn 
 |-  { <. z , y >. } Fn { z }
42 40 41 jctil 
 |-  ( y e. B -> ( { <. z , y >. } Fn { z } /\ ( { <. z , y >. } ` z ) e. B ) )
43 fneq1 
 |-  ( w = { <. z , y >. } -> ( w Fn { z } <-> { <. z , y >. } Fn { z } ) )
44 fveq1 
 |-  ( w = { <. z , y >. } -> ( w ` z ) = ( { <. z , y >. } ` z ) )
45 44 eleq1d 
 |-  ( w = { <. z , y >. } -> ( ( w ` z ) e. B <-> ( { <. z , y >. } ` z ) e. B ) )
46 43 45 anbi12d 
 |-  ( w = { <. z , y >. } -> ( ( w Fn { z } /\ ( w ` z ) e. B ) <-> ( { <. z , y >. } Fn { z } /\ ( { <. z , y >. } ` z ) e. B ) ) )
47 42 46 syl5ibrcom 
 |-  ( y e. B -> ( w = { <. z , y >. } -> ( w Fn { z } /\ ( w ` z ) e. B ) ) )
48 47 rexlimiv 
 |-  ( E. y e. B w = { <. z , y >. } -> ( w Fn { z } /\ ( w ` z ) e. B ) )
49 36 48 impbii 
 |-  ( ( w Fn { z } /\ ( w ` z ) e. B ) <-> E. y e. B w = { <. z , y >. } )
50 17 22 49 3bitri 
 |-  ( w e. X_ x e. { z } B <-> E. y e. B w = { <. z , y >. } )
51 13 15 50 vtoclbg 
 |-  ( F e. _V -> ( F e. X_ x e. { z } B <-> E. y e. B F = { <. z , y >. } ) )
52 8 12 51 pm5.21nii 
 |-  ( F e. X_ x e. { z } B <-> E. y e. B F = { <. z , y >. } )
53 3 7 52 vtoclbg 
 |-  ( A e. V -> ( F e. X_ x e. { A } B <-> E. y e. B F = { <. A , y >. } ) )