Metamath Proof Explorer

Theorem aceq0

Description: Equivalence of two versions of the Axiom of Choice. The proof uses neither AC nor the Axiom of Regularity. The right-hand side is our original ax-ac . (Contributed by NM, 5-Apr-2004)

Ref Expression
Assertion aceq0 
|- ( E. y A. z e. x A. w e. z E! v e. z E. u e. y ( z e. u /\ v e. u ) <-> E. y A. z A. w ( ( z e. w /\ w e. x ) -> E. v A. u ( E. t ( ( u e. w /\ w e. t ) /\ ( u e. t /\ t e. y ) ) <-> u = v ) ) )

Proof

Step Hyp Ref Expression
1 aceq1 
 |-  ( E. y A. z e. x A. w e. z E! v e. z E. u e. y ( z e. u /\ v e. u ) <-> E. y A. z A. w ( ( z e. w /\ w e. x ) -> E. x A. z ( E. x ( ( z e. w /\ w e. x ) /\ ( z e. x /\ x e. y ) ) <-> z = x ) ) )
2 equequ2 
 |-  ( v = x -> ( u = v <-> u = x ) )
3 2 bibi2d 
 |-  ( v = x -> ( ( E. t ( ( u e. w /\ w e. t ) /\ ( u e. t /\ t e. y ) ) <-> u = v ) <-> ( E. t ( ( u e. w /\ w e. t ) /\ ( u e. t /\ t e. y ) ) <-> u = x ) ) )
4 elequ2 
 |-  ( t = x -> ( w e. t <-> w e. x ) )
5 4 anbi2d 
 |-  ( t = x -> ( ( u e. w /\ w e. t ) <-> ( u e. w /\ w e. x ) ) )
6 elequ2 
 |-  ( t = x -> ( u e. t <-> u e. x ) )
7 elequ1 
 |-  ( t = x -> ( t e. y <-> x e. y ) )
8 6 7 anbi12d 
 |-  ( t = x -> ( ( u e. t /\ t e. y ) <-> ( u e. x /\ x e. y ) ) )
9 5 8 anbi12d 
 |-  ( t = x -> ( ( ( u e. w /\ w e. t ) /\ ( u e. t /\ t e. y ) ) <-> ( ( u e. w /\ w e. x ) /\ ( u e. x /\ x e. y ) ) ) )
10 9 cbvexvw 
 |-  ( E. t ( ( u e. w /\ w e. t ) /\ ( u e. t /\ t e. y ) ) <-> E. x ( ( u e. w /\ w e. x ) /\ ( u e. x /\ x e. y ) ) )
11 10 bibi1i 
 |-  ( ( E. t ( ( u e. w /\ w e. t ) /\ ( u e. t /\ t e. y ) ) <-> u = x ) <-> ( E. x ( ( u e. w /\ w e. x ) /\ ( u e. x /\ x e. y ) ) <-> u = x ) )
12 3 11 bitrdi 
 |-  ( v = x -> ( ( E. t ( ( u e. w /\ w e. t ) /\ ( u e. t /\ t e. y ) ) <-> u = v ) <-> ( E. x ( ( u e. w /\ w e. x ) /\ ( u e. x /\ x e. y ) ) <-> u = x ) ) )
13 12 albidv 
 |-  ( v = x -> ( A. u ( E. t ( ( u e. w /\ w e. t ) /\ ( u e. t /\ t e. y ) ) <-> u = v ) <-> A. u ( E. x ( ( u e. w /\ w e. x ) /\ ( u e. x /\ x e. y ) ) <-> u = x ) ) )
14 elequ1 
 |-  ( u = z -> ( u e. w <-> z e. w ) )
15 14 anbi1d 
 |-  ( u = z -> ( ( u e. w /\ w e. x ) <-> ( z e. w /\ w e. x ) ) )
16 elequ1 
 |-  ( u = z -> ( u e. x <-> z e. x ) )
