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