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

Axiom ax-ac2 8343
Description: In order to avoid uses of ax-reg 7560 for derivation of AC equivalents, we provide ax-ac2 8343, 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 8345. We removed the leading quantifier to make it slightly shorter, since we have ax-gen 1555 available. The derivation of ax-ac2 8343 from ax-ac 8339 is shown by theorem axac2 8346, and the reverse derivation by axac 8347. Note that we use ax-reg 7560 to derive ax-ac 8339 from ax-ac2 8343, but not to derive ax-ac2 8343 from ax-ac 8339. (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  set  y
2 vx . . . . . . . 8  set  x
31, 2wel 1726 . . . . . . 7  wff  y  e.  x
4 vz . . . . . . . . 9  set  z
54, 1wel 1726 . . . . . . . 8  wff  z  e.  y
6 vv . . . . . . . . . . 11  set  v
76, 2wel 1726 . . . . . . . . . 10  wff  v  e.  x
81, 6weq 1653 . . . . . . . . . . 11  wff  y  =  v
98wn 3 . . . . . . . . . 10  wff  -.  y  =  v
107, 9wa 359 . . . . . . . . 9  wff  ( v  e.  x  /\  -.  y  =  v )
114, 6wel 1726 . . . . . . . . 9  wff  z  e.  v
1210, 11wa 359 . . . . . . . 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 359 . . . . . 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 1726 . . . . . . . 8  wff  z  e.  x
176, 4wel 1726 . . . . . . . . . 10  wff  v  e.  z
186, 1wel 1726 . . . . . . . . . 10  wff  v  e.  y
1917, 18wa 359 . . . . . . . . 9  wff  ( v  e.  z  /\  v  e.  y )
20 vu . . . . . . . . . . . 12  set  u
2120, 4wel 1726 . . . . . . . . . . 11  wff  u  e.  z
2220, 1wel 1726 . . . . . . . . . . 11  wff  u  e.  y
2321, 22wa 359 . . . . . . . . . 10  wff  ( u  e.  z  /\  u  e.  y )
2420, 6weq 1653 . . . . . . . . . 10  wff  u  =  v
2523, 24wi 4 . . . . . . . . 9  wff  ( ( u  e.  z  /\  u  e.  y )  ->  u  =  v )
2619, 25wa 359 . . . . . . . 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 359 . . . . . 6  wff  ( -.  y  e.  x  /\  ( z  e.  x  ->  ( ( v  e.  z  /\  v  e.  y )  /\  (
( u  e.  z  /\  u  e.  y )  ->  u  =  v ) ) ) )
2914, 28wo 358 . . . . 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 1549 . . . 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 1550 . . 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 1549 . 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 1550 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 set class
This axiom is referenced by:  axac3  8344
  Copyright terms: Public domain W3C validator