Theorem axpowndlem3 5016

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 5015	. 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 5014	. 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 1187	. . . . . 6 |- (A.x x = z -> A.xA.x x = z)
4		hbae 1187	. . . . . . 7 |- (A.x x = z -> A.yA.x x = z)
5		nd3 5005	. . . . . . . . . . 11 |- (A.x x = z -> -. A.y x e. z)
6		mtt 724	. . . . . . . . . . 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 1182	. . . . . . . . . . . 12 |- (A.z z = x -> (A.z -. x e. y -> A.x -. x e. y))
9	8	alequcoms 1185	. . . . . . . . . . 11 |- (A.x x = z -> (A.z -. x e. y -> A.x -. x e. y))
10		alnex 1074	. . . . . . . . . . 11 |- (A.z -. x e. y <-> -. E.z x e. y)
11		alnex 1074	. . . . . . . . . . 11 |- (A.x -. x e. y <-> -. E.x x e. y)
12	9, 10, 11	3imtr3g 563	. . . . . . . . . 10 |- (A.x x = z -> (-. E.z x e. y -> -. E.x x e. y))
13	7, 12	sylbird 212	. . . . . . . . 9 |- (A.x x = z -> ((E.z x e. y -> A.y x e. z) -> -. E.x x e. y))
14	13	a4sd 1026	. . . . . . . 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 1037	. . . . . 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 1103	. . . . 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 2826	. . . . . . . . 9 |- {(/)} e. V
19		eleq2 1582	. . . . . . . . . . 11 |- (x = {(/)} -> (w e. x <-> w e. {(/)}))
20	19	imbi2d 623	. . . . . . . . . 10 |- (x = {(/)} -> ((w = (/) -> w e. x) <-> (w = (/) -> w e. {(/)})))
21	20	albidv 1320	. . . . . . . . 9 |- (x = {(/)} -> (A.w(w = (/) -> w e. x) <-> A.w(w = (/) -> w e. {(/)})))
22	18, 21	cla4ev 1916	. . . . . . . 8 |- (A.w(w = (/) -> w e. {(/)}) -> E.xA.w(w = (/) -> w e. x))
23		0ex 2766	. . . . . . . . . 10 |- (/) e. V
24	23	snid 2487	. . . . . . . . 9 |- (/) e. {(/)}
25		eleq1 1581	. . . . . . . . 9 |- (w = (/) -> (w e. {(/)} <-> (/) e. {(/)}))
26	24, 25	mpbiri 201	. . . . . . . 8 |- (w = (/) -> w e. {(/)})
27	22, 26	mpg 1027	. . . . . . 7 |- E.xA.w(w = (/) -> w e. x)
28		n0 2341	. . . . . . . . . . 11 |- (-. w = (/) <-> E.x x e. w)
29	28	con1bii 227	. . . . . . . . . 10 |- (-. E.x x e. w <-> w = (/))
30	29	imbi1i 193	. . . . . . . . 9 |- ((-. E.x x e. w -> w e. x) <-> (w = (/) -> w e. x))
31	30	albii 1040	. . . . . . . 8 |- (A.w(-. E.x x e. w -> w e. x) <-> A.w(w = (/) -> w e. x))
32	31	exbii 1092	. . . . . . 7 |- (E.xA.w(-. E.x x e. w -> w e. x) <-> E.xA.w(w = (/) -> w e. x))
33	27, 32	mpbir 197	. . . . . 6 |- E.xA.w(-. E.x x e. w -> w e. x)
34		hbnae 1189	. . . . . . 7 |- (-. A.x x = y -> A.x -. A.x x = y)
35		hbnae 1189	. . . . . . . 8 |- (-. A.x x = y -> A.y -. A.x x = y)
36		dveel1 1398	. . . . . . . . . . . 12 |- (-. A.y y = x -> (x e. w -> A.y x e. w))
37	36	nalequcoms 1186	. . . . . . . . . . 11 |- (-. A.x x = y -> (x e. w -> A.y x e. w))
38	34, 37	hbexd 1155	. . . . . . . . . 10 |- (-. A.x x = y -> (E.x x e. w -> A.yE.x x e. w))
39	35, 38	hbnd 1150	. . . . . . . . 9 |- (-. A.x x = y -> (-. E.x x e. w -> A.y -. E.x x e. w))
40		dveel2 1399	. . . . . . . . . 10 |- (-. A.y y = x -> (w e. x -> A.y w e. x))
41	40	nalequcoms 1186	. . . . . . . . 9 |- (-. A.x x = y -> (w e. x -> A.y w e. x))
42	35, 39, 41	hbimd 1151	. . . . . . . 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 1254	. . . . . . . . . . . . 13 |- (-. A.x x = y -> (w = y -> A.x w = y))
44	43	imdistani 454	. . . . . . . . . . . 12 |- ((-. A.x x = y /\ w = y) -> (-. A.x x = y /\ A.x w = y))
45		hba1 1044	. . . . . . . . . . . . . 14 |- (A.x w = y -> A.xA.x w = y)
46		elequ2 1179	. . . . . . . . . . . . . . 15 |- (w = y -> (x e. w <-> x e. y))
47	46	a4s 1025	. . . . . . . . . . . . . 14 |- (A.x w = y -> (x e. w <-> x e. y))
48	45, 47	exbid 1146	. . . . . . . . . . . . 13 |- (A.x w = y -> (E.x x e. w <-> E.x x e. y))
49	48	adantl 397	. . . . . . . . . . . 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	notbid 622	. . . . . . . . . 10 |- ((-. A.x x = y /\ w = y) -> (-. E.x x e. w <-> -. E.x x e. y))
52		elequ1 1178	. . . . . . . . . . 11 |- (w = y -> (w e. x <-> y e. x))
53	52	adantl 397	. . . . . . . . . 10 |- ((-. A.x x = y /\ w = y) -> (w e. x <-> y e. x))
54	51, 53	imbi12d 637	. . . . . . . . 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 380	. . . . . . . 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 1362	. . . . . . 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 1146	. . . . . 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 200	. . . . 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 135	. 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 136	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 153   /\ wa 230  A.wal 995   = wceq 997   e. wcel 999  E.wex 1021  (/)c0 2331  {csn 2461

This theorem is referenced by:  axpowndlem4 5017

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-sep 2758  ax-nul 2765  ax-pow 2798  ax-reg 4653

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-ral 1696  df-rex 1697  df-v 1859  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-nul 2332  df-pw 2454  df-sn 2464  df-pr 2465

Copyright terms: Public domain