Axiom ax-ac2 8299

Description: In order to avoid uses of ax-reg 7516 for derivation of AC equivalents, we provide ax-ac2 8299, 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 8301. We removed the leading quantifier to make it slightly shorter, since we have ax-gen 1552 available. The derivation of ax-ac2 8299 from ax-ac 8295 is shown by theorem axac2 8302, and the reverse derivation by axac 8303. Note that we use ax-reg 7516 to derive ax-ac 8295 from ax-ac2 8299, but not to derive ax-ac2 8299 from ax-ac 8295. (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

Step	Hyp	Ref	Expression
1		vy	. . . . . . . 8 set y
2		vx	. . . . . . . 8 set x
3	1, 2	wel 1722	. . . . . . 7 wff y e. x
4		vz	. . . . . . . . 9 set z
5	4, 1	wel 1722	. . . . . . . 8 wff z e. y
6		vv	. . . . . . . . . . 11 set v
7	6, 2	wel 1722	. . . . . . . . . 10 wff v e. x
8	1, 6	weq 1650	. . . . . . . . . . 11 wff y = v
9	8	wn 3	. . . . . . . . . 10 wff -. y = v
10	7, 9	wa 359	. . . . . . . . 9 wff ( v e. x /\ -. y = v )
11	4, 6	wel 1722	. . . . . . . . 9 wff z e. v
12	10, 11	wa 359	. . . . . . . 8 wff ( ( v e. x /\ -. y = v ) /\ z e. v )
13	5, 12	wi 4	. . . . . . 7 wff ( z e. y -> ( ( v e. x /\ -. y = v ) /\ z e. v ) )
14	3, 13	wa 359	. . . . . 6 wff ( y e. x /\ ( z e. y -> ( ( v e. x /\ -. y = v ) /\ z e. v ) ) )
15	3	wn 3	. . . . . . 7 wff -. y e. x
16	4, 2	wel 1722	. . . . . . . 8 wff z e. x
17	6, 4	wel 1722	. . . . . . . . . 10 wff v e. z
18	6, 1	wel 1722	. . . . . . . . . 10 wff v e. y
19	17, 18	wa 359	. . . . . . . . 9 wff ( v e. z /\ v e. y )
20		vu	. . . . . . . . . . . 12 set u
21	20, 4	wel 1722	. . . . . . . . . . 11 wff u e. z
22	20, 1	wel 1722	. . . . . . . . . . 11 wff u e. y
23	21, 22	wa 359	. . . . . . . . . 10 wff ( u e. z /\ u e. y )
24	20, 6	weq 1650	. . . . . . . . . 10 wff u = v
25	23, 24	wi 4	. . . . . . . . 9 wff ( ( u e. z /\ u e. y ) -> u = v )
26	19, 25	wa 359	. . . . . . . 8 wff ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) )
27	16, 26	wi 4	. . . . . . 7 wff ( z e. x -> ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) )
28	15, 27	wa 359	. . . . . 6 wff ( -. y e. x /\ ( z e. x -> ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) ) )
29	14, 28	wo 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 ) ) ) ) )
30	29, 20	wal 1546	. . . 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 ) ) ) ) )
31	30, 6	wex 1547	. . 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 ) ) ) ) )
32	31, 4	wal 1546	. 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 ) ) ) ) )
33	32, 1	wex 1547	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 ) ) ) ) )

This axiom is referenced by:  axac3  8300