# Metamath Proof Explorer

## 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}×{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 ${⊢}¬{1}_{𝑜}=\varnothing$
12 elsni ${⊢}{1}_{𝑜}\in \left\{\varnothing \right\}\to {1}_{𝑜}=\varnothing$
13 11 12 mto ${⊢}¬{1}_{𝑜}\in \left\{\varnothing \right\}$
14 disjsn ${⊢}\left\{\varnothing \right\}\cap \left\{{1}_{𝑜}\right\}=\varnothing ↔¬{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)×\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)×\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)×\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)×\left({{A}}^{\left\{{1}_{𝑜}\right\}}\right)\right)\approx \left({A}×{A}\right)$
27 22 25 26 syl2anc ${⊢}{A}\in {V}\to \left(\left({{A}}^{\left\{\varnothing \right\}}\right)×\left({{A}}^{\left\{{1}_{𝑜}\right\}}\right)\right)\approx \left({A}×{A}\right)$
28 entr ${⊢}\left(\left({{A}}^{{2}_{𝑜}}\right)\approx \left(\left({{A}}^{\left\{\varnothing \right\}}\right)×\left({{A}}^{\left\{{1}_{𝑜}\right\}}\right)\right)\wedge \left(\left({{A}}^{\left\{\varnothing \right\}}\right)×\left({{A}}^{\left\{{1}_{𝑜}\right\}}\right)\right)\approx \left({A}×{A}\right)\right)\to \left({{A}}^{{2}_{𝑜}}\right)\approx \left({A}×{A}\right)$
29 19 27 28 syl2anc ${⊢}{A}\in {V}\to \left({{A}}^{{2}_{𝑜}}\right)\approx \left({A}×{A}\right)$