MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  aceq1 Structured version   Visualization version   Unicode version

Theorem aceq1 8553
Description: Equivalence of two versions of the Axiom of Choice ax-ac 8894. 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.)
Assertion
Ref Expression
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 ) ) )
Distinct variable group:    x, y, z, w, v, u

Proof of Theorem aceq1
Dummy variables  t  h are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 biidd 241 . . . . . . 7  |-  ( 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
) ) )
21cbvralv 3021 . . . . . 6  |-  ( 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 eleq1 2519 . . . . . . . . . 10  |-  ( v  =  z  ->  (
v  e.  u  <->  z  e.  u ) )
43anbi2d 711 . . . . . . . . 9  |-  ( v  =  z  ->  (
( h  e.  u  /\  v  e.  u
)  <->  ( h  e.  u  /\  z  e.  u ) ) )
54rexbidv 2903 . . . . . . . 8  |-  ( v  =  z  ->  ( E. u  e.  y 
( h  e.  u  /\  v  e.  u
)  <->  E. u  e.  y  ( h  e.  u  /\  z  e.  u
) ) )
65cbvreuv 3023 . . . . . . 7  |-  ( 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 )
)
76ralbii 2821 . . . . . 6  |-  ( 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 )
)
82, 7bitri 253 . . . . 5  |-  ( 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 )
)
98ralbii 2821 . . . 4  |-  ( 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 eleq1 2519 . . . . . . . . 9  |-  ( z  =  h  ->  (
z  e.  u  <->  h  e.  u ) )
1110anbi1d 712 . . . . . . . 8  |-  ( z  =  h  ->  (
( z  e.  u  /\  v  e.  u
)  <->  ( h  e.  u  /\  v  e.  u ) ) )
1211rexbidv 2903 . . . . . . 7  |-  ( z  =  h  ->  ( E. u  e.  y 
( z  e.  u  /\  v  e.  u
)  <->  E. u  e.  y  ( h  e.  u  /\  v  e.  u
) ) )
1312reueqd 2999 . . . . . 6  |-  ( 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
) ) )
1413raleqbi1dv 2997 . . . . 5  |-  ( 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
) ) )
1514cbvralv 3021 . . . 4  |-  ( 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 eleq1 2519 . . . . . . . . 9  |-  ( w  =  h  ->  (
w  e.  u  <->  h  e.  u ) )
1716anbi1d 712 . . . . . . . 8  |-  ( w  =  h  ->  (
( w  e.  u  /\  z  e.  u
)  <->  ( h  e.  u  /\  z  e.  u ) ) )
1817rexbidv 2903 . . . . . . 7  |-  ( w  =  h  ->  ( E. u  e.  y 
( w  e.  u  /\  z  e.  u
)  <->  E. u  e.  y  ( h  e.  u  /\  z  e.  u
) ) )
1918reueqd 2999 . . . . . 6  |-  ( 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
) ) )
2019raleqbi1dv 2997 . . . . 5  |-  ( 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
) ) )
2120cbvralv 3021 . . . 4  |-  ( 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 )
)
229, 15, 213bitr4i 281 . . 3  |-  ( 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 )
)
2322exbii 1720 . 2  |-  ( 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 1788 . . . . . 6  |-  ( 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 448 . . . . . . . 8  |-  ( ( ( 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 363 . . . . . . . 8  |-  ( ( 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 ) ) ) )
2725, 26bitri 253 . . . . . . 7  |-  ( ( ( 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 ) ) ) )
2827albii 1693 . . . . . 6  |-  ( 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 df-eu 2305 . . . . . . . . . . 11  |-  ( 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 2746 . . . . . . . . . . 11  |-  ( 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 1836 . . . . . . . . . . . . . . 15  |-  ( 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 835 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 655 . . . . . . . . . . . . . . . . 17  |-  ( ( ( z  e.  w  /\  x  e.  y
)  /\  ( w  e.  x  /\  z  e.  x ) )  <->  ( z  e.  w  /\  (
x  e.  y  /\  ( w  e.  x  /\  z  e.  x
) ) ) )
3432, 33bitr3i 255 . . . . . . . . . . . . . . . 16  |-  ( ( ( z  e.  w  /\  w  e.  x
)  /\  ( z  e.  x  /\  x  e.  y ) )  <->  ( z  e.  w  /\  (
x  e.  y  /\  ( w  e.  x  /\  z  e.  x
) ) ) )
3534exbii 1720 . . . . . . . . . . . . . . 15  |-  ( 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 2745 . . . . . . . . . . . . . . . . 17  |-  ( E. u  e.  y  ( w  e.  u  /\  z  e.  u )  <->  E. u ( u  e.  y  /\  ( w  e.  u  /\  z  e.  u ) ) )
37 eleq1 2519 . . . . . . . . . . . . . . . . . . 19  |-  ( u  =  x  ->  (
u  e.  y  <->  x  e.  y ) )
38 eleq2 2520 . . . . . . . . . . . . . . . . . . . 20  |-  ( u  =  x  ->  (
w  e.  u  <->  w  e.  x ) )
39 eleq2 2520 . . . . . . . . . . . . . . . . . . . 20  |-  ( u  =  x  ->  (
z  e.  u  <->  z  e.  x ) )
4038, 39anbi12d 718 . . . . . . . . . . . . . . . . . . 19  |-  ( u  =  x  ->  (
( w  e.  u  /\  z  e.  u
)  <->  ( w  e.  x  /\  z  e.  x ) ) )
4137, 40anbi12d 718 . . . . . . . . . . . . . . . . . 18  |-  ( u  =  x  ->  (
( u  e.  y  /\  ( w  e.  u  /\  z  e.  u ) )  <->  ( x  e.  y  /\  (
w  e.  x  /\  z  e.  x )
) ) )
4241cbvexv 2119 . . . . . . . . . . . . . . . . 17  |-  ( E. u ( u  e.  y  /\  ( w  e.  u  /\  z  e.  u ) )  <->  E. x
( x  e.  y  /\  ( w  e.  x  /\  z  e.  x ) ) )
4336, 42bitri 253 . . . . . . . . . . . . . . . 16  |-  ( E. u  e.  y  ( w  e.  u  /\  z  e.  u )  <->  E. x ( x  e.  y  /\  ( w  e.  x  /\  z  e.  x ) ) )
4443anbi2i 701 . . . . . . . . . . . . . . 15  |-  ( ( 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 ) ) ) )
4531, 35, 443bitr4i 281 . . . . . . . . . . . . . 14  |-  ( 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 ) ) )
4645bibi1i 316 . . . . . . . . . . . . 13  |-  ( ( 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 ) )
4746albii 1693 . . . . . . . . . . . 12  |-  ( 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 ) )
4847exbii 1720 . . . . . . . . . . 11  |-  ( 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 ) )
4929, 30, 483bitr4i 281 . . . . . . . . . 10  |-  ( 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 ) )
5049imbi2i 314 . . . . . . . . 9  |-  ( ( 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 ) ) )
5150albii 1693 . . . . . . . 8  |-  ( 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 2744 . . . . . . . 8  |-  ( 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 1763 . . . . . . . . 9  |-  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 1763 . . . . . . . . . 10  |-  F/ z  t  e.  w
55 nfa1 1981 . . . . . . . . . . 11  |-  F/ z A. z ( E. x ( ( z  e.  w  /\  w  e.  x )  /\  (
z  e.  x  /\  x  e.  y )
)  <->  z  =  x )
5655nfex 2033 . . . . . . . . . 10  |-  F/ z E. x A. z
( E. x ( ( z  e.  w  /\  w  e.  x
)  /\  ( z  e.  x  /\  x  e.  y ) )  <->  z  =  x )
5754, 56nfim 2005 . . . . . . . . 9  |-  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 eleq1 2519 . . . . . . . . . 10  |-  ( z  =  t  ->  (
z  e.  w  <->  t  e.  w ) )
5958imbi1d 319 . . . . . . . . 9  |-  ( 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 ) ) ) )
6053, 57, 59cbval 2116 . . . . . . . 8  |-  ( 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 ) ) )
6151, 52, 603bitr4i 281 . . . . . . 7  |-  ( 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 ) ) )
6261imbi2i 314 . . . . . 6  |-  ( ( 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 ) ) ) )
6324, 28, 623bitr4i 281 . . . . 5  |-  ( 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 ) ) )
6463albii 1693 . . . 4  |-  ( 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 1925 . . . 4  |-  ( 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 2744 . . . 4  |-  ( 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 ) ) )
6764, 65, 663bitr4ri 282 . . 3  |-  ( 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 ) ) )
6867exbii 1720 . 2  |-  ( 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 ) ) )
6923, 68bitri 253 1  |-  ( 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 ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371   A.wal 1444   E.wex 1665   E!weu 2301   A.wral 2739   E.wrex 2740   E!wreu 2741
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ral 2744  df-rex 2745  df-reu 2746
This theorem is referenced by:  aceq0  8554  dfac1  8569
  Copyright terms: Public domain W3C validator