Theorem axacndlem4 3756

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(s):   y,z,w

Proof of Theorem axacndlem4

Step	Hyp	Ref	Expression
1		axac 1085	. . . . 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 673	. . . . . . . . 9 |- (A.v(y e. z /\ z e. w) -> (y e. z /\ z e. w))
3	2	syl4 19	. . . . . . . 8 |- (((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.20i 691	. . . . . . 7 |- (A.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.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.20i 691	. . . . . 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)))
6	5	19.22i 723	. . . . 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)))
7	1, 6	ax-mp 6	. . . 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))
8		eq6 826	. . . . . 6 |- (-. A.x x = z -> A.x -. A.x x = z)
9		eq6 826	. . . . . . 7 |- (-. A.x x = y -> A.x -. A.x x = y)
10		eq6 826	. . . . . . 7 |- (-. A.x x = w -> A.x -. A.x x = w)
11	9, 10	hban 704	. . . . . 6 |- ((-. A.x x = y /\ -. A.x x = w) -> A.x(-. A.x x = y /\ -. A.x x = w))
12	8, 11	hban 704	. . . . 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)))
13		eq6 826	. . . . . . 7 |- (-. A.x x = z -> A.y -. A.x x = z)
14		eq6 826	. . . . . . . 8 |- (-. A.x x = y -> A.y -. A.x x = y)
15		eq6 826	. . . . . . . 8 |- (-. A.x x = w -> A.y -. A.x x = w)
16	14, 15	hban 704	. . . . . . 7 |- ((-. A.x x = y /\ -. A.x x = w) -> A.y(-. A.x x = y /\ -. A.x x = w))
17	13, 16	hban 704	. . . . . 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)))
18		eq6 826	. . . . . . . 8 |- (-. A.x x = z -> A.z -. A.x x = z)
19		eq6 826	. . . . . . . . 9 |- (-. A.x x = y -> A.z -. A.x x = y)
20		eq6 826	. . . . . . . . 9 |- (-. A.x x = w -> A.z -. A.x x = w)
21	19, 20	hban 704	. . . . . . . 8 |- ((-. A.x x = y /\ -. A.x x = w) -> A.z(-. A.x x = y /\ -. A.x x = w))
22	18, 21	hban 704	. . . . . . 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)))
23		ax-17 925	. . . . . . . . 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)))
24		ax15 1006	. . . . . . . . . . . . 13 |- (-. A.x x = y -> (-. A.x x = z -> (y e. z -> A.x y e. z)))
25	24	com12 13	. . . . . . . . . . . 12 |- (-. A.x x = z -> (-. A.x x = y -> (y e. z -> A.x y e. z)))
26	25	imp 277	. . . . . . . . . . 11 |- ((-. A.x x = z /\ -. A.x x = y) -> (y e. z -> A.x y e. z))
27	26	adantrr 312	. . . . . . . . . 10 |- ((-. A.x x = z /\ (-. A.x x = y /\ -. A.x x = w)) -> (y e. z -> A.x y e. z))
28		ax15 1006	. . . . . . . . . . . 12 |- (-. A.x x = z -> (-. A.x x = w -> (z e. w -> A.x z e. w)))
29	28	imp 277	. . . . . . . . . . 11 |- ((-. A.x x = z /\ -. A.x x = w) -> (z e. w -> A.x z e. w))
30	29	adantrl 311	. . . . . . . . . 10 |- ((-. A.x x = z /\ (-. A.x x = y /\ -. A.x x = w)) -> (z e. w -> A.x z e. w))
31	27, 30	hband 788	. . . . . . . . 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)))
32	23, 31	hbald 790	. . . . . . . 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)))
33		eq6 826	. . . . . . . . . 10 |- (-. A.x x = z -> A.w -. A.x x = z)
34		eq6 826	. . . . . . . . . . 11 |- (-. A.x x = y -> A.w -. A.x x = y)
35		eq6 826	. . . . . . . . . . 11 |- (-. A.x x = w -> A.w -. A.x x = w)
36	34, 35	hban 704	. . . . . . . . . 10 |- ((-. A.x x = y /\ -. A.x x = w) -> A.w(-. A.x x = y /\ -. A.x x = w))
37	33, 36	hban 704	. . . . . . . . 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)))
38		ax15 1006	. . . . . . . . . . . . . . . 16 |- (-. A.x x = y -> (-. A.x x = w -> (y e. w -> A.x y e. w)))
39	38	imp 277	. . . . . . . . . . . . . . 15 |- ((-. A.x x = y /\ -. A.x x = w) -> (y e. w -> A.x y e. w))
40		ddeel1 1003	. . . . . . . . . . . . . . . 16 |- (-. A.x x = w -> (w e. v -> A.x w e. v))
41	40	adantl 305	. . . . . . . . . . . . . . 15 |- ((-. A.x x = y /\ -. A.x x = w) -> (w e. v -> A.x w e. v))
42	39, 41	hband 788	. . . . . . . . . . . . . 14 |- ((-. A.x x = y /\ -. A.x x = w) -> ((y e. w /\ w e. v) -> A.x(y e. w /\ w e. v)))
43	42	adantl 305	. . . . . . . . . . . . 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)))
44	31, 43	hband 788	. . . . . . . . . . . 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))))
45	37, 44	hbexd 791	. . . . . . . . . . 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))))
46		ax-12 802	. . . . . . . . . . . . 13 |- (-. A.x x = y -> (-. A.x x = w -> (y = w -> A.x y = w)))
47	46	imp 277	. . . . . . . . . . . 12 |- ((-. A.x x = y /\ -. A.x x = w) -> (y = w -> A.x y = w))
48	47	adantl 305	. . . . . . . . . . 11 |- ((-. A.x x = z /\ (-. A.x x = y /\ -. A.x x = w)) -> (y = w -> A.x y = w))
49	12, 45, 48	hbbid 789	. . . . . . . . . 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)))
50	17, 49	hbald 790