Theorem pwadjoin 4120

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

Assertion

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∨ wo 357   ∧ wa 358   = wceq 1642   ∈ wcel 1710  {cab 2339  ∃wrex 2616   ∖ cdif 3207   ∪ cun 3208   ⊆ wss 3258  ℘cpw 3723  {csn 3738

This proof depends on 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 proof 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 used by:  nnadjoinpw  4522