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

Axiom ax-ac2 8631
Description: In order to avoid uses of ax-reg 7806 for derivation of AC equivalents, we provide ax-ac2 8631, 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 8633. We removed the leading quantifier to make it slightly shorter, since we have ax-gen 1591 available. The derivation of ax-ac2 8631 from ax-ac 8627 is shown by theorem axac2 8634, and the reverse derivation by axac 8635. Note that we use ax-reg 7806 to derive ax-ac 8627 from ax-ac2 8631, but not to derive ax-ac2 8631 from ax-ac 8627. (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 1757 . . . . . . 7  wff  y  e.  x
4 vz . . . . . . . . 9  setvar  z
54, 1wel 1757 . . . . . . . 8  wff  z  e.  y
6 vv . . . . . . . . . . 11  setvar  v
76, 2wel 1757 . . . . . . . . . 10  wff  v  e.  x
81, 6weq 1695 . . . . . . . . . . 11  wff  y  =  v
98wn 3 . . . . . . . . . 10  wff  -.  y  =  v
107, 9wa 369 . . . . . . . . 9  wff  ( v  e.  x  /\  -.  y  =  v )
114, 6wel 1757 . . . . . . . . 9  wff  z  e.  v
1210, 11wa 369 . . . . . . . 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 369 . . . . . 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 1757 . . . . . . . 8  wff  z  e.  x
176, 4wel 1757 . . . . . . . . . 10  wff  v  e.  z
186, 1wel 1757 . . . . . . . . . 10  wff  v  e.  y
1917, 18wa 369 . . . . . . . . 9  wff  ( v  e.  z  /\  v  e.  y )
20 vu . . . . . . . . . . . 12  setvar  u
2120, 4wel 1757 . . . . . . . . . . 11  wff  u  e.  z
2220, 1wel 1757 . . . . . . . . . . 11  wff  u  e.  y
2321, 22wa 369 . . . . . . . . . 10  wff  ( u  e.  z  /\  u  e.  y )
2420, 6weq 1695 . . . . . . . . . 10  wff  u  =  v
2523, 24wi 4 . . . . . . . . 9  wff  ( ( u  e.  z  /\  u  e.  y )  ->  u  =  v )
2619, 25wa 369 . . . . . . . 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 369 . . . . . 6  wff  ( -.  y  e.  x  /\  ( z  e.  x  ->  ( ( v  e.  z  /\  v  e.  y )  /\  (
( u  e.  z  /\  u  e.  y )  ->  u  =  v ) ) ) )
2914, 28wo 368 . . . . 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 1367 . . . 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 1586 . . 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 1367 . 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 1586 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  8632
  Copyright terms: Public domain W3C validator