Metamath Proof Explorer

Theorem dfackm

Description: Equivalence of the Axiom of Choice and Maes' AC ackm . The proof consists of lemmas kmlem1 through kmlem16 and this final theorem. AC is not used for the proof. Note: bypassing the first step (i.e., replacing dfac5 with biid ) establishes the AC equivalence shown by Maes' writeup. The left-hand-side AC shown here was chosen because it is shorter to display. (Contributed by NM, 13-Apr-2004) (Revised by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion dfackm 
|- ( CHOICE <-> A. x E. y A. z E. v A. u ( ( y e. x /\ ( z e. y -> ( ( v e. x /\ -. y = v ) /\ z e. v ) ) ) \/ ( -. y e. x /\ ( z e. x -> ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dfac5 
 |-  ( CHOICE <-> A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) )
2 eqid 
 |-  { t | E. h e. x t = ( h \ U. ( x \ { h } ) ) } = { t | E. h e. x t = ( h \ U. ( x \ { h } ) ) }
3 2 kmlem13 
 |-  ( A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) <-> A. x ( -. E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) )
4 kmlem8 
 |-  ( ( -. E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) <-> ( E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) \/ E. y ( -. y e. x /\ A. z e. x E! v v e. ( z i^i y ) ) ) )
5 4 albii 
 |-  ( A. x ( -. E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) <-> A. x ( E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) \/ E. y ( -. y e. x /\ A. z e. x E! v v e. ( z i^i y ) ) ) )
6 3 5 bitri 
 |-  ( A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) <-> A. x ( E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) \/ E. y ( -. y e. x /\ A. z e. x E! v v e. ( z i^i y ) ) ) )
7 df-ne 
 |-  ( y =/= v <-> -. y = v )
8 7 bicomi 
 |-  ( -. y = v <-> y =/= v )
9 8 anbi2i 
 |-  ( ( v e. x /\ -. y = v ) <-> ( v e. x /\ y =/= v ) )
10 9 anbi1i 
 |-  ( ( ( v e. x /\ -. y = v ) /\ z e. v ) <-> ( ( v e. x /\ y =/= v ) /\ z e. v ) )
11 10 imbi2i 
 |-  ( ( z e. y -> ( ( v e. x /\ -. y = v ) /\ z e. v ) ) <-> ( z e. y -> ( ( v e. x /\ y =/= v ) /\ z e. v ) ) )
12 biid 
 |-  ( ( z e. x -> ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) ) <-> ( z e. x -> ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) ) )
13 biid 
 |-  ( A. z e. x E! v v e. ( z i^i y ) <-> A. z e. x E! v v e. ( z i^i y ) )
14 11 12 13 kmlem16 
 |-  ( ( E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) \/ E. y ( -. y e. x /\ A. z e. x E! v v e. ( z i^i y ) ) ) <-> E. y A. z E. v A. u ( ( y e. x /\ ( z e. y -> ( ( v e. x /\ -. y = v ) /\ z e. v ) ) ) \/ ( -. y e. x /\ ( z e. x -> ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) ) ) ) )
15 14 albii 
 |-  ( A. x ( E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) \/ E. y ( -. y e. x /\ A. z e. x E! v v e. ( z i^i y ) ) ) <-> A. x E. y A. z E. v A. u ( ( y e. x /\ ( z e. y -> ( ( v e. x /\ -. y = v ) /\ z e. v ) ) ) \/ ( -. y e. x /\ ( z e. x -> ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) ) ) ) )
16 6 15 bitri 
 |-  ( A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) <-> A. x E. y A. z E. v A. u ( ( y e. x /\ ( z e. y -> ( ( v e. x /\ -. y = v ) /\ z e. v ) ) ) \/ ( -. y e. x /\ ( z e. x -> ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) ) ) ) )
17 1 16 bitri 
 |-  ( CHOICE <-> A. x E. y A. z E. v A. u ( ( y e. x /\ ( z e. y -> ( ( v e. x /\ -. y = v ) /\ z e. v ) ) ) \/ ( -. y e. x /\ ( z e. x -> ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) ) ) ) )