17 16 anbi1d 
 |-  ( u = z -> ( ( u e. x /\ x e. y ) <-> ( z e. x /\ x e. y ) ) )
18 15 17 anbi12d 
 |-  ( u = z -> ( ( ( u e. w /\ w e. x ) /\ ( u e. x /\ x e. y ) ) <-> ( ( z e. w /\ w e. x ) /\ ( z e. x /\ x e. y ) ) ) )
19 18 exbidv 
 |-  ( u = z -> ( E. x ( ( u e. w /\ w e. x ) /\ ( u e. x /\ x e. y ) ) <-> E. x ( ( z e. w /\ w e. x ) /\ ( z e. x /\ x e. y ) ) ) )
20 equequ1 
 |-  ( u = z -> ( u = x <-> z = x ) )
21 19 20 bibi12d 
 |-  ( u = z -> ( ( E. x ( ( u e. w /\ w e. x ) /\ ( u e. x /\ x e. y ) ) <-> u = x ) <-> ( E. x ( ( z e. w /\ w e. x ) /\ ( z e. x /\ x e. y ) ) <-> z = x ) ) )
22 21 cbvalvw 
 |-  ( A. u ( E. x ( ( u e. w /\ w e. x ) /\ ( u e. x /\ x e. y ) ) <-> u = x ) <-> A. z ( E. x ( ( z e. w /\ w e. x ) /\ ( z e. x /\ x e. y ) ) <-> z = x ) )
23 13 22 bitrdi 
 |-  ( v = x -> ( A. u ( E. t ( ( u e. w /\ w e. t ) /\ ( u e. t /\ t e. y ) ) <-> u = v ) <-> A. z ( E. x ( ( z e. w /\ w e. x ) /\ ( z e. x /\ x e. y ) ) <-> z = x ) ) )
24 23 cbvexvw 
 |-  ( E. v A. u ( E. t ( ( u e. w /\ w e. t ) /\ ( u e. t /\ t e. y ) ) <-> u = v ) <-> E. x A. z ( E. x ( ( z e. w /\ w e. x ) /\ ( z e. x /\ x e. y ) ) <-> z = x ) )
25 24 imbi2i 
 |-  ( ( ( z e. w /\ w e. x ) -> E. v A. u ( E. t ( ( u e. w /\ w e. t ) /\ ( u e. t /\ t e. y ) ) <-> u = v ) ) <-> ( ( z e. w /\ w e. x ) -> E. x A. z ( E. x ( ( z e. w /\ w e. x ) /\ ( z e. x /\ x e. y ) ) <-> z = x ) ) )
26 25 2albii 
 |-  ( A. z A. w ( ( z e. w /\ w e. x ) -> E. v A. u ( E. t ( ( u e. w /\ w e. t ) /\ ( u e. t /\ t e. y ) ) <-> u = v ) ) <-> A. z A. w ( ( z e. w /\ w e. x ) -> E. x A. z ( E. x ( ( z e. w /\ w e. x ) /\ ( z e. x /\ x e. y ) ) <-> z = x ) ) )
27 26 exbii 
 |-  ( E. y A. z A. w ( ( z e. w /\ w e. x ) -> E. v A. u ( E. t ( ( u e. w /\ w e. t ) /\ ( u e. t /\ t e. y ) ) <-> u = v ) ) <-> E. y A. z A. w ( ( z e. w /\ w e. x ) -> E. x A. z ( E. x ( ( z e. w /\ w e. x ) /\ ( z e. x /\ x e. y ) ) <-> z = x ) ) )
28 1 27 bitr4i 
 |-  ( E. y A. z e. x A. w e. z E! v e. z E. u e. y ( z e. u /\ v e. u ) <-> E. y A. z A. w ( ( z e. w /\ w e. x ) -> E. v A. u ( E. t ( ( u e. w /\ w e. t ) /\ ( u e. t /\ t e. y ) ) <-> u = v ) ) )