Theorem axpowndlem3 4874

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 4873	. 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 4872	. 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 1128	. . . . . 6 |- (A.x x = z -> A.xA.x x = z)
4		hbae 1128	. . . . . . 7 |- (A.x x = z -> A.yA.x x = z)
5		nd3 4863	. . . . . . . . . . 11 |- (A.x x = z -> -. A.y x e. z)
6		mtt 709	. . . . . . . . . . 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-10 1103	. . . . . . . . . . . 12 |- (A.z z = x -> (A.z -. x e. y -> A.x -. x e. y))
9	8	alequcoms 1126	. . . . . . . . . . 11 |- (A.x x = z -> (A.z -. x e. y -> A.x -. x e. y))
10		alnex 1009	. . . . . . . . . . 11 |- (A.z -. x e. y <-> -. E.z x e. y)
11		alnex 1009	. . . . . . . . . . 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 961	. . . . . . . 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 972	. . . . . 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 1038	. . . . 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 2738	. . . . . . . . 9 |- {(/)} e. V
19		eleq2 1511	. . . . . . . . . . 11 |- (x = {(/)} -> (w e. x <-> w e. {(/)}))
20	19	imbi2d 610	. . . . . . . . . 10 |- (x = {(/)} -> ((w = (/) -> w e. x) <-> (w = (/) -> w e. {(/)})))
21	20	albidv 1260	. . . . . . . . 9 |- (x = {(/)} -> (A.w(w = (/) -> w e. x) <-> A.w(w = (/) -> w e. {(/)})))
22	18, 21	cla4ev 1842	. . . . . . . 8 |- (A.w(w = (/) -> w e. {(/)}) -> E.xA.w(w = (/) -> w e. x))
23		0ex 2679	. . . . . . . . . 10 |- (/) e. V
24	23	snid 2406	. . . . . . . . 9 |- (/) e. {(/)}
25		eleq1 1510	. . . . . . . . 9 |- (w = (/) -> (w e. {(/)} <-> (/) e. {(/)}))
26	24, 25	mpbiri 194	. . . . . . . 8 |- (w = (/) -> w e. {(/)})
27	22, 26	mpg 962	. . . . . . 7 |- E.xA.w(w = (/) -> w e. x)
28		n0 2260	. . . . . . . . . . 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 975	. . . . . . . 8 |- (A.w(-. E.x x e. w -> w e. x) <-> A.w(w = (/) -> w e. x))
32	31	exbii 1027	. . . . . . 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 1130	. . . . . . 7 |- (-. A.x x = y -> A.x -. A.x x = y)
35		hbnae 1130	. . . . . . . 8 |- (-. A.x x = y -> A.y -. A.x x = y)
36		dveel1 1336	. . . . . . . . . . . 12 |- (-. A.y y = x -> (x e. w -> A.y x e. w))
37	36	nalequcoms 1127	. . . . . . . . . . 11 |- (-. A.x x = y -> (x e. w -> A.y x e. w))
38	34, 37	hbexd 1090	. . . . . . . . . 10 |- (-. A.x x = y -> (E.x x e. w -> A.yE.x x e. w))
39	35, 38	hbnd 1085	. . . . . . . . 9 |- (-. A.x x = y -> (-. E.x x e. w -> A.y -. E.x x e. w))
40		dveel2 1337	. . . . . . . . . 10 |- (-. A.y y = x -> (w e. x -> A.y w e. x))
41	40	nalequcoms 1127	. . . . . . . . 9 |- (-. A.x x = y -> (w e. x -> A.y w e. x))
42	35, 39, 41	hbimd 1086	. . . . . . . 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 1197	. . . . . . . . . . . . 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 979	. . . . . . . . . . . . . 14 |- (A.x w = y -> A.xA.x w = y)
46		elequ2 1124	. . . . . . . . . . . . . . 15 |- (w = y -> (x e. w <-> x e. y))
47	46	a4s 960	. . . . . . . . . . . . . 14 |- (A.x w = y -> (x e. w <-> x e. y))
48	45, 47	exbid 1081	. . . . . . . . . . . . 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 1123	. . . . . . . . . . 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 1302	. . . . . . 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 1081	. . . . . 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 950  E.wex 956   = wceq 1099   e. wcel 1105  (/)c0 2251  {csn 2380

This theorem is referenced by:  axpowndlem4 4875

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-13 1107  ax-14 1108  ax-11 1180  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436  ax-sep 2671  ax-nul 2678  ax-pow 2710  ax-reg 4517

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 957  df-sb 1155  df-eu 1359  df-mo 1360  df-clab 1441  df-cleq 1446  df-clel 1449  df-ne 1563  df-ral 1625  df-rex 1626  df-v 1787  df-dif 2020  df-un 2021  df-in 2022  df-ss 2024  df-nul 2252  df-pw 2373  df-sn 2383  df-pr 2384

Copyright terms: Public domain