Theorem axpowndlem3 4951

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

Assertion

Ref	Expression
axpowndlem3	|- (-. 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 axpowndlem3

Step	Hyp	Ref	Expression
1		axpowndlem2 4950	. 2 |- (-. 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))))
2		axpowndlem1 4949	. 2 |- (A.x x = y -> (-. x = y -> E.xA.y(A.x(E.z x e. y -> A.y x e. z) -> y e. x)))
3		hbae 1145	. . . . . 6 |- (A.x x = z -> A.xA.x x = z)
4		hbae 1145	. . . . . . 7 |- (A.x x = z -> A.yA.x x = z)
5		nd3 4940	. . . . . . . . . . 11 |- (A.x x = z -> -. A.y x e. z)
6		mtt 712	. . . . . . . . . . 11 |- (-. A.y x e. z -> (-. E.z x e. y <-> (E.z x e. y -> A.y x e. z)))
7	5, 6	syl 10	. . . . . . . . . 10 |- (A.x x = z -> (-. E.z x e. y <-> (E.z x e. y -> A.y x e. z)))
8		ax-10o 1140	. . . . . . . . . . . 12 |- (A.z z = x -> (A.z -. x e. y -> A.x -. x e. y))
9	8	alequcoms 1143	. . . . . . . . . . 11 |- (A.x x = z -> (A.z -. x e. y -> A.x -. x e. y))
10		alnex 1033	. . . . . . . . . . 11 |- (A.z -. x e. y <-> -. E.z x e. y)
11		alnex 1033	. . . . . . . . . . 11 |- (A.x -. x e. y <-> -. E.x x e. y)
12	9, 10, 11	3imtr3g 552	. . . . . . . . . 10 |- (A.x x = z -> (-. E.z x e. y -> -. E.x x e. y))
13	7, 12	sylbird 205	. . . . . . . . 9 |- (A.x x = z -> ((E.z x e. y -> A.y x e. z) -> -. E.x x e. y))
14	13	a4sd 985	. . . . . . . 8 |- (A.x x = z -> (A.x(E.z x e. y -> A.y x e. z) -> -. E.x x e. y))
15	14	imim1d 28	. . . . . . 7 |- (A.x x = z -> ((-. E.x x e. y -> y e. x) -> (A.x(E.z x e. y -> A.y x e. z) -> y e. x)))
16	4, 15	19.20d 996	. . . . . 6 |- (A.x x = z -> (A.y(-. E.x x e. y -> y e. x) -> A.y(A.x(E.z x e. y -> A.y x e. z) -> y e. x)))
17	3, 16	19.22d 1062	. . . . 5 |- (A.x x = z -> (E.xA.y(-. E.x x e. y -> y e. x) -> E.xA.y(A.x(E.z x e. y -> A.y x e. z) -> y e. x)))
18		p0ex 2770	. . . . . . . . 9 |- {(/)} e. V
19		eleq2 1535	. . . . . . . . . . 11 |- (x = {(/)} -> (w e. x <-> w e. {(/)}))
20	19	imbi2d 612	. . . . . . . . . 10 |- (x = {(/)} -> ((w = (/) -> w e. x) <-> (w = (/) -> w e. {(/)})))
21	20	albidv 1278	. . . . . . . . 9 |- (x = {(/)} -> (A.w(w = (/) -> w e. x) <-> A.w(w = (/) -> w e. {(/)})))
22	18, 21	cla4ev 1869	. . . . . . . 8 |- (A.w(w = (/) -> w e. {(/)}) -> E.xA.w(w = (/) -> w e. x))
23		0ex 2711	. . . . . . . . . 10 |- (/) e. V
24	23	snid 2435	. . . . . . . . 9 |- (/) e. {(/)}
25		eleq1 1534	. . . . . . . . 9 |- (w = (/) -> (w e. {(/)} <-> (/) e. {(/)}))
26	24, 25	mpbiri 194	. . . . . . . 8 |- (w = (/) -> w e. {(/)})
27	22, 26	mpg 986	. . . . . . 7 |- E.xA.w(w = (/) -> w e. x)
28		n0 2289	. . . . . . . . . . 11 |- (-. w = (/) <-> E.x x e. w)
29	28	con1bii 220	. . . . . . . . . 10 |- (-. E.x x e. w <-> w = (/))
30	29	imbi1i 186	. . . . . . . . 9 |- ((-. E.x x e. w -> w e. x) <-> (w = (/) -> w e. x))
31	30	albii 999	. . . . . . . 8 |- (A.w(-. E.x x e. w -> w e. x) <-> A.w(w = (/) -> w e. x))
32	31	exbii 1051	. . . . . . 7 |- (E.xA.w(-. E.x x e. w -> w e. x) <-> E.xA.w(w = (/) -> w e. x))
33	27, 32	mpbir 190	. . . . . 6 |- E.xA.w(-. E.x x e. w -> w e. x)
34		hbnae 1147	. . . . . . 7 |- (-. A.x x = y -> A.x -. A.x x = y)
35		hbnae 1147	. . . . . . . 8 |- (-. A.x x = y -> A.y -. A.x x = y)
36		dveel1 1356	. . . . . . . . . . . 12 |- (-. A.y y = x -> (x e. w -> A.y x e. w))
37	36	nalequcoms 1144	. . . . . . . . . . 11 |- (-. A.x x = y -> (x e. w -> A.y x e. w))
38	34, 37	hbexd 1114	. . . . . . . . . 10 |- (-. A.x x = y -> (E.x x e. w -> A.yE.x x e. w))
39	35, 38	hbnd 1109	. . . . . . . . 9 |- (-. A.x x = y -> (-. E.x x e. w -> A.y -. E.x x e. w))
40		dveel2 1357	. . . . . . . . . 10 |- (-. A.y y = x -> (w e. x -> A.y w e. x))
41	40	nalequcoms 1144	. . . . . . . . 9 |- (-. A.x x = y -> (w e. x -> A.y w e. x))
42	35, 39, 41	hbimd 1110	. . . . . . . 8 |- (-. A.x x = y -> ((-. E.x x e. w -> w e. x) -> A.y(-. E.x x e. w -> w e. x)))
43		dveeq2 1212	. . . . . . . . . . . . 13 |- (-. A.x x = y -> (w = y -> A.x w = y))
44	43	imdistani 443	. . . . . . . . . . . 12 |- ((-. A.x x = y /\ w = y) -> (-. A.x x = y /\ A.x w = y))
45		hba1 1003	. . . . . . . . . . . . . 14 |- (A.x w = y -> A.xA.x w = y)
46		elequ2 1137	. . . . . . . . . . . . . . 15 |- (w = y -> (x e. w <-> x e. y))
47	46	a4s 984	. . . . . . . . . . . . . 14 |- (A.x w = y -> (x e. w <-> x e. y))
48	45, 47	exbid 1105	. . . . . . . . . . . . 13 |- (A.x w = y -> (E.x x e. w <-> E.x x e. y))
49	48	adantl 388	. . . . . . . . . . . 12 |- ((-. A.x x = y /\ A.x w = y) -> (E.x x e. w <-> E.x x e. y))
50	44, 49	syl 10	. . . . . . . . . . 11 |- ((-. A.x x = y /\ w = y) -> (E.x x e. w <-> E.x x e. y))
51	50	negbid 611	. . . . . . . . . 10 |- ((-. A.x x = y /\ w = y) -> (-. E.x x e. w <-> -. E.x x e. y))
52		elequ1 1136	. . . . . . . . . . 11 |- (w = y -> (w e. x <-> y e. x))
53	52	adantl 388	. . . . . . . . . 10 |- ((-. A.x x = y /\ w = y) -> (w e. x <-> y e. x))
54	51, 53	imbi12d 626	. . . . . . . . 9 |- ((-. A.x x = y /\ w = y) -> ((-. E.x x e. w -> w e. x) <-> (-. E.x x e. y -> y e. x)))
55	54	ex 373	. . . . . . . 8 |- (-. A.x x = y -> (w = y -> ((-. E.x x e. w -> w e. x) <-> (-. E.x x e. y -> y e. x))))
56	35, 42, 55	cbvald 1320	. . . . . . 7 |- (-. A.x x = y -> (A.w(-. E.x x e. w -> w e. x) <-> A.y(-. E.x x e. y -> y e. x)))
57	34, 56	exbid 1105	. . . . . 6 |- (-. A.x x = y -> (E.xA.w(-. E.x x e. w -> w e. x) <-> E.xA.y(-. E.x x e. y -> y e. x)))
58	33, 57	mpbii 193	. . . . 5 |- (-. A.x x = y -> E.xA.y(-. E.x x e. y -> y e. x))
59	17, 58	syl5 21	. . . 4 |- (A.x x = z -> (-. A.x x = y -> E.xA.y(A.x(E.z x e. y -> A.y x e. z) -> y e. x)))
60	59	a1dd 42	. . 3 |- (A.x x = z -> (-. A.x x = y -> (-. x = y -> E.xA.y(A.x(E.z x e. y -> A.y x e. z) -> y e. x))))
61	60, 2	pm2.61d2 129	. 2 |- (A.x x = z -> (-. x = y -> E.xA.y(A.x(E.z x e. y -> A.y x e. z) -> y e. x)))
62	1, 2, 61	pm2.61ii 130	1 |- (-. x = y -> E.xA.y(A.x(E.z x e. y -> A.y x e. z) -> y e. x))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   /\ wa 223  A.wal 954   = wceq 956   e. wcel 958  E.wex 980  (/)c0 2280  {csn 2409

This theorem is referenced by:  axpowndlem4 4952

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703  ax-nul 2710  ax-pow 2742  ax-reg 4593

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-ral 1649  df-rex 1650  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-pr 2413

Copyright terms: Public domain