Metamath Proof Explorer

Theorem dfac4

Description: Equivalence of two versions of the Axiom of Choice. The right-hand side is Axiom AC of BellMachover p. 488. The proof does not depend on AC. (Contributed by NM, 24-Mar-2004) (Revised by Mario Carneiro, 26-Jun-2015)

Ref Expression
Assertion dfac4 
|- ( CHOICE <-> A. x E. f ( f Fn x /\ A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) )

Proof

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 ) ) )