Metamath Proof Explorer

Theorem aceq1

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

Ref Expression
Assertion 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 ) ) )

Proof

Step Hyp Ref Expression
1 biidd 
 |-  ( w = t -> ( E! v e. h E. u e. y ( h e. u /\ v e. u ) <-> E! v e. h E. u e. y ( h e. u /\ v e. u ) ) )
2 1 cbvralvw 
 |-  ( A. w e. h E! v e. h E. u e. y ( h e. u /\ v e. u ) <-> A. t e. h E! v e. h E. u e. y ( h e. u /\ v e. u ) )
3 elequ1 
 |-  ( v = z -> ( v e. u <-> z e. u ) )
4 3 anbi2d 
 |-  ( v = z -> ( ( h e. u /\ v e. u ) <-> ( h e. u /\ z e. u ) ) )
5 4 rexbidv 
 |-  ( v = z -> ( E. u e. y ( h e. u /\ v e. u ) <-> E. u e. y ( h e. u /\ z e. u ) ) )
6 5 cbvreuvw 
 |-  ( E! v e. h E. u e. y ( h e. u /\ v e. u ) <-> E! z e. h E. u e. y ( h e. u /\ z e. u ) )
7 6 ralbii 
 |-  ( A. t e. h E! v e. h E. u e. y ( h e. u /\ v e. u ) <-> A. t e. h E! z e. h E. u e. y ( h e. u /\ z e. u ) )
8 2 7 bitri 
 |-  ( A. w e. h E! v e. h E. u e. y ( h e. u /\ v e. u ) <-> A. t e. h E! z e. h E. u e. y ( h e. u /\ z e. u ) )
9 8 ralbii 
 |-  ( A. h e. x A. w e. h E! v e. h E. u e. y ( h e. u /\ v e. u ) <-> A. h e. x A. t e. h E! z e. h E. u e. y ( h e. u /\ z e. u ) )
10 elequ1 
 |-  ( z = h -> ( z e. u <-> h e. u ) )
11 10 anbi1d 
 |-  ( z = h -> ( ( z e. u /\ v e. u ) <-> ( h e. u /\ v e. u ) ) )
12 11 rexbidv 
 |-  ( z = h -> ( E. u e. y ( z e. u /\ v e. u ) <-> E. u e. y ( h e. u /\ v e. u ) ) )
13 12 reueqd 
 |-  ( z = h -> ( E! v e. z E. u e. y ( z e. u /\ v e. u ) <-> E! v e. h E. u e. y ( h e. u /\ v e. u ) ) )
14 13 raleqbi1dv 
 |-  ( z = h -> ( A. w e. z E! v e. z E. u e. y ( z e. u /\ v e. u ) <-> A. w e. h E! v e. h E. u e. y ( h e. u /\ v e. u ) ) )
15 14 cbvralvw 
 |-  ( A. z e. x A. w e. z E! v e. z E. u e. y ( z e. u /\ v e. u ) <-> A. h e. x A. w e. h E! v e. h E. u e. y ( h e. u /\ v e. u ) )
16 elequ1 
 |-  ( w = h -> ( w e. u <-> h e. u ) )
17 16 anbi1d 
 |-  ( w = h -> ( ( w e. u /\ z e. u ) <-> ( h e. u /\ z e. u ) ) )
18 17 rexbidv 
 |-  ( w = h -> ( E. u e. y ( w e. u /\ z e. u ) <-> E. u e. y ( h e. u /\ z e. u ) ) )
19 18 reueqd 
 |-  ( w = h -> ( E! z e. w E. u e. y ( w e. u /\ z e. u ) <-> E! z e. h E. u e. y ( h e. u /\ z e. u ) ) )
20 19 raleqbi1dv 
 |-  ( w = h -> ( A. t e. w E! z e. w E. u e. y ( w e. u /\ z e. u ) <-> A. t e. h E! z e. h E. u e. y ( h e. u /\ z e. u ) ) )
21 20 cbvralvw 
 |-  ( A. w e. x A. t e. w E! z e. w E. u e. y ( w e. u /\ z e. u ) <-> A. h e. x A. t e. h E! z e. h E. u e. y ( h e. u /\ z e. u ) )
22 9 15 21 3bitr4i 
 |-  ( A. z e. x A. w e. z E! v e. z E. u e. y ( z e. u /\ v e. u ) <-> A. w e. x A. t e. w E! z e. w E. u e. y ( w e. u /\ z e. u ) )
23 22 exbii 
 |-  ( 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. w e. x A. t e. w E! z e. w E. u e. y ( w e. u /\ z e. u ) )
24 19.21v 
 |-  ( A. z ( w e. x -> ( z e. w -> E. x A. z ( E. x ( ( z e. w /\ w e. x ) /\ ( z e. x /\ x e. y ) ) <-> z = x ) ) ) <-> ( w e. x -> A. z ( z e. w -> E. x A. z ( E. x ( ( z e. w /\ w e. x ) /\ ( z e. x /\ x e. y ) ) <-> z = x ) ) ) )
