Theorem unipw 2746

Description: A class equals the union of its power class. Exercise 6(a) of [Enderton] p. 38.

Assertion

Ref	Expression
unipw	|- U.P~A = A

Proof of Theorem unipw

Step	Hyp	Ref	Expression
1		eluni 2496	. . . 4 |- (x e. U.P~A <-> E.y(x e. y /\ y e. P~A))
2		visset 1804	. . . . . . . 8 |- y e. V
3	2	elpw 2394	. . . . . . 7 |- (y e. P~A <-> y (_ A)
4		ssel 2053	. . . . . . 7 |- (y (_ A -> (x e. y -> x e. A))
5	3, 4	sylbi 199	. . . . . 6 |- (y e. P~A -> (x e. y -> x e. A))
6	5	impcom 351	. . . . 5 |- ((x e. y /\ y e. P~A) -> x e. A)
7	6	19.23aiv 1290	. . . 4 |- (E.y(x e. y /\ y e. P~A) -> x e. A)
8	1, 7	sylbi 199	. . 3 |- (x e. U.P~A -> x e. A)
9	8	ssriv 2059	. 2 |- U.P~A (_ A
10		visset 1804	. . . . . 6 |- x e. V
11	10	snid 2425	. . . . 5 |- x e. {x}
12		snex 2740	. . . . . 6 |- {x} e. V
13		eleq2 1527	. . . . . . 7 |- (y = {x} -> (x e. y <-> x e. {x}))
14		eleq1 1526	. . . . . . 7 |- (y = {x} -> (y e. P~A <-> {x} e. P~A))
15	13, 14	anbi12d 626	. . . . . 6 |- (y = {x} -> ((x e. y /\ y e. P~A) <-> (x e. {x} /\ {x} e. P~A)))
16	12, 15	cla4ev 1860	. . . . 5 |- ((x e. {x} /\ {x} e. P~A) -> E.y(x e. y /\ y e. P~A))
17	11, 16	mpan 693	. . . 4 |- ({x} e. P~A -> E.y(x e. y /\ y e. P~A))
18	10	snelpw 2742	. . . 4 |- (x e. A <-> {x} e. P~A)
19	17, 18, 1	3imtr4 219	. . 3 |- (x e. A -> x e. U.P~A)
20	19	ssriv 2059	. 2 |- A (_ U.P~A
21	9, 20	eqssi 2068	1 |- U.P~A = A

Syntax hints:   -> wi 3   /\ wa 223   = wceq 953   e. wcel 955  E.wex 977   (_ wss 2037  P~cpw 2391  {csn 2399  U.cuni 2493

This theorem is referenced by:  sspwuni 2748  pwexb 2898  univ 2899  unixpss 3248  unirnioo 6335  distop 7591  distps 7596  cncnplem1 7713  uniopn 7801  opnuni 7808  dfchsup2 9213  hsupval2t 9215  hsupvalt 9216  shsupclt 9221  shsupunss 9230  mapdiscn 10398  fgsb 10444  dtopcl 10459  dtt2 10462

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-pow 2732

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-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  df-uni 2494

Copyright terms: Public domain