Theorem altxpsspw

Description: An inclusion rule for alternate Cartesian products. (Contributed by Scott Fenton, 24-Mar-2012)

	Ref	Expression
Assertion	altxpsspw	$$⊢\left(A\mathrm{\times \times }B\right)\subseteq 𝒫𝒫\left(A\cup 𝒫B\right)$$

Proof

Step	Hyp	Ref	Expression
1		elaltxp	$$⊢z\in \left(A\mathrm{\times \times }B\right)\leftrightarrow \exists x\in A\exists y\in Bz=⟪x,y⟫$$
2		df-altop	$$⊢⟪x,y⟫=\left\{\left\{x\right\},\left\{x,\left\{y\right\}\right\}\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	5	adantr	$$⊢\left(x\in A\wedge y\in B\right)\to \left\{x\right\}\subseteq A\cup 𝒫B$$
7		elun1	$$⊢x\in A\to x\in \left(A\cup 𝒫B\right)$$
8		snssi	$$⊢y\in B\to \left\{y\right\}\subseteq B$$
9		vsnex	$$⊢\left\{y\right\}\in \mathrm{V}$$
10	9	elpw	$$⊢\left\{y\right\}\in 𝒫B\leftrightarrow \left\{y\right\}\subseteq B$$
11		elun2	$$⊢\left\{y\right\}\in 𝒫B\to \left\{y\right\}\in \left(A\cup 𝒫B\right)$$
12	10 11	sylbir	$$⊢\left\{y\right\}\subseteq B\to \left\{y\right\}\in \left(A\cup 𝒫B\right)$$
13	8 12	syl	$$⊢y\in B\to \left\{y\right\}\in \left(A\cup 𝒫B\right)$$
14	7 13	anim12i	$$⊢\left(x\in A\wedge y\in B\right)\to \left(x\in \left(A\cup 𝒫B\right)\wedge \left\{y\right\}\in \left(A\cup 𝒫B\right)\right)$$
15		vex	$$⊢x\in \mathrm{V}$$
16	15 9	prss	$$⊢\left(x\in \left(A\cup 𝒫B\right)\wedge \left\{y\right\}\in \left(A\cup 𝒫B\right)\right)\leftrightarrow \left\{x,\left\{y\right\}\right\}\subseteq A\cup 𝒫B$$
17	14 16	sylib	$$⊢\left(x\in A\wedge y\in B\right)\to \left\{x,\left\{y\right\}\right\}\subseteq A\cup 𝒫B$$
18		prex	$$⊢\left\{\left\{x\right\},\left\{x,\left\{y\right\}\right\}\right\}\in \mathrm{V}$$
19	18	elpw	$$⊢\left\{\left\{x\right\},\left\{x,\left\{y\right\}\right\}\right\}\in 𝒫𝒫\left(A\cup 𝒫B\right)\leftrightarrow \left\{\left\{x\right\},\left\{x,\left\{y\right\}\right\}\right\}\subseteq 𝒫\left(A\cup 𝒫B\right)$$
20		vsnex	$$⊢\left\{x\right\}\in \mathrm{V}$$
21		prex	$$⊢\left\{x,\left\{y\right\}\right\}\in \mathrm{V}$$
22	20 21	prsspw	$$⊢\left\{\left\{x\right\},\left\{x,\left\{y\right\}\right\}\right\}\subseteq 𝒫\left(A\cup 𝒫B\right)\leftrightarrow \left(\left\{x\right\}\subseteq A\cup 𝒫B\wedge \left\{x,\left\{y\right\}\right\}\subseteq A\cup 𝒫B\right)$$
23	19 22	bitri	$$⊢\left\{\left\{x\right\},\left\{x,\left\{y\right\}\right\}\right\}\in 𝒫𝒫\left(A\cup 𝒫B\right)\leftrightarrow \left(\left\{x\right\}\subseteq A\cup 𝒫B\wedge \left\{x,\left\{y\right\}\right\}\subseteq A\cup 𝒫B\right)$$
24	6 17 23	sylanbrc	$$⊢\left(x\in A\wedge y\in B\right)\to \left\{\left\{x\right\},\left\{x,\left\{y\right\}\right\}\right\}\in 𝒫𝒫\left(A\cup 𝒫B\right)$$
25	2 24	eqeltrid	$$⊢\left(x\in A\wedge y\in B\right)\to ⟪x,y⟫\in 𝒫𝒫\left(A\cup 𝒫B\right)$$
26		eleq1a	$$⊢⟪x,y⟫\in 𝒫𝒫\left(A\cup 𝒫B\right)\to \left(z=⟪x,y⟫\to z\in 𝒫𝒫\left(A\cup 𝒫B\right)\right)$$
27	25 26	syl	$$⊢\left(x\in A\wedge y\in B\right)\to \left(z=⟪x,y⟫\to z\in 𝒫𝒫\left(A\cup 𝒫B\right)\right)$$
28	27	rexlimivv	$$⊢\exists x\in A\exists y\in Bz=⟪x,y⟫\to z\in 𝒫𝒫\left(A\cup 𝒫B\right)$$
29	1 28	sylbi	$$⊢z\in \left(A\mathrm{\times \times }B\right)\to z\in 𝒫𝒫\left(A\cup 𝒫B\right)$$
30	29	ssriv	$$⊢\left(A\mathrm{\times \times }B\right)\subseteq 𝒫𝒫\left(A\cup 𝒫B\right)$$