Step |
Hyp |
Ref |
Expression |
1 |
|
dfac3 |
|- ( CHOICE <-> A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) |
2 |
|
fveq1 |
|- ( f = y -> ( f ` z ) = ( y ` z ) ) |
3 |
2
|
eleq1d |
|- ( f = y -> ( ( f ` z ) e. z <-> ( y ` z ) e. z ) ) |
4 |
3
|
imbi2d |
|- ( f = y -> ( ( z =/= (/) -> ( f ` z ) e. z ) <-> ( z =/= (/) -> ( y ` z ) e. z ) ) ) |
5 |
4
|
ralbidv |
|- ( f = y -> ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) <-> A. z e. x ( z =/= (/) -> ( y ` z ) e. z ) ) ) |
6 |
5
|
cbvexvw |
|- ( E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) <-> E. y A. z e. x ( z =/= (/) -> ( y ` z ) e. z ) ) |
7 |
|
fvex |
|- ( y ` w ) e. _V |
8 |
|
eqid |
|- ( w e. x |-> ( y ` w ) ) = ( w e. x |-> ( y ` w ) ) |
9 |
7 8
|
fnmpti |
|- ( w e. x |-> ( y ` w ) ) Fn x |
10 |
|
fveq2 |
|- ( w = z -> ( y ` w ) = ( y ` z ) ) |
11 |
|
fvex |
|- ( y ` z ) e. _V |
12 |
10 8 11
|
fvmpt |
|- ( z e. x -> ( ( w e. x |-> ( y ` w ) ) ` z ) = ( y ` z ) ) |
13 |
12
|
eleq1d |
|- ( z e. x -> ( ( ( w e. x |-> ( y ` w ) ) ` z ) e. z <-> ( y ` z ) e. z ) ) |
14 |
13
|
imbi2d |
|- ( z e. x -> ( ( z =/= (/) -> ( ( w e. x |-> ( y ` w ) ) ` z ) e. z ) <-> ( z =/= (/) -> ( y ` z ) e. z ) ) ) |
15 |
14
|
ralbiia |
|- ( A. z e. x ( z =/= (/) -> ( ( w e. x |-> ( y ` w ) ) ` z ) e. z ) <-> A. z e. x ( z =/= (/) -> ( y ` z ) e. z ) ) |
16 |
15
|
anbi2i |
|- ( ( ( w e. x |-> ( y ` w ) ) Fn x /\ A. z e. x ( z =/= (/) -> ( ( w e. x |-> ( y ` w ) ) ` z ) e. z ) ) <-> ( ( w e. x |-> ( y ` w ) ) Fn x /\ A. z e. x ( z =/= (/) -> ( y ` z ) e. z ) ) ) |
17 |
9 16
|
mpbiran |
|- ( ( ( w e. x |-> ( y ` w ) ) Fn x /\ A. z e. x ( z =/= (/) -> ( ( w e. x |-> ( y ` w ) ) ` z ) e. z ) ) <-> A. z e. x ( z =/= (/) -> ( y ` z ) e. z ) ) |
18 |
|
fvrn0 |
|- ( y ` w ) e. ( ran y u. { (/) } ) |
19 |
18
|
rgenw |
|- A. w e. x ( y ` w ) e. ( ran y u. { (/) } ) |
20 |
8
|
fmpt |
|- ( A. w e. x ( y ` w ) e. ( ran y u. { (/) } ) <-> ( w e. x |-> ( y ` w ) ) : x --> ( ran y u. { (/) } ) ) |
21 |
19 20
|
mpbi |
|- ( w e. x |-> ( y ` w ) ) : x --> ( ran y u. { (/) } ) |
22 |
|
vex |
|- x e. _V |
23 |
|
vex |
|- y e. _V |
24 |
23
|
rnex |
|- ran y e. _V |
25 |
|
p0ex |
|- { (/) } e. _V |
26 |
24 25
|
unex |
|- ( ran y u. { (/) } ) e. _V |
27 |
|
fex2 |
|- ( ( ( w e. x |-> ( y ` w ) ) : x --> ( ran y u. { (/) } ) /\ x e. _V /\ ( ran y u. { (/) } ) e. _V ) -> ( w e. x |-> ( y ` w ) ) e. _V ) |
28 |
21 22 26 27
|
mp3an |
|- ( w e. x |-> ( y ` w ) ) e. _V |
29 |
|
fneq1 |
|- ( f = ( w e. x |-> ( y ` w ) ) -> ( f Fn x <-> ( w e. x |-> ( y ` w ) ) Fn x ) ) |
30 |
|
fveq1 |
|- ( f = ( w e. x |-> ( y ` w ) ) -> ( f ` z ) = ( ( w e. x |-> ( y ` w ) ) ` z ) ) |
31 |
30
|
eleq1d |
|- ( f = ( w e. x |-> ( y ` w ) ) -> ( ( f ` z ) e. z <-> ( ( w e. x |-> ( y ` w ) ) ` z ) e. z ) ) |
32 |
31
|
imbi2d |
|- ( f = ( w e. x |-> ( y ` w ) ) -> ( ( z =/= (/) -> ( f ` z ) e. z ) <-> ( z =/= (/) -> ( ( w e. x |-> ( y ` w ) ) ` z ) e. z ) ) ) |
33 |
32
|
ralbidv |
|- ( f = ( w e. x |-> ( y ` w ) ) -> ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) <-> A. z e. x ( z =/= (/) -> ( ( w e. x |-> ( y ` w ) ) ` z ) e. z ) ) ) |
34 |
29 33
|
anbi12d |
|- ( f = ( w e. x |-> ( y ` w ) ) -> ( ( f Fn x /\ A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) <-> ( ( w e. x |-> ( y ` w ) ) Fn x /\ A. z e. x ( z =/= (/) -> ( ( w e. x |-> ( y ` w ) ) ` z ) e. z ) ) ) ) |
35 |
28 34
|
spcev |
|- ( ( ( w e. x |-> ( y ` w ) ) Fn x /\ A. z e. x ( z =/= (/) -> ( ( w e. x |-> ( y ` w ) ) ` z ) e. z ) ) -> E. f ( f Fn x /\ A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) ) |
36 |
17 35
|
sylbir |
|- ( A. z e. x ( z =/= (/) -> ( y ` z ) e. z ) -> E. f ( f Fn x /\ A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) ) |
37 |
36
|
exlimiv |
|- ( E. y A. z e. x ( z =/= (/) -> ( y ` z ) e. z ) -> E. f ( f Fn x /\ A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) ) |
38 |
6 37
|
sylbi |
|- ( E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> E. f ( f Fn x /\ A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) ) |
39 |
|
exsimpr |
|- ( E. f ( f Fn x /\ A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) -> E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) |
40 |
38 39
|
impbii |
|- ( E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) <-> E. f ( f Fn x /\ A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) ) |
41 |
40
|
albii |
|- ( A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) <-> A. x E. f ( f Fn x /\ A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) ) |
42 |
1 41
|
bitri |
|- ( CHOICE <-> A. x E. f ( f Fn x /\ A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) ) |