Theorem axacndlem4 4934

Description: Lemma for the Axiom of Choice with no distinct variable conditions.

Assertion

Ref	Expression
axacndlem4	|- E.xA.yA.z(A.x(y e. z /\ z e. w) -> E.wA.y(E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. x)) <-> y = w))

Distinct variable group:   y,z,w

Proof of Theorem axacndlem4

Step	Hyp	Ref	Expression
1		axac 4717	. . . . 5 |- E.vA.yA.z((y e. z /\ z e. w) -> E.wA.y(E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. v)) <-> y = w))
2		ax-4 970	. . . . . . . 8 |- (A.v(y e. z /\ z e. w) -> (y e. z /\ z e. w))
3	2	imim1i 16	. . . . . . 7 |- (((y e. z /\ z e. w) -> E.wA.y(E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. v)) <-> y = w)) -> (A.v(y e. z /\ z e. w) -> E.wA.y(E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. v)) <-> y = w)))
4	3	19.20i2 990	. . . . . 6 |- (A.yA.z((y e. z /\ z e. w) -> E.wA.y(E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. v)) <-> y = w)) -> A.yA.z(A.v(y e. z /\ z e. w) -> E.wA.y(E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. v)) <-> y = w)))
5	4	19.22i 1036	. . . . 5 |- (E.vA.yA.z((y e. z /\ z e. w) -> E.wA.y(E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. v)) <-> y = w)) -> E.vA.yA.z(A.v(y e. z /\ z e. w) -> E.wA.y(E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. v)) <-> y = w)))
6	1, 5	ax-mp 7	. . . 4 |- E.vA.yA.z(A.v(y e. z /\ z e. w) -> E.wA.y(E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. v)) <-> y = w))
7		hbnae 1143	. . . . . 6 |- (-. A.x x = z -> A.x -. A.x x = z)
8		hbnae 1143	. . . . . . 7 |- (-. A.x x = y -> A.x -. A.x x = y)
9		hbnae 1143	. . . . . . 7 |- (-. A.x x = w -> A.x -. A.x x = w)
10	8, 9	hban 1006	. . . . . 6 |- ((-. A.x x = y /\ -. A.x x = w) -> A.x(-. A.x x = y /\ -. A.x x = w))
11	7, 10	hban 1006	. . . . 5 |- ((-. A.x x = z /\ (-. A.x x = y /\ -. A.x x = w)) -> A.x(-. A.x x = z /\ (-. A.x x = y /\ -. A.x x = w)))
12		hbnae 1143	. . . . . . 7 |- (-. A.x x = z -> A.y -. A.x x = z)
13		hbnae 1143	. . . . . . . 8 |- (-. A.x x = y -> A.y -. A.x x = y)
14		hbnae 1143	. . . . . . . 8 |- (-. A.x x = w -> A.y -. A.x x = w)
15	13, 14	hban 1006	. . . . . . 7 |- ((-. A.x x = y /\ -. A.x x = w) -> A.y(-. A.x x = y /\ -. A.x x = w))
16	12, 15	hban 1006	. . . . . 6 |- ((-. A.x x = z /\ (-. A.x x = y /\ -. A.x x = w)) -> A.y(-. A.x x = z /\ (-. A.x x = y /\ -. A.x x = w)))
17		hbnae 1143	. . . . . . . 8 |- (-. A.x x = z -> A.z -. A.x x = z)
18		hbnae 1143	. . . . . . . . 9 |- (-. A.x x = y -> A.z -. A.x x = y)
19		hbnae 1143	. . . . . . . . 9 |- (-. A.x x = w -> A.z -. A.x x = w)
20	18, 19	hban 1006	. . . . . . . 8 |- ((-. A.x x = y /\ -. A.x x = w) -> A.z(-. A.x x = y /\ -. A.x x = w))
21	17, 20	hban 1006	. . . . . . 7 |- ((-. A.x x = z /\ (-. A.x x = y /\ -. A.x x = w)) -> A.z(-. A.x x = z /\ (-. A.x x = y /\ -. A.x x = w)))
22		ax-17 968	. . . . . . . . 9 |- ((-. A.x x = z /\ (-. A.x x = y /\ -. A.x x = w)) -> A.v(-. A.x x = z /\ (-. A.x x = y /\ -. A.x x = w)))
23		ax-15 1353	. . . . . . . . . . . 12 |- (-. A.x x = y -> (-. A.x x = z -> (y e. z -> A.x y e. z)))
24	23	impcom 351	. . . . . . . . . . 11 |- ((-. A.x x = z /\ -. A.x x = y) -> (y e. z -> A.x y e. z))
25	24	adantrr 395	. . . . . . . . . 10 |- ((-. A.x x = z /\ (-. A.x x = y /\ -. A.x x = w)) -> (y e. z -> A.x y e. z))
26		ax-15 1353	. . . . . . . . . . . 12 |- (-. A.x x = z -> (-. A.x x = w -> (z e. w -> A.x z e. w)))
27	26	imp 350	. . . . . . . . . . 11 |- ((-. A.x x = z /\ -. A.x x = w) -> (z e. w -> A.x z e. w))
28	27	adantrl 394	. . . . . . . . . 10 |- ((-. A.x x = z /\ (-. A.x x = y /\ -. A.x x = w)) -> (z e. w -> A.x z e. w))
29	25, 28	hband 1107	. . . . . . . . 9 |- ((-. A.x x = z /\ (-. A.x x = y /\ -. A.x x = w)) -> ((y e. z /\ z e. w) -> A.x(y e. z /\ z e. w)))
30	22, 29	hbald 1109	. . . . . . . 8 |- ((-. A.x x = z /\ (-. A.x x = y /\ -. A.x x = w)) -> (A.v(y e. z /\ z e. w) -> A.xA.v(y e. z /\ z e. w)))
31		hbnae 1143	. . . . . . . . . 10 |- (-. A.x x = z -> A.w -. A.x x = z)
32		hbnae 1143	. . . . . . . . . . 11 |- (-. A.x x = y -> A.w -. A.x x = y)
33		hbnae 1143	. . . . . . . . . . 11 |- (-. A.x x = w -> A.w -. A.x x = w)
34	32, 33	hban 1006	. . . . . . . . . 10 |- ((-. A.x x = y /\ -. A.x x = w) -> A.w(-. A.x x = y /\ -. A.x x = w))
35	31, 34	hban 1006	. . . . . . . . 9 |- ((-. A.x x = z /\ (-. A.x x = y /\ -. A.x x = w)) -> A.w(-. A.x x = z /\ (-. A.x x = y /\ -. A.x x = w)))
36		ax-15 1353	. . . . . . . . . . . . . . . 16 |- (-. A.x x = y -> (-. A.x x = w -> (y e. w -> A.x y e. w)))
37	36	imp 350	. . . . . . . . . . . . . . 15 |- ((-. A.x x = y /\ -. A.x x = w) -> (y e. w -> A.x y e. w))
38		dveel1 1349	. . . . . . . . . . . . . . . 16 |- (-. A.x x = w -> (w e. v -> A.x w e. v))
39	38	adantl 388	. . . . . . . . . . . . . . 15 |- ((-. A.x x = y /\ -. A.x x = w) -> (w e. v -> A.x w e. v))
40	37, 39	hband 1107	. . . . . . . . . . . . . 14 |- ((-. A.x x = y /\ -. A.x x = w) -> ((y e. w /\ w e. v) -> A.x(y e. w /\ w e. v)))
41	40	adantl 388	. . . . . . . . . . . . 13 |- ((-. A.x x = z /\ (-. A.x x = y /\ -. A.x x = w)) -> ((y e. w /\ w e. v) -> A.x(y e. w /\ w e. v)))
42	29, 41	hband 1107	. . . . . . . . . . . 12 |- ((-. A.x x = z /\ (-. A.x x = y /\ -. A.x x = w)) -> (((y e. z /\ z e. w) /\ (y e. w /\ w e. v)) -> A.x((y e. z /\ z e. w) /\ (y e. w /\ w e. v))))
43	35, 42	hbexd 1110	. . . . . . . . . . 11 |- ((-. A.x x = z /\ (-. A.x x = y /\ -. A.x x = w)) -> (E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. v)) -> A.xE.w((y e. z /\ z e. w) /\ (y e. w /\ w e. v))))
44		ax-12 965	. . . . . . . . . . . . 13 |- (-. A.x x = y -> (-. A.x x = w -> (y = w -> A.x y = w)))
45	44	imp 350	. . . . . . . . . . . 12 |- ((-. A.x x = y /\ -. A.x x = w) -> (y = w -> A.x y = w))
46	45	adantl 388	. . . . . . . . . . 11 |- ((-. A.x x = z /\ (-. A.x x = y /\ -. A.x x = w)) -> (y = w -> A.x y = w))
47	11, 43, 46	hbbid 1108	. . . . . . . . . 10 |- ((-. A.x x = z /\ (-. A.x x = y /\ -. A.x x = w)) -> ((E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. v)) <-> y = w) -> A.x(E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. v)) <-> y = w)))
48	16, 47	hbald 1109	. . . . . . . . 9 |- ((-. A.x x = z /\ (-. A.x x = y /\ -. A.x x = w)) -> (A.y(E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. v)) <-> y = w) -> A.x