25 impexp 
 |-  ( ( ( 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 ) ) <-> ( 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 bi2.04 
 |-  ( ( 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 ) ) ) <-> ( w e. x -> ( z e. w -> E. x A. z ( E. x ( ( z e. w /\ w e. x ) /\ ( z e. x /\ x e. y ) ) <-> z = x ) ) ) )
27 25 26 bitri 
 |-  ( ( ( 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 ) ) <-> ( w e. x -> ( z e. w -> E. x A. z ( E. x ( ( z e. w /\ w e. x ) /\ ( z e. x /\ x e. y ) ) <-> z = x ) ) ) )
28 27 albii 
 |-  ( A. z ( ( 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 ) ) <-> A. z ( w e. x -> ( z e. w -> E. x A. z ( E. x ( ( z e. w /\ w e. x ) /\ ( z e. x /\ x e. y ) ) <-> z = x ) ) ) )
29 eu6 
 |-  ( E! z ( z e. w /\ E. u e. y ( w e. u /\ z e. u ) ) <-> E. x A. z ( ( z e. w /\ E. u e. y ( w e. u /\ z e. u ) ) <-> z = x ) )
30 df-reu 
 |-  ( E! z e. w E. u e. y ( w e. u /\ z e. u ) <-> E! z ( z e. w /\ E. u e. y ( w e. u /\ z e. u ) ) )
31 19.42v 
 |-  ( E. x ( z e. w /\ ( x e. y /\ ( w e. x /\ z e. x ) ) ) <-> ( z e. w /\ E. x ( x e. y /\ ( w e. x /\ z e. x ) ) ) )
32 an42 
 |-  ( ( ( z e. w /\ x e. y ) /\ ( w e. x /\ z e. x ) ) <-> ( ( z e. w /\ w e. x ) /\ ( z e. x /\ x e. y ) ) )
33 anass 
 |-  ( ( ( z e. w /\ x e. y ) /\ ( w e. x /\ z e. x ) ) <-> ( z e. w /\ ( x e. y /\ ( w e. x /\ z e. x ) ) ) )
34 32 33 bitr3i 
 |-  ( ( ( z e. w /\ w e. x ) /\ ( z e. x /\ x e. y ) ) <-> ( z e. w /\ ( x e. y /\ ( w e. x /\ z e. x ) ) ) )
35 34 exbii 
 |-  ( E. x ( ( z e. w /\ w e. x ) /\ ( z e. x /\ x e. y ) ) <-> E. x ( z e. w /\ ( x e. y /\ ( w e. x /\ z e. x ) ) ) )
36 df-rex 
 |-  ( E. u e. y ( w e. u /\ z e. u ) <-> E. u ( u e. y /\ ( w e. u /\ z e. u ) ) )
37 elequ1 
 |-  ( u = x -> ( u e. y <-> x e. y ) )
38 elequ2 
 |-  ( u = x -> ( w e. u <-> w e. x ) )
39 elequ2 
 |-  ( u = x -> ( z e. u <-> z e. x ) )
40 38 39 anbi12d 
 |-  ( u = x -> ( ( w e. u /\ z e. u ) <-> ( w e. x /\ z e. x ) ) )
41 37 40 anbi12d 
 |-  ( u = x -> ( ( u e. y /\ ( w e. u /\ z e. u ) ) <-> ( x e. y /\ ( w e. x /\ z e. x ) ) ) )
42 41 cbvexvw 
 |-  ( E. u ( u e. y /\ ( w e. u /\ z e. u ) ) <-> E. x ( x e. y /\ ( w e. x /\ z e. x ) ) )
43 36 42 bitri 
 |-  ( E. u e. y ( w e. u /\ z e. u ) <-> E. x ( x e. y /\ ( w e. x /\ z e. x ) ) )
44 43 anbi2i 
 |-  ( ( z e. w /\ E. u e. y ( w e. u /\ z e. u ) ) <-> ( z e. w /\ E. x ( x e. y /\ ( w e. x /\ z e. x ) ) ) )
45 31 35 44 3bitr4i 
 |-  ( E. x ( ( z e. w /\ w e. x ) /\ ( z e. x /\ x e. y ) ) <-> ( z e. w /\ E. u e. y ( w e. u /\ z e. u ) ) )
46 45 bibi1i 
 |-  ( ( E. x ( ( z e. w /\ w e. x ) /\ ( z e. x /\ x e. y ) ) <-> z = x ) <-> ( ( z e. w /\ E. u e. y ( w e. u /\ z e. u ) ) <-> z = x ) )
47 46 albii 
 |-  ( A. z ( E. x ( ( z e. w /\ w e. x ) /\ ( z e. x /\ x e. y ) ) <-> z = x ) <-> A. z ( ( z e. w /\ E. u e. y ( w e. u /\ z e. u ) ) <-> z = x ) )
