Theorem axpowndlem2 3744

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

Assertion

Ref	Expression
axpowndlem2	|- (-. A.x x = y -> (-. A.x x = z -> (-. x = y -> E.xA.y(A.x(E.z x e. y -> A.y x e. z) -> y e. x))))

Distinct variable group(s):   y,z

Proof of Theorem axpowndlem2

Step	Hyp	Ref	Expression
1		axpow 1082	. . . . . . 7 |- E.wA.y(A.w(w e. y -> w e. z) -> y e. w)
2		19.8a 712	. . . . . . . . . . . 12 |- (w e. y -> E.z w e. y)
3		ax-4 673	. . . . . . . . . . . 12 |- (A.y w e. z -> w e. z)
4	2, 3	syl34 20	. . . . . . . . . . 11 |- ((E.z w e. y -> A.y w e. z) -> (w e. y -> w e. z))
5	4	19.20i 691	. . . . . . . . . 10 |- (A.w(E.z w e. y -> A.y w e. z) -> A.w(w e. y -> w e. z))
6	5	syl4 19	. . . . . . . . 9 |- ((A.w(w e. y -> w e. z) -> y e. w) -> (A.w(E.z w e. y -> A.y w e. z) -> y e. w))
7	6	19.20i 691	. . . . . . . 8 |- (A.y(A.w(w e. y -> w e. z) -> y e. w) -> A.y(A.w(E.z w e. y -> A.y w e. z) -> y e. w))
8	7	19.22i 723	. . . . . . 7 |- (E.wA.y(A.w(w e. y -> w e. z) -> y e. w) -> E.wA.y(A.w(E.z w e. y -> A.y w e. z) -> y e. w))
9	1, 8	ax-mp 6	. . . . . 6 |- E.wA.y(A.w(E.z w e. y -> A.y w e. z) -> y e. w)
10	9	a1i 7	. . . . 5 |- (-. w = y -> E.wA.y(A.w(E.z w e. y -> A.y w e. z) -> y e. w))
11	10	ax-gen 677	. . . 4 |- A.w(-. w = y -> E.wA.y(A.w(E.z w e. y -> A.y w e. z) -> y e. w))
12		eq6 826	. . . . . 6 |- (-. A.x x = y -> A.x -. A.x x = y)
13		eq6 826	. . . . . 6 |- (-. A.x x = z -> A.x -. A.x x = z)
14	12, 13	hban 704	. . . . 5 |- ((-. A.x x = y /\ -. A.x x = z) -> A.x(-. A.x x = y /\ -. A.x x = z))
15		ddeeq2 1002	. . . . . . . 8 |- (-. A.x x = y -> (w = y -> A.x w = y))
16	12, 15	hbnd 786	. . . . . . 7 |- (-. A.x x = y -> (-. w = y -> A.x -. w = y))
17	16	adantr 306	. . . . . 6 |- ((-. A.x x = y /\ -. A.x x = z) -> (-. w = y -> A.x -. w = y))
18		ax-17 925	. . . . . . 7 |- ((-. A.x x = y /\ -. A.x x = z) -> A.w(-. A.x x = y /\ -. A.x x = z))
19		eq6 826	. . . . . . . . 9 |- (-. A.x x = y -> A.y -. A.x x = y)
20		eq6 826	. . . . . . . . 9 |- (-. A.x x = z -> A.y -. A.x x = z)
21	19, 20	hban 704	. . . . . . . 8 |- ((-. A.x x = y /\ -. A.x x = z) -> A.y(-. A.x x = y /\ -. A.x x = z))
22		eq6 826	. . . . . . . . . . 11 |- (-. A.x x = y -> A.w -. A.x x = y)
23		eq6 826	. . . . . . . . . . 11 |- (-. A.x x = z -> A.w -. A.x x = z)
24	22, 23	hban 704	. . . . . . . . . 10 |- ((-. A.x x = y /\ -. A.x x = z) -> A.w(-. A.x x = y /\ -. A.x x = z))
25		eq6 826	. . . . . . . . . . . . 13 |- (-. A.x x = y -> A.z -. A.x x = y)
26		eq6 826	. . . . . . . . . . . . 13 |- (-. A.x x = z -> A.z -. A.x x = z)
27	25, 26	hban 704	. . . . . . . . . . . 12 |- ((-. A.x x = y /\ -. A.x x = z) -> A.z(-. A.x x = y /\ -. A.x x = z))
28		ddeel2 1004	. . . . . . . . . . . . 13 |- (-. A.x x = y -> (w e. y -> A.x w e. y))
29	28	adantr 306	. . . . . . . . . . . 12 |- ((-. A.x x = y /\ -. A.x x = z) -> (w e. y -> A.x w e. y))
30	27, 29	hbexd 791	. . . . . . . . . . 11 |- ((-. A.x x = y /\ -. A.x x = z) -> (E.z w e. y -> A.xE.z w e. y))
31		ddeel2 1004	. . . . . . . . . . . . 13 |- (-. A.x x = z -> (w e. z -> A.x w e. z))
32	31	adantl 305	. . . . . . . . . . . 12 |- ((-. A.x x = y /\ -. A.x x = z) -> (w e. z -> A.x w e. z))
33	21, 32	hbald 790	. . . . . . . . . . 11 |- ((-. A.x x = y /\ -. A.x x = z) -> (A.y w e. z -> A.xA.y w e. z))
34	14, 30, 33	hbimd 787	. . . . . . . . . 10 |- ((-. A.x x = y /\ -. A.x x = z) -> ((E.z w e. y -> A.y w e. z) -> A.x(E.z w e. y -> A.y w e. z)))
35	24, 34	hbald 790	. . . . . . . . 9 |- ((-. A.x x = y /\ -. A.x x = z) -> (A.w(E.z w e. y -> A.y w e. z) -> A.xA.w(E.z w e. y -> A.y w e. z)))
36		ddeel1 1003	. . . . . . . . . 10 |- (-. A.x x = y -> (y e. w -> A.x y e. w))
37	36	adantr 306	. . . . . . . . 9 |- ((-. A.x x = y /\ -. A.x x = z) -> (y e. w -> A.x y e. w))
38	14, 35, 37	hbimd 787	. . . . . . . 8 |- ((-. A.x x = y /\ -. A.x x = z) -> ((A.w(E.z w e. y -> A.y w e. z) -> y e. w) -> A.x(A.w(E.z w e. y -> A.y w e. z) -> y e. w)))
39	21, 38	hbald 790	. . . . . . 7 |- ((-. A.x x = y /\ -. A.x x = z) -> (A.y(A.w(E.z w e. y -> A.y w e. z) -> y e. w) -> A.xA.y(A.w(E.z w e. y -> A.y w e. z) -> y e. w)))
40	18, 39	hbexd 791	. . . . . 6 |- ((-. A.x x = y /\ -. A.x x = z) -> (E.wA.y(A.w(E.z w e. y -> A.y w e. z) -> y e. w) -> A.xE.wA.y(A.w(E.z w e. y -> A.y w e. z) -> y e. w)))
41	14, 17, 40	hbimd 787	. . . . 5 |- ((-. A.x x = y /\ -. A.x x = z) -> ((-. w = y -> E.wA.y(A.w(E.z w e. y -> A.y w e. z) -> y e. w)) -> A.x(-. w = y -> E.wA.y(A.w(E.z w e. y -> A.y w e. z) -> y e. w))))
42		a8b 817	. . . . . . . . 9 |- (w = x -> (w = y <-> x = y))
43	42	negbid 463	. . . . . . . 8 |- (w = x -> (-. w = y <-> -. x = y))
44	43	adantl 305	. . . . . . 7 |- (((-. A.x x = y /\ -. A.x x = z) /\ w = x) -> (-. w = y <-> -. x = y))
45	18, 34	hbald 790	. . . . . . . . . . 11 |- ((-. A.x x = y /\ -. A.x x = z) -> (A.w(E.z w e. y -> A.y w e. z) -> A.xA.w(E.z w e. y -> A.y w e. z)))
46	14, 45, 37	hbimd 787	. . . . . . . . . 10 |- ((-. A.x x = y /\ -. A.x x = z) -> ((A.w(E.z w e. y -> A.y w e. z) -> y e. w) -> A.x(A.w(E.z w e. y -> A.y w e. z) -> y e. w)))
47	21, 46	hbald 790	. . . . . . . . 9 |- ((-. A.x x = y /\ -. A.x x = z) -> (A.y(A.w(E.z w e. y -> A.y w e. z) -> y e. w) -> A.xA.y(A.w(E.z w e. y -> A.y w e. z) -> y e. w)))
48		nd5 3736	. . . . . . . . . . . . 13 |- (-. A.x x = y -> (w = x -> A.y w = x))
49	48	adantr 306	. . . . . . . . . . . 12 |- ((-. A.x x = y /\ -. A.x x = z) -> (w = x -> A.y w = x))
50	49	imdistani 340	. . . . . . . . . . 11 |- (((-. A.x x = y /\ -. A.x x = z) /\ w = x) -> ((-. A.x x = y /\ -. A.x x = z) /\ A.y w = x))
51		hba1 698	. . . . . . . . . . . . 13 |- (A.y w = x -> A.yA.y w = x)
52	21, 51	hban 704	. . . . . . . . . . . 12 |- (((-. A.x x = y /\ -. A.x x = z) /\ A.y w = x) -> A.y((-. A.x x = y /\ -. A.x x = z) /\ A.y w = x))
53		nd5 3736	. . . . . . . . . . . . . . . . . . . 20 |- (-. A.x x = z -> (w = x -> A.z w = x))
54	53	imdistani 340	. . . . . . . . . . . . . . . . . . 19 |- ((-. A.x x = z /\ w = x) -> (-. A.x x = z /\ A.z w = x))
55		hba1 698	. . . . . . . . . . . . . . . . . . . . 21 |- (A.z w = x -> A.zA.z w = x)
56		a13b 819	. . . . . . . . . . . . . . . . . . . . . 22 |- (w = x -> (w e. y <-> x e. y))
57	56	a4s 682	. . . . . . . . . . . . . . . . . . . . 21 |- (A.z w = x -> (w e. y <-> x e. y))
58	55, 57	biexd 783	. . . . . . . . . . . . . . . . . . . 20 |- (A.z w = x -> (E.z w e. y <-> E.z x e. y))
59	58	adantl 305	. . . . . . . . . . . . . . . . . . 19 |- ((-. A.x x = z /\ A.z w = x) -> (E.z w e. y <-> E.z x e. y))
60	54, 59	syl 12	. . . . . . . . . . . . . . . . . 18 |- ((-. A.x x = z /\ w = x) -> (E.z w e. y <-> E.z x e. y))
61	60	adantll 309	. . . . . . . . . . . . . . . . 17 |- (((-. A.x x = y /\ -. A.x x = z) /\ w = x) -> (E.z w e. y <-> E.z x e. y))
62	48	imdistani 340	. . . . . . . . . . . . . . . . . . 19 |- (