Theorem axpowndlem3 4970

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 4969	. 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 4968	. 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 1147	. . . . . 6 |- (A.x x = z -> A.xA.x x = z)
4		hbae 1147	. . . . . . 7 |- (A.x x = z -> A.yA.x x = z)
5		nd3 4959	. . . . . . . . . . 11 |- (A.x x = z -> -. A.y x e. z)
6		mtt 714	. . . . . . . . . . 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 1142	. . . . . . . . . . . 12 |- (A.z z = x -> (A.z -. x e. y -> A.x -. x e. y))
9	8	alequcoms 1145	. . . . . . . . . . 11 |- (A.x x = z -> (A.z -. x e. y -> A.x -. x e. y))
10		alnex 1035	. . . . . . . . . . 11 |- (A.z -. x e. y <-> -. E.z x e. y)
11		alnex 1035	. . . . . . . . . . 11 |- (A.x -. x e. y <-> -. E.x x e. y)
12	9, 10, 11	3imtr3g 554	. . . . . . . . . 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 987	. . . . . . . 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 998	. . . . . 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 1064	. . . . 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 2777	. . . . . . . . 9 |- {(/)} e. V
19		eleq2 1538	. . . . . . . . . . 11 |- (x = {(/)} -> (w e. x <-> w e. {(/)}))
20	19	imbi2d 614	. . . . . . . . . 10 |- (x = {(/)} -> ((w = (/) -> w e. x) <-> (w = (/) -> w e. {(/)})))
21	20	albidv 1280	. . . . . . . . 9 |- (x = {(/)} -> (A.w(w = (/) -> w e. x) <-> A.w(w = (/) -> w e. {(/)})))
22	18, 21	cla4ev 1872	. . . . . . . 8 |- (A.w(w = (/) -> w e. {(/)}) -> E.xA.w(w = (/) -> w e. x))
23		0ex 2717	. . . . . . . . . 10 |- (/) e. V
24	23	snid 2440	. . . . . . . . 9 |- (/) e. {(/)}
25		eleq1 1537	. . . . . . . . 9 |- (w = (/) -> (w e. {(/)} <-> (/) e. {(/)}))
26	24, 25	mpbiri 194	. . . . . . . 8 |- (w = (/) -> w e. {(/)})
27	22, 26	mpg 988	. . . . . . 7 |- E.xA.w(w = (/) -> w e. x)
28		n0 2294	. . . . . . . . . . 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 1001	. . . . . . . 8 |- (A.w(-. E.x x e. w -> w e. x) <-> A.w(w = (/) -> w e. x))
32	31	exbii 1053	. . . . . . 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 1149	. . . . . . 7 |- (-. A.x x = y -> A.x -. A.x x = y)
35		hbnae 1149	. . . . . . . 8 |- (-. A.x x = y -> A.y -. A.x x = y)
36		dveel1 1358	. . . . . . . . . . . 12 |- (-. A.y y = x -> (x e. w -> A.y x e. w))
37	36	nalequcoms 1146	. . . . . . . . . . 11 |- (-. A.x x = y -> (x e. w -> A.y x e. w))
38	34, 37	hbexd 1116	. . . . . . . . . 10 |- (-. A.x x = y -> (E.x x e. w -> A.yE.x x e. w))
39	35, 38	hbnd 1111	. . . . . . . . 9 |- (-. A.x x = y -> (-. E.x x e. w -> A.y -. E.x x e. w))
40		dveel2 1359	. . . . . . . . . 10 |- (-. A.y y = x -> (w e. x -> A.y w e. x))
41	40	nalequcoms 1146	. . . . . . . . 9 |- (-. A.x x = y -> (w e. x -> A.y w e. x))
42	35, 39, 41	hbimd 1112	. . . . . . . 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 1214	. . . . . . . . . . . . 13 |- (-. A.x x = y -> (w = y -> A.x w = y))
44	43	imdistani 445	. . . . . . . . . . . 12 |- ((-. A.x x = y /\ w = y) -> (-. A.x x = y /\ A.x w = y))
45		hba1 1005	. . . . . . . . . . . . . 14 |- (A.x w = y -> A.xA.x w = y)
46		elequ2 1139	. . . . . . . . . . . . . . 15 |- (w = y -> (x e. w <-> x e. y))
47	46	a4s 986	. . . . . . . . . . . . . 14 |- (A.x w = y -> (x e. w <-> x e. y))
48	45, 47	exbid 1107	. . . . . . . . . . . . 13 |- (A.x w = y -> (E.x x e. w <-> E.x x e. y))
49	48	adantl 390	. . . . . . . . . . . 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 613	. . . . . . . . . 10 |- ((-. A.x x = y /\ w = y) -> (-. E.x x e. w <-> -. E.x x e. y))
52		elequ1 1138	. . . . . . . . . . 11 |- (w = y -> (w e. x <-> y e. x))
53	52	adantl 390	. . . . . . . . . 10 |- ((-. A.x x = y /\ w = y) -> (w e. x <-> y e. x))
54	51, 53	imbi12d 628	. . . . . . . . 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 1322	. . . . . . 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 1107	. . . . . 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 956   = wceq 958   e. wcel 960  E.wex 982  (/)c0 2284  {csn 2414

This theorem is referenced by:  axpowndlem4 4971

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-sep 2709  ax-nul 2716  ax-pow 2749  ax-reg 4609

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-ral 1652  df-rex 1653  df-v 1815  df-dif 2053  df-un 2054  df-in 2055  df-ss 2057  df-nul 2285  df-pw 2407  df-sn 2417  df-pr 2418

Copyright terms: Public domain