48 47 exbii 
 |-  ( E. x A. z ( E. x ( ( z e. w /\ w e. x ) /\ ( z e. x /\ x e. y ) ) <-> z = x ) <-> E. x A. z ( ( z e. w /\ E. u e. y ( w e. u /\ z e. u ) ) <-> z = x ) )
49 29 30 48 3bitr4i 
 |-  ( E! z e. w E. u e. y ( w e. u /\ z e. u ) <-> E. x A. z ( E. x ( ( z e. w /\ w e. x ) /\ ( z e. x /\ x e. y ) ) <-> z = x ) )
50 49 imbi2i 
 |-  ( ( t e. w -> E! z e. w E. u e. y ( w e. u /\ z e. u ) ) <-> ( t e. w -> E. x A. z ( E. x ( ( z e. w /\ w e. x ) /\ ( z e. x /\ x e. y ) ) <-> z = x ) ) )
51 50 albii 
 |-  ( A. t ( t e. w -> E! z e. w E. u e. y ( w e. u /\ z e. u ) ) <-> A. t ( t e. w -> E. x A. z ( E. x ( ( z e. w /\ w e. x ) /\ ( z e. x /\ x e. y ) ) <-> z = x ) ) )
52 df-ral 
 |-  ( A. t e. w E! z e. w E. u e. y ( w e. u /\ z e. u ) <-> A. t ( t e. w -> E! z e. w E. u e. y ( w e. u /\ z e. u ) ) )
53 nfv 
 |-  F/ t ( z e. w -> E. x A. z ( E. x ( ( z e. w /\ w e. x ) /\ ( z e. x /\ x e. y ) ) <-> z = x ) )
54 nfv 
 |-  F/ z t e. w
55 nfa1 
 |-  F/ z A. z ( E. x ( ( z e. w /\ w e. x ) /\ ( z e. x /\ x e. y ) ) <-> z = x )
56 55 nfex 
 |-  F/ z E. x A. z ( E. x ( ( z e. w /\ w e. x ) /\ ( z e. x /\ x e. y ) ) <-> z = x )
57 54 56 nfim 
 |-  F/ z ( t e. w -> E. x A. z ( E. x ( ( z e. w /\ w e. x ) /\ ( z e. x /\ x e. y ) ) <-> z = x ) )
58 elequ1 
 |-  ( z = t -> ( z e. w <-> t e. w ) )
59 58 imbi1d 
 |-  ( z = t -> ( ( z e. w -> E. x A. z ( E. x ( ( z e. w /\ w e. x ) /\ ( z e. x /\ x e. y ) ) <-> z = x ) ) <-> ( t e. w -> E. x A. z ( E. x ( ( z e. w /\ w e. x ) /\ ( z e. x /\ x e. y ) ) <-> z = x ) ) ) )
60 53 57 59 cbvalv1 
 |-  ( A. z ( z e. w -> E. x A. z ( E. x ( ( z e. w /\ w e. x ) /\ ( z e. x /\ x e. y ) ) <-> z = x ) ) <-> A. t ( t e. w -> E. x A. z ( E. x ( ( z e. w /\ w e. x ) /\ ( z e. x /\ x e. y ) ) <-> z = x ) ) )
61 51 52 60 3bitr4i 
 |-  ( A. t e. w E! z e. w E. u e. y ( w e. u /\ z e. u ) <-> A. z ( z e. w -> E. x A. z ( E. x ( ( z e. w /\ w e. x ) /\ ( z e. x /\ x e. y ) ) <-> z = x ) ) )
62 61 imbi2i 
 |-  ( ( w e. x -> A. t e. w E! z e. w E. u e. y ( w e. u /\ z e. u ) ) <-> ( w e. x -> A. z ( z e. w -> E. x A. z ( E. x ( ( z e. w /\ w e. x ) /\ ( z e. x /\ x e. y ) ) <-> z = x ) ) ) )
63 24 28 62 3bitr4i 
 |-  ( A. z ( ( 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 ) ) <-> ( w e. x -> A. t e. w E! z e. w E. u e. y ( w e. u /\ z e. u ) ) )
64 63 albii 
 |-  ( A. w A. z ( ( 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 ) ) <-> A. w ( w e. x -> A. t e. w E! z e. w E. u e. y ( w e. u /\ z e. u ) ) )
65 alcom 
 |-  ( 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 ) ) <-> A. w A. z ( ( 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 ) ) )
66 df-ral 
 |-  ( A. w e. x A. t e. w E! z e. w E. u e. y ( w e. u /\ z e. u ) <-> A. w ( w e. x -> A. t e. w E! z e. w E. u e. y ( w e. u /\ z e. u ) ) )
67 64 65 66 3bitr4ri 
 |-  ( A. w e. x A. t e. w E! z e. w E. u e. y ( w e. u /\ z e. u ) <-> 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 ) ) )
68 67 exbii 
 |-  ( E. y A. w e. x A. t e. w E! z e. w E. u e. y ( w e. u /\ z 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 ) ) )
69 23 68 bitri 
 |-  ( 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 ) ) )