MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-ac2 Structured version   Unicode version

Axiom ax-ac2 8895
Description: In order to avoid uses of ax-reg 8111 for derivation of AC equivalents, we provide ax-ac2 8895, which is equivalent to the standard AC of textbooks. This appears to be the shortest known equivalent to the standard AC when expressed in terms of set theory primitives. It was found by Kurt Maes as theorem ackm 8897. We removed the leading quantifier to make it slightly shorter, since we have ax-gen 1666 available. The derivation of ax-ac2 8895 from ax-ac 8891 is shown by theorem axac2 8898, and the reverse derivation by axac 8899. Note that we use ax-reg 8111 to derive ax-ac 8891 from ax-ac2 8895, but not to derive ax-ac2 8895 from ax-ac 8891. (Contributed by NM, 19-Dec-2016.)
Assertion
Ref Expression
ax-ac2  |-  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 ) ) ) ) )
Distinct variable group:    x, y, z, v, u

Detailed syntax breakdown of Axiom ax-ac2
StepHypRef Expression
1 vy . . . . . . . 8  setvar  y
2 vx . . . . . . . 8  setvar  x
31, 2wel 1870 . . . . . . 7  wff  y  e.  x
4 vz . . . . . . . . 9  setvar  z
54, 1wel 1870 . . . . . . . 8  wff  z  e.  y
6 vv . . . . . . . . . . 11  setvar  v
76, 2wel 1870 . . . . . . . . . 10  wff  v  e.  x
81, 6weq 1781 . . . . . . . . . . 11  wff  y  =  v
98wn 3 . . . . . . . . . 10  wff  -.  y  =  v
107, 9wa 371 . . . . . . . . 9  wff  ( v  e.  x  /\  -.  y  =  v )
114, 6wel 1870 . . . . . . . . 9  wff  z  e.  v
1210, 11wa 371 . . . . . . . 8  wff  ( ( v  e.  x  /\  -.  y  =  v
)  /\  z  e.  v )
135, 12wi 4 . . . . . . 7  wff  ( z  e.  y  ->  (
( v  e.  x  /\  -.  y  =  v )  /\  z  e.  v ) )
143, 13wa 371 . . . . . 6  wff  ( y  e.  x  /\  (
z  e.  y  -> 
( ( v  e.  x  /\  -.  y  =  v )  /\  z  e.  v )
) )
153wn 3 . . . . . . 7  wff  -.  y  e.  x
164, 2wel 1870 . . . . . . . 8  wff  z  e.  x
176, 4wel 1870 . . . . . . . . . 10  wff  v  e.  z
186, 1wel 1870 . . . . . . . . . 10  wff  v  e.  y
1917, 18wa 371 . . . . . . . . 9  wff  ( v  e.  z  /\  v  e.  y )
20 vu . . . . . . . . . . . 12  setvar  u
2120, 4wel 1870 . . . . . . . . . . 11  wff  u  e.  z
2220, 1wel 1870 . . . . . . . . . . 11  wff  u  e.  y
2321, 22wa 371 . . . . . . . . . 10  wff  ( u  e.  z  /\  u  e.  y )
2420, 6weq 1781 . . . . . . . . . 10  wff  u  =  v
2523, 24wi 4 . . . . . . . . 9  wff  ( ( u  e.  z  /\  u  e.  y )  ->  u  =  v )
2619, 25wa 371 . . . . . . . 8  wff  ( ( v  e.  z  /\  v  e.  y )  /\  ( ( u  e.  z  /\  u  e.  y )  ->  u  =  v ) )
2716, 26wi 4 . . . . . . 7  wff  ( z  e.  x  ->  (
( v  e.  z  /\  v  e.  y )  /\  ( ( u  e.  z  /\  u  e.  y )  ->  u  =  v ) ) )
2815, 27wa 371 . . . . . 6  wff  ( -.  y  e.  x  /\  ( z  e.  x  ->  ( ( v  e.  z  /\  v  e.  y )  /\  (
( u  e.  z  /\  u  e.  y )  ->  u  =  v ) ) ) )
2914, 28wo 370 . . . . 5  wff  ( ( 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 ) ) ) ) )
3029, 20wal 1436 . . . 4  wff  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 ) ) ) ) )
3130, 6wex 1660 . . 3  wff  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 ) ) ) ) )
3231, 4wal 1436 . 2  wff  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 ) ) ) ) )
3332, 1wex 1660 1  wff  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 ) ) ) ) )
Colors of variables: wff setvar class
This axiom is referenced by:  axac3  8896
  Copyright terms: Public domain W3C validator