Theorem xpsspw

Description: A Cartesian product is included in the power of the power of the union of its arguments. (Contributed by NM, 13-Sep-2006)

	Ref	Expression
Assertion	xpsspw	$$⊢A\times B\subseteq 𝒫𝒫\left(A\cup B\right)$$

Proof

Step	Hyp	Ref	Expression
1		relxp	$$⊢\mathrm{Rel}\left(A\times B\right)$$
2		opelxp	$$⊢⟨x,y⟩\in \left(A\times B\right)\leftrightarrow \left(x\in A\wedge y\in B\right)$$
3		snssi	$$⊢x\in A\to \left\{x\right\}\subseteq A$$
4		ssun3	$$⊢\left\{x\right\}\subseteq A\to \left\{x\right\}\subseteq A\cup B$$
5	3 4	syl	$$⊢x\in A\to \left\{x\right\}\subseteq A\cup B$$
6		snex	$$⊢\left\{x\right\}\in \mathrm{V}$$
7	6	elpw	$$⊢\left\{x\right\}\in 𝒫\left(A\cup B\right)\leftrightarrow \left\{x\right\}\subseteq A\cup B$$
8	5 7	sylibr	$$⊢x\in A\to \left\{x\right\}\in 𝒫\left(A\cup B\right)$$
9	8	adantr	$$⊢\left(x\in A\wedge y\in B\right)\to \left\{x\right\}\in 𝒫\left(A\cup B\right)$$
10		df-pr	$$⊢\left\{x,y\right\}=\left\{x\right\}\cup \left\{y\right\}$$
11		snssi	$$⊢y\in B\to \left\{y\right\}\subseteq B$$
12		ssun4	$$⊢\left\{y\right\}\subseteq B\to \left\{y\right\}\subseteq A\cup B$$
13	11 12	syl	$$⊢y\in B\to \left\{y\right\}\subseteq A\cup B$$
14	5 13	anim12i	$$⊢\left(x\in A\wedge y\in B\right)\to \left(\left\{x\right\}\subseteq A\cup B\wedge \left\{y\right\}\subseteq A\cup B\right)$$
15		unss	$$⊢\left(\left\{x\right\}\subseteq A\cup B\wedge \left\{y\right\}\subseteq A\cup B\right)\leftrightarrow \left\{x\right\}\cup \left\{y\right\}\subseteq A\cup B$$
16	14 15	sylib	$$⊢\left(x\in A\wedge y\in B\right)\to \left\{x\right\}\cup \left\{y\right\}\subseteq A\cup B$$
17	10 16	eqsstrid	$$⊢\left(x\in A\wedge y\in B\right)\to \left\{x,y\right\}\subseteq A\cup B$$
18		zfpair2	$$⊢\left\{x,y\right\}\in \mathrm{V}$$
19	18	elpw	$$⊢\left\{x,y\right\}\in 𝒫\left(A\cup B\right)\leftrightarrow \left\{x,y\right\}\subseteq A\cup B$$
20	17 19	sylibr	$$⊢\left(x\in A\wedge y\in B\right)\to \left\{x,y\right\}\in 𝒫\left(A\cup B\right)$$
21	9 20	jca	$$⊢\left(x\in A\wedge y\in B\right)\to \left(\left\{x\right\}\in 𝒫\left(A\cup B\right)\wedge \left\{x,y\right\}\in 𝒫\left(A\cup B\right)\right)$$
22		prex	$$⊢\left\{\left\{x\right\},\left\{x,y\right\}\right\}\in \mathrm{V}$$
23	22	elpw	$$⊢\left\{\left\{x\right\},\left\{x,y\right\}\right\}\in 𝒫𝒫\left(A\cup B\right)\leftrightarrow \left\{\left\{x\right\},\left\{x,y\right\}\right\}\subseteq 𝒫\left(A\cup B\right)$$
24		vex	$$⊢x\in \mathrm{V}$$
25		vex	$$⊢y\in \mathrm{V}$$
26	24 25	dfop	$$⊢⟨x,y⟩=\left\{\left\{x\right\},\left\{x,y\right\}\right\}$$
27	26	eleq1i	$$⊢⟨x,y⟩\in 𝒫𝒫\left(A\cup B\right)\leftrightarrow \left\{\left\{x\right\},\left\{x,y\right\}\right\}\in 𝒫𝒫\left(A\cup B\right)$$
28	6 18	prss	$$⊢\left(\left\{x\right\}\in 𝒫\left(A\cup B\right)\wedge \left\{x,y\right\}\in 𝒫\left(A\cup B\right)\right)\leftrightarrow \left\{\left\{x\right\},\left\{x,y\right\}\right\}\subseteq 𝒫\left(A\cup B\right)$$
29	23 27 28	3bitr4ri	$$⊢\left(\left\{x\right\}\in 𝒫\left(A\cup B\right)\wedge \left\{x,y\right\}\in 𝒫\left(A\cup B\right)\right)\leftrightarrow ⟨x,y⟩\in 𝒫𝒫\left(A\cup B\right)$$
30	21 29	sylib	$$⊢\left(x\in A\wedge y\in B\right)\to ⟨x,y⟩\in 𝒫𝒫\left(A\cup B\right)$$
31	2 30	sylbi	$$⊢⟨x,y⟩\in \left(A\times B\right)\to ⟨x,y⟩\in 𝒫𝒫\left(A\cup B\right)$$
32	1 31	relssi	$$⊢A\times B\subseteq 𝒫𝒫\left(A\cup B\right)$$