Theorem axpowndlem2 4937

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:   y,z

Proof of Theorem axpowndlem2

Step	Hyp	Ref	Expression
1		axpow 2740	. . . . . . 7 |- E.wA.y(A.w(w e. y -> w e. z) -> y e. w)
2		19.8a 1028	. . . . . . . . . . . 12 |- (w e. y -> E.z w e. y)
3		ax-4 972	. . . . . . . . . . . 12 |- (A.y w e. z -> w e. z)
4	2, 3	imim12i 18	. . . . . . . . . . 11 |- ((E.z w e. y -> A.y w e. z) -> (w e. y -> w e. z))
5	4	19.20i 991	. . . . . . . . . 10 |- (A.w(E.z w e. y -> A.y w e. z) -> A.w(w e. y -> w e. z))
6	5	imim1i 16	. . . . . . . . 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 991	. . . . . . . 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 1039	. . . . . . 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 7	. . . . . 6 |- E.wA.y(A.w(E.z w e. y -> A.y w e. z) -> y e. w)
10	9	a1i 8	. . . . 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 962	. . . 4 |- A.w(-. w = y -> E.wA.y(A.w(E.z w e. y -> A.y w e. z) -> y e. w))
12		hbnae 1146	. . . . . 6 |- (-. A.x x = y -> A.x -. A.x x = y)
13		hbnae 1146	. . . . . 6 |- (-. A.x x = z -> A.x -. A.x x = z)
14	12, 13	hban 1008	. . . . 5 |- ((-. A.x x = y /\ -. A.x x = z) -> A.x(-. A.x x = y /\ -. A.x x = z))
15		dveeq2 1212	. . . . . . . 8 |- (-. A.x x = y -> (w = y -> A.x w = y))
16	12, 15	hbnd 1108	. . . . . . 7 |- (-. A.x x = y -> (-. w = y -> A.x -. w = y))
17	16	adantr 389	. . . . . 6 |- ((-. A.x x = y /\ -. A.x x = z) -> (-. w = y -> A.x -. w = y))
18		ax-17 970	. . . . . . 7 |- ((-. A.x x = y /\ -. A.x x = z) -> A.w(-. A.x x = y /\ -. A.x x = z))
19		hbnae 1146	. . . . . . . . 9 |- (-. A.x x = y -> A.y -. A.x x = y)
20		hbnae 1146	. . . . . . . . 9 |- (-. A.x x = z -> A.y -. A.x x = z)
21	19, 20	hban 1008	. . . . . . . 8 |- ((-. A.x x = y /\ -. A.x x = z) -> A.y(-. A.x x = y /\ -. A.x x = z))
22		hbnae 1146	. . . . . . . . . . 11 |- (-. A.x x = y -> A.w -. A.x x = y)
23		hbnae 1146	. . . . . . . . . . 11 |- (-. A.x x = z -> A.w -. A.x x = z)
24	22, 23	hban 1008	. . . . . . . . . 10 |- ((-. A.x x = y /\ -. A.x x = z) -> A.w(-. A.x x = y /\ -. A.x x = z))
25		hbnae 1146	. . . . . . . . . . . . 13 |- (-. A.x x = y -> A.z -. A.x x = y)
26		hbnae 1146	. . . . . . . . . . . . 13 |- (-. A.x x = z -> A.z -. A.x x = z)
27	25, 26	hban 1008	. . . . . . . . . . . 12 |- ((-. A.x x = y /\ -. A.x x = z) -> A.z(-. A.x x = y /\ -. A.x x = z))
28		dveel2 1357	. . . . . . . . . . . . 13 |- (-. A.x x = y -> (w e. y -> A.x w e. y))
29	28	adantr 389	. . . . . . . . . . . 12 |- ((-. A.x x = y /\ -. A.x x = z) -> (w e. y -> A.x w e. y))
30	27, 29	hbexd 1113	. . . . . . . . . . 11 |- ((-. A.x x = y /\ -. A.x x = z) -> (E.z w e. y -> A.xE.z w e. y))
31		dveel2 1357	. . . . . . . . . . . . 13 |- (-. A.x x = z -> (w e. z -> A.x w e. z))
32	31	adantl 388	. . . . . . . . . . . 12 |- ((-. A.x x = y /\ -. A.x x = z) -> (w e. z -> A.x w e. z))
33	21, 32	hbald 1112	. . . . . . . . . . 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 1109	. . . . . . . . . 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 1112	. . . . . . . . 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		dveel1 1356	. . . . . . . . . 10 |- (-. A.x x = y -> (y e. w -> A.x y e. w))
37	36	adantr 389	. . . . . . . . 9 |- ((-. A.x x = y /\ -. A.x x = z) -> (y e. w -> A.x y e. w))
38	14, 35, 37	hbimd 1109	. . . . . . . 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 1112	. . . . . . 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 1113	. . . . . 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 1109	. . . . 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		equequ1 1133	. . . . . . . . 9 |- (w = x -> (w = y <-> x = y))
43	42	negbid 610	. . . . . . . 8 |- (w = x -> (-. w = y <-> -. x = y))
44	43	adantl 388	. . . . . . 7 |- (((-. A.x x = y /\ -. A.x x = z) /\ w = x) -> (-. w = y <-> -. x = y))
45	18, 34	hbald 1112	. . . . . . . . . . 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 1109	. . . . . . . . . 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 1112	. . . . . . . . 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 4929	. . . . . . . . . . . . 13 |- (-. A.x x = y -> (w = x -> A.y w = x))
49	48	adantr 389	. . . . . . . . . . . 12 |- ((-. A.x x = y /\ -. A.x x = z) -> (w = x -> A.y w = x))
50	49	imdistani 443	. . . . . . . . . . 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 1002	. . . . . . . . . . . . 13 |- (A.y w = x -> A.yA.y w = x)
52	21, 51	hban 1008	. . . . . . . . . . . 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 4929	. . . . . . . . . . . . . . . . . . . 20 |- (-. A.x x = z -> (w = x -> A.z w = x))
54	53	imdistani 443	. . . . . . . . . . . . . . . . . . 19 |- ((-. A.x x = z /\ w = x) -> (-. A.x x = z /\ A.z w = x))
55		hba1 1002	. . . . . . . . . . . . . . . . . . . . 21 |- (A.z w = x -> A.zA.z w = x)
56		elequ1 1135	. . . . . . . . . . . . . . . . . . . . . 22 |- (w = x -> (w e. y <-> x e. y))
57	56	a4s 983	. . . . . . . . . . . . . . . . . . . . 21 |- (A.z w = x -> (w e. y <-> x e. y))
58	55, 57	exbid 1104	. . . . . . . . . . . . . . . . . . . 20 |- (A.z w = x -> (E.z w e. y <-> E.z x e. y))
59	58	adantl 388	. . . . . . . . . . . . . . . . . . 19 |- ((-. A.x x = z /\ A.z w = x) -> (E.z w e. y <-> E.z x e. y))
60	54, 59