Theorem pwadjoin 4120

Description: Compute the power class of an adjoinment. (Contributed by SF, 30-Jan-2015.)

Assertion

Ref	Expression
pwadjoin	|- ~P(A u. {X}) = (~PA u. {a | E.b e. ~P Aa = (b u. {X})})

Distinct variable groups:   A,a,b   X,a,b

Proof of Theorem pwadjoin

Dummy variables x z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		uncom 3409	. . . . . . . . . . . . . . 15 |- (A u. {X}) = ({X} u. A)
2	1	sseq2i 3297	. . . . . . . . . . . . . 14 |- (z C_ (A u. {X}) <-> z C_ ({X} u. A))
3		ssundif 3634	. . . . . . . . . . . . . 14 |- (z C_ ({X} u. A) <-> (z \ {X}) C_ A)
4	2, 3	bitri 240	. . . . . . . . . . . . 13 |- (z C_ (A u. {X}) <-> (z \ {X}) C_ A)
5	4	biimpi 186	. . . . . . . . . . . 12 |- (z C_ (A u. {X}) -> (z \ {X}) C_ A)
6	5	adantr 451	. . . . . . . . . . 11 |- ((z C_ (A u. {X}) /\ X e. z) -> (z \ {X}) C_ A)
7		vex 2863	. . . . . . . . . . . . 13 |- z e. _V
8		snex 4112	. . . . . . . . . . . . 13 |- {X} e. _V
9	7, 8	difex 4108	. . . . . . . . . . . 12 |- (z \ {X}) e. _V
10	9	elpw 3729	. . . . . . . . . . 11 |- ((z \ {X}) e. ~PA <-> (z \ {X}) C_ A)
11	6, 10	sylibr 203	. . . . . . . . . 10 |- ((z C_ (A u. {X}) /\ X e. z) -> (z \ {X}) e. ~PA)
12		difsnid 3855	. . . . . . . . . . . 12 |- (X e. z -> ((z \ {X}) u. {X}) = z)
13	12	eqcomd 2358	. . . . . . . . . . 11 |- (X e. z -> z = ((z \ {X}) u. {X}))
14	13	adantl 452	. . . . . . . . . 10 |- ((z C_ (A u. {X}) /\ X e. z) -> z = ((z \ {X}) u. {X}))
15		uneq1 3412	. . . . . . . . . . . 12 |- (b = (z \ {X}) -> (b u. {X}) = ((z \ {X}) u. {X}))
16	15	eqeq2d 2364	. . . . . . . . . . 11 |- (b = (z \ {X}) -> (z = (b u. {X}) <-> z = ((z \ {X}) u. {X})))
17	16	rspcev 2956	. . . . . . . . . 10 |- (((z \ {X}) e. ~PA /\ z = ((z \ {X}) u. {X})) -> E.b e. ~P Az = (b u. {X}))
18	11, 14, 17	syl2anc 642	. . . . . . . . 9 |- ((z C_ (A u. {X}) /\ X e. z) -> E.b e. ~P Az = (b u. {X}))
19	18	ex 423	. . . . . . . 8 |- (z C_ (A u. {X}) -> (X e. z -> E.b e. ~P Az = (b u. {X})))
20	19	con3d 125	. . . . . . 7 |- (z C_ (A u. {X}) -> (-. E.b e. ~P Az = (b u. {X}) -> -. X e. z))
21		ssel 3268	. . . . . . . . . . . . 13 |- (z C_ (A u. {X}) -> (x e. z -> x e. (A u. {X})))
22	21	com12 27	. . . . . . . . . . . 12 |- (x e. z -> (z C_ (A u. {X}) -> x e. (A u. {X})))
23		elun 3221	. . . . . . . . . . . . . . . 16 |- (x e. (A u. {X}) <-> (x e. A \/ x e. {X}))
24		elsn 3749	. . . . . . . . . . . . . . . . 17 |- (x e. {X} <-> x = X)
25	24	orbi2i 505	. . . . . . . . . . . . . . . 16 |- ((x e. A \/ x e. {X}) <-> (x e. A \/ x = X))
26	23, 25	bitri 240	. . . . . . . . . . . . . . 15 |- (x e. (A u. {X}) <-> (x e. A \/ x = X))
27		ax-1 6	. . . . . . . . . . . . . . . 16 |- (x e. A -> ((x e. z /\ -. X e. z) -> x e. A))
28		eleq1 2413	. . . . . . . . . . . . . . . . . 18 |- (x = X -> (x e. z <-> X e. z))
29	28	anbi1d 685	. . . . . . . . . . . . . . . . 17 |- (x = X -> ((x e. z /\ -. X e. z) <-> (X e. z /\ -. X e. z)))
30		pm2.21 100	. . . . . . . . . . . . . . . . . 18 |- (-. X e. z -> (X e. z -> x e. A))
31	30	impcom 419	. . . . . . . . . . . . . . . . 17 |- ((X e. z /\ -. X e. z) -> x e. A)
32	29, 31	syl6bi 219	. . . . . . . . . . . . . . . 16 |- (x = X -> ((x e. z /\ -. X e. z) -> x e. A))
33	27, 32	jaoi 368	. . . . . . . . . . . . . . 15 |- ((x e. A \/ x = X) -> ((x e. z /\ -. X e. z) -> x e. A))
34	26, 33	sylbi 187	. . . . . . . . . . . . . 14 |- (x e. (A u. {X}) -> ((x e. z /\ -. X e. z) -> x e. A))
35	34	exp3a 425	. . . . . . . . . . . . 13 |- (x e. (A u. {X}) -> (x e. z -> (-. X e. z -> x e. A)))
36	35	com12 27	. . . . . . . . . . . 12 |- (x e. z -> (x e. (A u. {X}) -> (-. X e. z -> x e. A)))
37	22, 36	syld 40	. . . . . . . . . . 11 |- (x e. z -> (z C_ (A u. {X}) -> (-. X e. z -> x e. A)))
38	37	imp3a 420	. . . . . . . . . 10 |- (x e. z -> ((z C_ (A u. {X}) /\ -. X e. z) -> x e. A))
39	38	com12 27	. . . . . . . . 9 |- ((z C_ (A u. {X}) /\ -. X e. z) -> (x e. z -> x e. A))
40	39	ssrdv 3279	. . . . . . . 8 |- ((z C_ (A u. {X}) /\ -. X e. z) -> z C_ A)
41	40	ex 423	. . . . . . 7 |- (z C_ (A u. {X}) -> (-. X e. z -> z C_ A))
42	20, 41	syld 40	. . . . . 6 |- (z C_ (A u. {X}) -> (-. E.b e. ~P Az = (b u. {X}) -> z C_ A))
43	42	orrd 367	. . . . 5 |- (z C_ (A u. {X}) -> (E.b e. ~P Az = (b u. {X}) \/ z C_ A))
44	43	orcomd 377	. . . 4 |- (z C_ (A u. {X}) -> (z C_ A \/ E.b e. ~P Az = (b u. {X})))
45		ssun3 3429	. . . . 5 |- (z C_ A -> z C_ (A u. {X}))
46		vex 2863	. . . . . . . . 9 |- b e. _V
47	46	elpw 3729	. . . . . . . 8 |- (b e. ~PA <-> b C_ A)
48		unss1 3433	. . . . . . . 8 |- (b C_ A -> (b u. {X}) C_ (A u. {X}))
49	47, 48	sylbi 187	. . . . . . 7 |- (b e. ~PA -> (b u. {X}) C_ (A u. {X}))
50		sseq1 3293	. . . . . . 7 |- (z = (b u. {X}) -> (z C_ (A u. {X}) <-> (b u. {X}) C_ (A u. {X})))
51	49, 50	syl5ibrcom 213	. . . . . 6 |- (b e. ~PA -> (z = (b u. {X}) -> z C_ (A u. {X})))
52	51	rexlimiv 2733	. . . . 5 |- (E.b e. ~P Az = (b u. {X}) -> z C_ (A u. {X}))
53	45, 52	jaoi 368	. . . 4 |- ((z C_ A \/ E.b e. ~P Az = (b u. {X})) -> z C_ (A u. {X}))
54	44, 53	impbii 180	. . 3 |- (z C_ (A u. {X}) <-> (z C_ A \/ E.b e. ~P Az = (b u. {X})))
55	7	elpw 3729	. . 3 |- (z e. ~P(A u. {X}) <-> z C_ (A u. {X}))
56		elun 3221	. . . 4 |- (z e. (~PA u. {a | E.b e. ~P Aa = (b u. {X})}) <-> (z e. ~PA \/ z e. {a | E.b e. ~P Aa = (b u. {X})}))
57	7	elpw 3729	. . . . 5 |- (z e. ~PA <-> z C_ A)
58		eqeq1 2359	. . . . . . 7 |- (a = z -> (a = (b u. {X}) <-> z = (b u. {X})))
59	58	rexbidv 2636	. . . . . 6 |- (a = z -> (E.b e. ~P Aa = (b u. {X}) <-> E.b e. ~P Az = (b u. {X})))
60	7, 59	elab 2986	. . . . 5 |- (z e. {a | E.b e. ~P Aa = (b u. {X})} <-> E.b e. ~P Az = (b u. {X}))
61	57, 60	orbi12i 507	. . . 4 |- ((z e. ~PA \/ z e. {a | E.b e. ~P Aa = (b u. {X})}) <-> (z C_ A \/ E.b e. ~P Az = (b u. {X})))
62	56, 61	bitri 240	. . 3 |- (z e. (~PA u. {a | E.b e. ~P Aa = (b u. {X})}) <-> (z C_ A \/ E.b e. ~P Az = (b u. {X})))
63	54, 55, 62	3bitr4i 268	. 2 |- (z e. ~P(A u. {X}) <-> z e. (~PA u. {a | E.b e. ~P Aa = (b u. {X})}))
64	63	eqriv 2350	1 |- ~P(A u. {X}) = (~PA u. {a | E.b e. ~P Aa = (b u. {X})})

Syntax hints:  -. wn 3   -> wi 4   \/ wo 357   /\ wa 358   = wceq 1642   e. wcel 1710  {cab 2339  E.wrex 2616   \ cdif 3207   u. cun 3208   C_ wss 3258  ~Pcpw 3723  {csn 3738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4079  ax-sn 4088

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ne 2519  df-ral 2620  df-rex 2621  df-v 2862  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-ss 3260  df-nul 3552  df-pw 3725  df-sn 3742

This theorem is referenced by:  nnadjoinpw  4522