Theorem map2xp

Description: A cardinal power with exponent 2 is equivalent to a Cartesian product with itself. (Contributed by Mario Carneiro, 31-May-2015) (Proof shortened by AV, 17-Jul-2022)

	Ref	Expression
Assertion	map2xp	$$⊢A\in V\to \left(A^{2_{𝑜}}\right)\approx \left(A\times A\right)$$

Proof

Step	Hyp	Ref	Expression
1		df2o3	$$⊢2_{𝑜}=\left\{\varnothing ,1_{𝑜}\right\}$$
2		df-pr	$$⊢\left\{\varnothing ,1_{𝑜}\right\}=\left\{\varnothing \right\}\cup \left\{1_{𝑜}\right\}$$
3	1 2	eqtri	$$⊢2_{𝑜}=\left\{\varnothing \right\}\cup \left\{1_{𝑜}\right\}$$
4	3	oveq2i	$$⊢A^{2_{𝑜}}=A^{\left(\left\{\varnothing \right\}\cup \left\{1_{𝑜}\right\}\right)}$$
5		snex	$$⊢\left\{\varnothing \right\}\in \mathrm{V}$$
6	5	a1i	$$⊢A\in V\to \left\{\varnothing \right\}\in \mathrm{V}$$
7		snex	$$⊢\left\{1_{𝑜}\right\}\in \mathrm{V}$$
8	7	a1i	$$⊢A\in V\to \left\{1_{𝑜}\right\}\in \mathrm{V}$$
9		id	$$⊢A\in V\to A\in V$$
10		1n0	$$⊢1_{𝑜}\ne \varnothing$$
11	10	neii	$$⊢\neg 1_{𝑜}=\varnothing$$
12		elsni	$$⊢1_{𝑜}\in \left\{\varnothing \right\}\to 1_{𝑜}=\varnothing$$
13	11 12	mto	$$⊢\neg 1_{𝑜}\in \left\{\varnothing \right\}$$
14		disjsn	$$⊢\left\{\varnothing \right\}\cap \left\{1_{𝑜}\right\}=\varnothing \leftrightarrow \neg 1_{𝑜}\in \left\{\varnothing \right\}$$
15	13 14	mpbir	$$⊢\left\{\varnothing \right\}\cap \left\{1_{𝑜}\right\}=\varnothing$$
16	15	a1i	$$⊢A\in V\to \left\{\varnothing \right\}\cap \left\{1_{𝑜}\right\}=\varnothing$$
17		mapunen	$$⊢\left(\left(\left\{\varnothing \right\}\in \mathrm{V}\wedge \left\{1_{𝑜}\right\}\in \mathrm{V}\wedge A\in V\right)\wedge \left\{\varnothing \right\}\cap \left\{1_{𝑜}\right\}=\varnothing \right)\to \left(A^{\left(\left\{\varnothing \right\}\cup \left\{1_{𝑜}\right\}\right)}\right)\approx \left(\left(A^{\left\{\varnothing \right\}}\right)\times \left(A^{\left\{1_{𝑜}\right\}}\right)\right)$$
18	6 8 9 16 17	syl31anc	$$⊢A\in V\to \left(A^{\left(\left\{\varnothing \right\}\cup \left\{1_{𝑜}\right\}\right)}\right)\approx \left(\left(A^{\left\{\varnothing \right\}}\right)\times \left(A^{\left\{1_{𝑜}\right\}}\right)\right)$$
19	4 18	eqbrtrid	$$⊢A\in V\to \left(A^{2_{𝑜}}\right)\approx \left(\left(A^{\left\{\varnothing \right\}}\right)\times \left(A^{\left\{1_{𝑜}\right\}}\right)\right)$$
20		0ex	$$⊢\varnothing \in \mathrm{V}$$
21	20	a1i	$$⊢A\in V\to \varnothing \in \mathrm{V}$$
22	9 21	mapsnend	$$⊢A\in V\to \left(A^{\left\{\varnothing \right\}}\right)\approx A$$
23		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
24	23	a1i	$$⊢A\in V\to 1_{𝑜}\in \mathrm{V}$$
25	9 24	mapsnend	$$⊢A\in V\to \left(A^{\left\{1_{𝑜}\right\}}\right)\approx A$$
26		xpen	$$⊢\left(\left(A^{\left\{\varnothing \right\}}\right)\approx A\wedge \left(A^{\left\{1_{𝑜}\right\}}\right)\approx A\right)\to \left(\left(A^{\left\{\varnothing \right\}}\right)\times \left(A^{\left\{1_{𝑜}\right\}}\right)\right)\approx \left(A\times A\right)$$
27	22 25 26	syl2anc	$$⊢A\in V\to \left(\left(A^{\left\{\varnothing \right\}}\right)\times \left(A^{\left\{1_{𝑜}\right\}}\right)\right)\approx \left(A\times A\right)$$
28		entr	$$⊢\left(\left(A^{2_{𝑜}}\right)\approx \left(\left(A^{\left\{\varnothing \right\}}\right)\times \left(A^{\left\{1_{𝑜}\right\}}\right)\right)\wedge \left(\left(A^{\left\{\varnothing \right\}}\right)\times \left(A^{\left\{1_{𝑜}\right\}}\right)\right)\approx \left(A\times A\right)\right)\to \left(A^{2_{𝑜}}\right)\approx \left(A\times A\right)$$
29	19 27 28	syl2anc	$$⊢A\in V\to \left(A^{2_{𝑜}}\right)\approx \left(A\times A\right)$$