Theorem axpowndlem3 4923

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 4922	. 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 4921	. 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 1141	. . . . . 6 |- (A.x x = z -> A.xA.x x = z)
4		hbae 1141	. . . . . . 7 |- (A.x x = z -> A.yA.x x = z)
5		nd3 4912	. . . . . . . . . . 11 |- (A.x x = z -> -. A.y x e. z)
6		mtt 710	. . . . . . . . . . 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 1136	. . . . . . . . . . . 12 |- (A.z z = x -> (A.z -. x e. y -> A.x -. x e. y))
9	8	alequcoms 1139	. . . . . . . . . . 11 |- (A.x x = z -> (A.z -. x e. y -> A.x -. x e. y))
10		alnex 1029	. . . . . . . . . . 11 |- (A.z -. x e. y <-> -. E.z x e. y)
11		alnex 1029	. . . . . . . . . . 11 |- (A.x -. x e. y <-> -. E.x x e. y)
12	9, 10, 11	3imtr3g 550	. . . . . . . . . 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 982	. . . . . . . 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 993	. . . . . 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 1058	. . . . 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 2760	. . . . . . . . 9 |- {(/)} e. V
19		eleq2 1527	. . . . . . . . . . 11 |- (x = {(/)} -> (w e. x <-> w e. {(/)}))
20	19	imbi2d 610	. . . . . . . . . 10 |- (x = {(/)} -> ((w = (/) -> w e. x) <-> (w = (/) -> w e. {(/)})))
21	20	albidv 1273	. . . . . . . . 9 |- (x = {(/)} -> (A.w(w = (/) -> w e. x) <-> A.w(w = (/) -> w e. {(/)})))
22	18, 21	cla4ev 1860	. . . . . . . 8 |- (A.w(w = (/) -> w e. {(/)}) -> E.xA.w(w = (/) -> w e. x))
23		0ex 2701	. . . . . . . . . 10 |- (/) e. V
24	23	snid 2425	. . . . . . . . 9 |- (/) e. {(/)}
25		eleq1 1526	. . . . . . . . 9 |- (w = (/) -> (w e. {(/)} <-> (/) e. {(/)}))
26	24, 25	mpbiri 194	. . . . . . . 8 |- (w = (/) -> w e. {(/)})
27	22, 26	mpg 983	. . . . . . 7 |- E.xA.w(w = (/) -> w e. x)
28		n0 2279	. . . . . . . . . . 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 996	. . . . . . . 8 |- (A.w(-. E.x x e. w -> w e. x) <-> A.w(w = (/) -> w e. x))
32	31	exbii 1047	. . . . . . 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 1143	. . . . . . 7 |- (-. A.x x = y -> A.x -. A.x x = y)
35		hbnae 1143	. . . . . . . 8 |- (-. A.x x = y -> A.y -. A.x x = y)
36		dveel1 1349	. . . . . . . . . . . 12 |- (-. A.y y = x -> (x e. w -> A.y x e. w))
37	36	nalequcoms 1140	. . . . . . . . . . 11 |- (-. A.x x = y -> (x e. w -> A.y x e. w))
38	34, 37	hbexd 1110	. . . . . . . . . 10 |- (-. A.x x = y -> (E.x x e. w -> A.yE.x x e. w))
39	35, 38	hbnd 1105	. . . . . . . . 9 |- (-. A.x x = y -> (-. E.x x e. w -> A.y -. E.x x e. w))
40		dveel2 1350	. . . . . . . . . 10 |- (-. A.y y = x -> (w e. x -> A.y w e. x))
41	40	nalequcoms 1140	. . . . . . . . 9 |- (-. A.x x = y -> (w e. x -> A.y w e. x))
42	35, 39, 41	hbimd 1106	. . . . . . . 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 1208	. . . . . . . . . . . . 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 1000	. . . . . . . . . . . . . 14 |- (A.x w = y -> A.xA.x w = y)
46		elequ2 1133	. . . . . . . . . . . . . . 15 |- (w = y -> (x e. w <-> x e. y))
47	46	a4s 981	. . . . . . . . . . . . . 14 |- (A.x w = y -> (x e. w <-> x e. y))
48	45, 47	exbid 1101	. . . . . . . . . . . . 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 609	. . . . . . . . . 10 |- ((-. A.x x = y /\ w = y) -> (-. E.x x e. w <-> -. E.x x e. y))
52		elequ1 1132	. . . . . . . . . . 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 624	. . . . . . . . 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 1315	. . . . . . 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 1101	. . . . . 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 951   = wceq 953   e. wcel 955  E.wex 977  (/)c0 2270  {csn 2399

This theorem is referenced by:  axpowndlem4 4924

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693  ax-nul 2700  ax-pow 2732  ax-reg 4565

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-ral 1641  df-rex 1642  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403

Copyright terms: Public domain