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

Axiom ax-ac2 7973
Description: In order to avoid uses of ax-reg 7190 for derivation of AC equivalents, we provide ax-ac2 7973, 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 7976. We removed the leading quantifier to make it slightly shorter, since we have ax-gen 1536 available. The derivation of ax-ac2 7973 from ax-ac 7969 is shown by theorem axac2 7977, and the reverse derivation by axac 7978. Note that we use ax-reg 7190 to derive ax-ac 7969 from ax-ac2 7973, but not to derive ax-ac2 7973 from ax-ac 7969. (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 1622 . . . . . . 7  wff  y  e.  x
4 vz . . . . . . . . 9  set  z
54, 1wel 1622 . . . . . . . 8  wff  z  e.  y
6 vv . . . . . . . . . . 11  set  v
76, 2wel 1622 . . . . . . . . . 10  wff  v  e.  x
81, 6weq 1620 . . . . . . . . . . 11  wff  y  =  v
98wn 5 . . . . . . . . . 10  wff  -.  y  =  v
107, 9wa 360 . . . . . . . . 9  wff  ( v  e.  x  /\  -.  y  =  v )
114, 6wel 1622 . . . . . . . . 9  wff  z  e.  v
1210, 11wa 360 . . . . . . . 8  wff  ( ( v  e.  x  /\  -.  y  =  v
)  /\  z  e.  v )
135, 12wi 6 . . . . . . 7  wff  ( z  e.  y  ->  (
( v  e.  x  /\  -.  y  =  v )  /\  z  e.  v ) )
143, 13wa 360 . . . . . 6  wff  ( y  e.  x  /\  (
z  e.  y  -> 
( ( v  e.  x  /\  -.  y  =  v )  /\  z  e.  v )
) )
153wn 5 . . . . . . 7  wff  -.  y  e.  x
164, 2wel 1622 . . . . . . . 8  wff  z  e.  x
176, 4wel 1622 . . . . . . . . . 10  wff  v  e.  z
186, 1wel 1622 . . . . . . . . . 10  wff  v  e.  y
1917, 18wa 360 . . . . . . . . 9  wff  ( v  e.  z  /\  v  e.  y )
20 vu . . . . . . . . . . . 12  set  u
2120, 4wel 1622 . . . . . . . . . . 11  wff  u  e.  z
2220, 1wel 1622 . . . . . . . . . . 11  wff  u  e.  y
2321, 22wa 360 . . . . . . . . . 10  wff  ( u  e.  z  /\  u  e.  y )
2420, 6weq 1620 . . . . . . . . . 10  wff  u  =  v
2523, 24wi 6 . . . . . . . . 9  wff  ( ( u  e.  z  /\  u  e.  y )  ->  u  =  v )
2619, 25wa 360 . . . . . . . 8  wff  ( ( v  e.  z  /\  v  e.  y )  /\  ( ( u  e.  z  /\  u  e.  y )  ->  u  =  v ) )
2716, 26wi 6 . . . . . . 7  wff  ( z  e.  x  ->  (
( v  e.  z  /\  v  e.  y )  /\  ( ( u  e.  z  /\  u  e.  y )  ->  u  =  v ) ) )
2815, 27wa 360 . . . . . 6  wff  ( -.  y  e.  x  /\  ( z  e.  x  ->  ( ( v  e.  z  /\  v  e.  y )  /\  (
( u  e.  z  /\  u  e.  y )  ->  u  =  v ) ) ) )
2914, 28wo 359 . . . . 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 1532 . . . 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 1537 . . 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 1532 . 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 1537 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  7974
  Copyright terms: Public domain W3C validator