Theorem ex-pw

Description: Example for df-pw . Example by David A. Wheeler. (Contributed by Mario Carneiro, 2-Jul-2016)

	Ref	Expression
Assertion	ex-pw	$$⊢A=\left\{3,5,7\right\}\to 𝒫A=\left(\left\{\varnothing \right\}\cup \left\{\left\{3\right\},\left\{5\right\},\left\{7\right\}\right\}\right)\cup \left(\left\{\left\{3,5\right\},\left\{3,7\right\},\left\{5,7\right\}\right\}\cup \left\{\left\{3,5,7\right\}\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		pweq	$$⊢A=\left\{3,5,7\right\}\to 𝒫A=𝒫\left\{3,5,7\right\}$$
2		qdass	$$⊢\left\{\varnothing ,\left\{3\right\}\right\}\cup \left\{\left\{5\right\},\left\{3,5\right\}\right\}=\left\{\varnothing ,\left\{3\right\},\left\{5\right\}\right\}\cup \left\{\left\{3,5\right\}\right\}$$
3		qdassr	$$⊢\left\{\left\{7\right\},\left\{3,7\right\}\right\}\cup \left\{\left\{5,7\right\},\left\{3,5,7\right\}\right\}=\left\{\left\{7\right\}\right\}\cup \left\{\left\{3,7\right\},\left\{5,7\right\},\left\{3,5,7\right\}\right\}$$
4	2 3	uneq12i	$$⊢\left(\left\{\varnothing ,\left\{3\right\}\right\}\cup \left\{\left\{5\right\},\left\{3,5\right\}\right\}\right)\cup \left(\left\{\left\{7\right\},\left\{3,7\right\}\right\}\cup \left\{\left\{5,7\right\},\left\{3,5,7\right\}\right\}\right)=\left(\left\{\varnothing ,\left\{3\right\},\left\{5\right\}\right\}\cup \left\{\left\{3,5\right\}\right\}\right)\cup \left(\left\{\left\{7\right\}\right\}\cup \left\{\left\{3,7\right\},\left\{5,7\right\},\left\{3,5,7\right\}\right\}\right)$$
5		pwtp	$$⊢𝒫\left\{3,5,7\right\}=\left(\left\{\varnothing ,\left\{3\right\}\right\}\cup \left\{\left\{5\right\},\left\{3,5\right\}\right\}\right)\cup \left(\left\{\left\{7\right\},\left\{3,7\right\}\right\}\cup \left\{\left\{5,7\right\},\left\{3,5,7\right\}\right\}\right)$$
6		df-tp	$$⊢\left\{\left\{3\right\},\left\{5\right\},\left\{7\right\}\right\}=\left\{\left\{3\right\},\left\{5\right\}\right\}\cup \left\{\left\{7\right\}\right\}$$
7	6	uneq2i	$$⊢\left\{\varnothing \right\}\cup \left\{\left\{3\right\},\left\{5\right\},\left\{7\right\}\right\}=\left\{\varnothing \right\}\cup \left(\left\{\left\{3\right\},\left\{5\right\}\right\}\cup \left\{\left\{7\right\}\right\}\right)$$
8		unass	$$⊢\left(\left\{\varnothing \right\}\cup \left\{\left\{3\right\},\left\{5\right\}\right\}\right)\cup \left\{\left\{7\right\}\right\}=\left\{\varnothing \right\}\cup \left(\left\{\left\{3\right\},\left\{5\right\}\right\}\cup \left\{\left\{7\right\}\right\}\right)$$
9	7 8	eqtr4i	$$⊢\left\{\varnothing \right\}\cup \left\{\left\{3\right\},\left\{5\right\},\left\{7\right\}\right\}=\left(\left\{\varnothing \right\}\cup \left\{\left\{3\right\},\left\{5\right\}\right\}\right)\cup \left\{\left\{7\right\}\right\}$$
10		tpass	$$⊢\left\{\varnothing ,\left\{3\right\},\left\{5\right\}\right\}=\left\{\varnothing \right\}\cup \left\{\left\{3\right\},\left\{5\right\}\right\}$$
11	10	uneq1i	$$⊢\left\{\varnothing ,\left\{3\right\},\left\{5\right\}\right\}\cup \left\{\left\{7\right\}\right\}=\left(\left\{\varnothing \right\}\cup \left\{\left\{3\right\},\left\{5\right\}\right\}\right)\cup \left\{\left\{7\right\}\right\}$$
12	9 11	eqtr4i	$$⊢\left\{\varnothing \right\}\cup \left\{\left\{3\right\},\left\{5\right\},\left\{7\right\}\right\}=\left\{\varnothing ,\left\{3\right\},\left\{5\right\}\right\}\cup \left\{\left\{7\right\}\right\}$$
13		unass	$$⊢\left(\left\{\left\{3,5\right\}\right\}\cup \left\{\left\{3,7\right\},\left\{5,7\right\}\right\}\right)\cup \left\{\left\{3,5,7\right\}\right\}=\left\{\left\{3,5\right\}\right\}\cup \left(\left\{\left\{3,7\right\},\left\{5,7\right\}\right\}\cup \left\{\left\{3,5,7\right\}\right\}\right)$$
14		tpass	$$⊢\left\{\left\{3,5\right\},\left\{3,7\right\},\left\{5,7\right\}\right\}=\left\{\left\{3,5\right\}\right\}\cup \left\{\left\{3,7\right\},\left\{5,7\right\}\right\}$$
15	14	uneq1i	$$⊢\left\{\left\{3,5\right\},\left\{3,7\right\},\left\{5,7\right\}\right\}\cup \left\{\left\{3,5,7\right\}\right\}=\left(\left\{\left\{3,5\right\}\right\}\cup \left\{\left\{3,7\right\},\left\{5,7\right\}\right\}\right)\cup \left\{\left\{3,5,7\right\}\right\}$$
16		df-tp	$$⊢\left\{\left\{3,7\right\},\left\{5,7\right\},\left\{3,5,7\right\}\right\}=\left\{\left\{3,7\right\},\left\{5,7\right\}\right\}\cup \left\{\left\{3,5,7\right\}\right\}$$
17	16	uneq2i	$$⊢\left\{\left\{3,5\right\}\right\}\cup \left\{\left\{3,7\right\},\left\{5,7\right\},\left\{3,5,7\right\}\right\}=\left\{\left\{3,5\right\}\right\}\cup \left(\left\{\left\{3,7\right\},\left\{5,7\right\}\right\}\cup \left\{\left\{3,5,7\right\}\right\}\right)$$
18	13 15 17	3eqtr4i	$$⊢\left\{\left\{3,5\right\},\left\{3,7\right\},\left\{5,7\right\}\right\}\cup \left\{\left\{3,5,7\right\}\right\}=\left\{\left\{3,5\right\}\right\}\cup \left\{\left\{3,7\right\},\left\{5,7\right\},\left\{3,5,7\right\}\right\}$$
19	12 18	uneq12i	$$⊢\left(\left\{\varnothing \right\}\cup \left\{\left\{3\right\},\left\{5\right\},\left\{7\right\}\right\}\right)\cup \left(\left\{\left\{3,5\right\},\left\{3,7\right\},\left\{5,7\right\}\right\}\cup \left\{\left\{3,5,7\right\}\right\}\right)=\left(\left\{\varnothing ,\left\{3\right\},\left\{5\right\}\right\}\cup \left\{\left\{7\right\}\right\}\right)\cup \left(\left\{\left\{3,5\right\}\right\}\cup \left\{\left\{3,7\right\},\left\{5,7\right\},\left\{3,5,7\right\}\right\}\right)$$
20		un4	$$⊢\left(\left\{\varnothing ,\left\{3\right\},\left\{5\right\}\right\}\cup \left\{\left\{3,5\right\}\right\}\right)\cup \left(\left\{\left\{7\right\}\right\}\cup \left\{\left\{3,7\right\},\left\{5,7\right\},\left\{3,5,7\right\}\right\}\right)=\left(\left\{\varnothing ,\left\{3\right\},\left\{5\right\}\right\}\cup \left\{\left\{7\right\}\right\}\right)\cup \left(\left\{\left\{3,5\right\}\right\}\cup \left\{\left\{3,7\right\},\left\{5,7\right\},\left\{3,5,7\right\}\right\}\right)$$
21	19 20	eqtr4i	$$⊢\left(\left\{\varnothing \right\}\cup \left\{\left\{3\right\},\left\{5\right\},\left\{7\right\}\right\}\right)\cup \left(\left\{\left\{3,5\right\},\left\{3,7\right\},\left\{5,7\right\}\right\}\cup \left\{\left\{3,5,7\right\}\right\}\right)=\left(\left\{\varnothing ,\left\{3\right\},\left\{5\right\}\right\}\cup \left\{\left\{3,5\right\}\right\}\right)\cup \left(\left\{\left\{7\right\}\right\}\cup \left\{\left\{3,7\right\},\left\{5,7\right\},\left\{3,5,7\right\}\right\}\right)$$
22	4 5 21	3eqtr4i	$$⊢𝒫\left\{3,5,7\right\}=\left(\left\{\varnothing \right\}\cup \left\{\left\{3\right\},\left\{5\right\},\left\{7\right\}\right\}\right)\cup \left(\left\{\left\{3,5\right\},\left\{3,7\right\},\left\{5,7\right\}\right\}\cup \left\{\left\{3,5,7\right\}\right\}\right)$$
23	1 22	syl6eq	$$⊢A=\left\{3,5,7\right\}\to 𝒫A=\left(\left\{\varnothing \right\}\cup \left\{\left\{3\right\},\left\{5\right\},\left\{7\right\}\right\}\right)\cup \left(\left\{\left\{3,5\right\},\left\{3,7\right\},\left\{5,7\right\}\right\}\cup \left\{\left\{3,5,7\right\}\right\}\right)$$